text:
{-# OPTIONS --without-K --safe #-}

module Dodo.Binary.Acyclic where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Function using (flip)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary using (Rel; REL)
open import Relation.Binary using (Irreflexive; Transitive; Symmetric)
open import Relation.Binary.Construct.Closure.Transitive using (TransClosure; [_]; _∷_; _++_)
-- Local imports
open import Dodo.Binary.Equality
open import Dodo.Binary.Transitive

-- # Definitions

-- | Acyclicity of a binary relation R: x R⁺ y → x ≠ y
--
-- Defined with an underlying equality (≈)
Acyclic : {a ℓ₁ ℓ₂ : Level} → {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
Acyclic _≈_ _<_ = Irreflexive _≈_ (TransClosure _<_)

-- # Operations

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a}
    {_≈_ : Rel A ℓ₁} {R : Rel A ℓ₂} where

  -- | Any acyclic relation is also irreflexive
  Acyclic⇒Irreflexive : Acyclic _≈_ R → Irreflexive _≈_ R
  Acyclic⇒Irreflexive acyclicR x≈y Rxy = acyclicR x≈y [ Rxy ]

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a}
    {_≈_ : Rel A ℓ₁} {P : Rel A ℓ₂} {Q : Rel A ℓ₃} where

  -- | If a relation is acyclic, then any subset of that relation is also acyclic
  acyclic-⊆₂ : Acyclic _≈_ Q → P ⊆₂ Q → Acyclic _≈_ P
  acyclic-⊆₂ acyclicQ P⊆Q x≈y P⁺ = acyclicQ x≈y (⊆₂-apply (⁺-preserves-⊆₂ P⊆Q) P⁺)

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a}
    {_≈_ : Rel A ℓ₁} {R : Rel A ℓ₂} where

  -- | If a relation is acyclic, then its transitive closure is also acyclic
  ⁺-preserves-acyclic : Acyclic _≈_ R → Acyclic _≈_ (TransClosure R)
  ⁺-preserves-acyclic acR x≈y R⁺⁺xy = acR x≈y (⇔₂-apply-⊇₂ ⁺-idem R⁺⁺xy)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
postulate
  F : Set₁ → Set₁

data P : Set₁ → Set₁ where
  c : P (F (P Set)) → P Set

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- There was a bug where reexported constructors weren't
-- properly translated when termination checking.
module OpenPublicTermination where

 module A where
   data U : Set where
     nat  : U
     list : U -> U

 module A' where
   open A public

 open A'

 f : U -> U
 f nat = nat
 f (list nat) = nat
 f (list (list u)) = f (list u)


text:
------------------------------------------------------------------------
-- Simple regular expression matcher (without soundness proof)
------------------------------------------------------------------------

open import Eq
open import Setoids
open import Prelude
import RegExps

module BoolMatcher (D : Datoid) where

private
  open module D' = Datoid D
  open module S' = Setoid setoid
  open module R  = RegExps setoid

infix 4 _∈‿⟦_⟧¿

------------------------------------------------------------------------
-- Helper function

decToBool : forall {x y} -> Dec (x ≈ y) -> Bool
decToBool (yes _) = true
decToBool (no _)  = false

------------------------------------------------------------------------
-- Regular expression matcher

matches-⊙¿ : (xs₁ xs₂ : [ carrier ]) -> (re₁ re₂ : RegExp) -> Bool

_∈‿⟦_⟧¿ : (xs : [ carrier ]) -> (re : RegExp) -> Bool
[]     ∈‿⟦ ε ⟧¿         = true
x ∷ [] ∈‿⟦ • ⟧¿         = true
x ∷ [] ∈‿⟦ sym y ⟧¿     = decToBool (x ≟ y)
xs     ∈‿⟦ re₁ ∣ re₂ ⟧¿ = xs ∈‿⟦ re₁ ⟧¿ ∨ xs ∈‿⟦ re₂ ⟧¿
xs     ∈‿⟦ re₁ ⊙ re₂ ⟧¿ = matches-⊙¿ [] xs re₁ re₂
[]     ∈‿⟦ re ⋆ ⟧¿      = true
x ∷ xs ∈‿⟦ re ⋆ ⟧¿      = matches-⊙¿ (x ∷ []) xs re (re ⋆)
_      ∈‿⟦ _ ⟧¿         = false

matches-⊙¿ xs₁ xs₂       re₁ re₂ with xs₁ ∈‿⟦ re₁ ⟧¿ ∨ xs₂ ∈‿⟦ re₂ ⟧¿
matches-⊙¿ xs₁ xs₂       re₁ re₂ | true  = true
matches-⊙¿ xs₁ []        re₁ re₂ | false = false
matches-⊙¿ xs₁ (x ∷ xs₂) re₁ re₂ | false =
  matches-⊙¿ (xs₁ ++ x ∷ []) xs₂ re₁ re₂

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.def.fun:10 -v tc.def.where:100 #-}

module PartialityMonad where

open import Common.Level
open import Common.Coinduction

record RawMonad {f} (M : Set f → Set f) : Set (lsuc f) where
  infixl 1 _>>=_

  field
    return : ∀ {A} → A → M A
    _>>=_  : ∀ {A B} → M A → (A → M B) → M B

------------------------------------------------------------------------
-- The partiality monad

data _⊥ {a} (A : Set a) : Set a where
  now   : (x : A) → A ⊥
  later : (x : ∞ (A ⊥)) → A ⊥

-- Fails if hidden pattern {f} is removed
monad : ∀ {f} → RawMonad {f = f} _⊥
-- monad {f} = record
monad = record
  { return = now
  ; _>>=_  = _>>=_
  }
  where
  _>>=_ : ∀ {A B} → A ⊥ → (A → B ⊥) → B ⊥
  now x   >>= f = f x
  later x >>= f = later (♯ (♭ x >>= f))

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
----------------------------------------------------------------------------
-- The FOTC lists of natural numbers type
----------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Data.Nat.List.Type where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- The FOTC lists of natural numbers type (inductive predicate for
-- total lists of natural numbers).
data ListN : D → Set where
  lnnil  : ListN []
  lncons : ∀ {n ns} → N n → ListN ns → ListN (n ∷ ns)
{-# ATP axioms lnnil lncons #-}

-- Induction principle.
ListN-ind : (A : D → Set) →
            A [] →
            (∀ {n ns} → N n → A ns → A (n ∷ ns)) →
            ∀ {ns} → ListN ns → A ns
ListN-ind A A[] h lnnil           = A[]
ListN-ind A A[] h (lncons Nn Lns) = h Nn (ListN-ind A A[] h Lns)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module x04equality where

------------------------------------------------------------------------------
-- EQUALITY

-- for any      type A
-- for any x of type A
-- refl constructor provides evidence that x ≡ x
-- i.e., every value is equal to itself
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

infix 4 _≡_

-- tell Agda which type corresponds to equality
{-# BUILTIN EQUALITY _≡_ #-}

{-
Note:
- 1st arg to _≡_ is PARAMETER (x : A)
  - BEST PRACTICE: use parameters when possible
  - can be a parameter because it does not vary
- 2nd arg is an INDEX in A → Set
  - must be an index, so it can be required to be equal to the first

------------------------------------------------------------------------------
-- EQUALITY is an EQUIVALENCE RELATION (reflexive, symmetric, transitive)

reflexivity in the def of equality, via refl constructor
-}

-- symmetry
sym : ∀ {A : Set} {x y : A}
  → x ≡ y  -- arg has type x ≡ y
    -----
  → y ≡ x
sym refl -- LHS :instantiates arg to refl CONSTRUCTOR (only one possible)
         -- refl requires x y to be the same
  = refl -- RHS : need a term of type x ≡ x, so refl

-- transitive
trans : ∀ {A : Set} {x y z : A}
  → x ≡ y
  →     y ≡ z
    -----
  → x ≡     z
trans refl refl = refl

------------------------------------------------------------------------------
-- EQUALITY SATISFIES CONGRUENCE

-- if two terms are equal, they remain so after same function is applied to both
cong : ∀ {A B : Set} (f : A → B) {x y : A}
  →   x ≡   y
    ---------
  → f x ≡ f y
cong f refl = refl

-- where f takes two args
cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B}
  →   u   ≡   x
  →     v ≡     y
    -------------
  → f u v ≡ f x y
cong₂ f refl refl = refl

-- if two functions are equal, then applying them to same term yields equal terms
cong-app : ∀ {A B : Set} {f g : A → B}
  →             f   ≡ g
    ---------------------
  → ∀ (x : A) → f x ≡ g x
cong-app refl x = refl

------------------------------------------------------------------------------
-- EQUALITY SATISFIES SUBSTITUTION

-- if two values are equal and a predicate holds of first then it also holds of second
subst : ∀ {A : Set} {x y : A} (P : A → Set)
  →   x ≡  y
    ---------
  → P x
  →     P y
subst P refl px = px

------------------------------------------------------------------------------
--  CHAINS OF EQUATIONS (aka EQUATIONAL REASONING)

module ≡-Reasoning {A : Set} where

  infix  1 begin_
  infixr 2 _≡⟨⟩_ _≡⟨_⟩_
  infix  3 _∎

  -- identity : this is just used to make proof look nice
  begin_ : ∀ {x y : A}
    → x ≡ y
      -----
    → x ≡ y
  begin x≡y = x≡y

  -- think of _≡⟨⟩_ as equivalent to _≡⟨ refl ⟩_
  _≡⟨⟩_ : ∀ (x : A) {y : A}
    → x ≡ y
      -----
    → x ≡ y
  x ≡⟨⟩ x≡y = x≡y

  _≡⟨_⟩_ : ∀ (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
      -----
    → x ≡ z
  x ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z

  _∎ : ∀ (x : A)
      -----
    → x ≡ x
  x ∎ = refl

open ≡-Reasoning

trans′ : ∀ {A : Set} {x y z : A}
  → x ≡ y
  →     y ≡ z
    -----
  → x ≡     z
trans′ {A} {x} {y} {z} x≡y y≡z =
  begin          -- Goal: x ≡ z   ; y≡z : y ≡ z; x≡y : x ≡ y
    x ≡⟨ x≡y ⟩   -- Goal: y ≡ z
    y ≡⟨ y≡z ⟩   -- Goal: z ≡ z
    z
  ∎

{-
EXERCISE trans and ≡-Reasoning (practice) TODO
Cannot use definition of trans’ using ≡-Reasoning as the definition for trans.
Why?
Hint: look at the definition of _≡⟨_⟩_

-- Your code goes here

------------------------------------------------------------------------------
Chains of equations, another example : addition is commutative
-}

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ
zero    + n = n
(suc m) + n = suc (m + n)

infixl 6  _+_

-- to save space, postulate (rather than prove) two lemmas:
-- POSTULATE : specifies a signature but no def. Use with care. DON'T postulate something false!
postulate
  +-identity : ∀ (m   : ℕ) → m + zero  ≡ m
  +-suc      : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero    ≡⟨ +-identity m ⟩
    m           ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
         m + suc n  ≡⟨ +-suc m n ⟩
    suc (m +     n) ≡⟨ cong suc (+-comm m n) ⟩
    suc (n +     m) ≡⟨⟩ -- terms are equivalent to simplified term
    suc  n +     m
  ∎

{-
------------------------------------------------------------------------------
Exercise ≤-Reasoning (stretch)

redo proof of +-monoʳ-≤ (from Chapter Relations) using an analogue of ≡-Reasoning

define ≤-Reasoning

use it to write out proof that addition is monotonic with regard to inequality
by redoing all of +-monoˡ-≤, +-monoʳ-≤, and +-mono-≤
-}

module ≤-Reasoning {A : Set} where

  data _≤_ : ℕ → ℕ → Set where
    z≤n : ∀ {n : ℕ}
        --------
      → zero ≤ n

    s≤s : ∀ {m n : ℕ}
      →     m ≤     n
        -------------
      → suc m ≤ suc n

  infix 4 _≤_

  ≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
  ≤-trans      z≤n         _  = z≤n
  ≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

  infix  1 begin≤_
  infixr 2 _≤⟨⟩_ _≤⟨_⟩_
  infix  3 _∎≤

  --------------------------------------------------

  begin≤_ : ∀ {x y : ℕ}
    → x ≤ y
      -----
    → x ≤ y
  begin≤ x≤y = x≤y

  -- can think of _≤⟨⟩_ as equivalent to _≤⟨ refl ⟩_
  _≤⟨⟩_ : ∀ (x : ℕ) {y : ℕ}
    → x ≤ y
      -----
    → x ≤ y
  x ≤⟨⟩ x≤y = x≤y

  _≤⟨_⟩_ : ∀ (x : ℕ) {y z : ℕ}
    → x ≤ y
    → y ≤ z
      -----
    → x ≤ z
  x ≤⟨ x≤y ⟩ y≤z = ≤-trans x≤y y≤z

  _∎≤ : ∀ (x : ℕ)
      -----
    → x ≤ x
  zero  ∎≤ = z≤n
  suc x ∎≤ = s≤s (x ∎≤)

  --------------------------------------------------

  +-monoʳ-≤ : ∀ (n p q : ℕ)
    →      p  ≤      q
      -------------
    → (n + p) ≤ (n + q)

  +-monoʳ-≤ zero    p q p≤q  =
    begin≤
      zero + p ≤⟨⟩
             p ≤⟨ p≤q ⟩
             q ≤⟨⟩
      zero + q
    ∎≤

  +-monoʳ-≤ (suc n) p q p≤q =
    begin≤
      suc n + p ≤⟨ s≤s (+-monoʳ-≤ n p q p≤q) ⟩
      suc n + q
    ∎≤

  -------------------------

  postulate
    +-comm-≤ : ∀ (m n : ℕ) → m + n ≤ n + m

  +-monoˡ-≤ : ∀ (m n p : ℕ)
    → m     ≤ n
      -------------
    → m + p ≤ n + p

  +-monoˡ-≤ m n p m≤n =
    begin≤
      m + p ≤⟨ +-comm-≤ m p ⟩
      p + m ≤⟨ +-monoʳ-≤ p m n m≤n ⟩
      p + n ≤⟨ +-comm-≤ p n ⟩
      n + p
    ∎≤

  -------------------------

  +-mono-≤ : ∀ (m n p q : ℕ)
    → m     ≤ n
    →     p ≤     q
      -------------
    → m + p ≤ n + q
  +-mono-≤ m n p q m≤n p≤q =
    begin≤
      m + p ≤⟨ +-monoˡ-≤ m n p m≤n ⟩
      n + p ≤⟨ +-monoʳ-≤ n p q p≤q ⟩
      n + q
    ∎≤

{-
------------------------------------------------------------------------------
-- Rewriting
-}

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd       n
      ------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even     n
      -----------
    → odd (suc n)

{-
given even (m + n) holds
prove even (n + m) holds

REWRITE: notation to support this kind of reasoning
-}

-- then use rewrite
even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev      -- even (n + m)
  rewrite +-comm n m  -- Goal: even (m + n); ev : even (m + n)
  = ev

{-
keyword REWRITE : followed by evidence of an equality
That equality is used to rewrite the type of the goal and of any variable in scope.
-}

even-comm' : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm' m n ev        -- Goal: even (n + m)  ; ev : even (m + n)
  rewrite
    +-comm m n           -- Goal: even (n + m)  ; ev : even (n + m) <-- rewrites evidence
  = ev --   ^
--          note: arg order diff than 'even-comm' above

------------------------------------------------------------------------------
-- Multiple rewrites : each separated by a vertical bar

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ zero    n        --    zero + n ≡ n + zero
                         --           n ≡ n + zero
  rewrite
    +-identity n         --           n ≡ n
  = refl
+-comm′ (suc m) n        -- suc  m + n  ≡ n + suc m
                         -- suc (m + n) ≡ n + suc m
  rewrite
    +-suc   n m          -- suc (m + n) ≡ suc (n + m) <-- rewrites LHS
  | +-comm′ m n          -- suc (n + m) ≡ suc (n + m) <-- rewrites RHS
  = refl

{-
Previous +-comm proof required cong suc (+-comm m n) (invoking inductive hypothesis).
Rewriting automatically takes congruence into account.
Proofs with rewriting are shorter.
Proofs as chains of equalities are easier to follow.
-}

+-comm′' : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′' zero    n =
  begin
    zero + n ≡⟨⟩
           n ≡⟨ +-comm′ zero n ⟩
    n + zero
  ∎
+-comm′' (suc m) n =
  begin
    suc m + n ≡⟨ +-comm′ (suc m)  n ⟩
    n + suc m
  ∎

{-
------------------------------------------------------------------------------
--rewrite is shorthand for 'WITH'
-}

even-comm′ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm′ m n ev with   m + n  | +-comm m n
...                  | .(n + m) | refl       = ev

{-
WITH : can be followed by one or more expressions, separated by bars
- where each equation has the same number of patterns

1st COLUMN asserts m + n and n + m are identical
2nd COLUMN justifies assertion with evidence of the appropriate equality

DOT PATTERN : .(n + m)
- dot followed by an expression
- used when other info forces value matched to be equal to value of expression in dot pattern

Here: m + n ≡ n + m justified by matching +-comm m n with refl

------------------------------------------------------------------------------
-- using SUBSTITUTION instead of REWRITE
-}

even-comm″ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm″ m n
  --      m + n ≡ n + m
  --            v
--= subst even {!!}
--= subst {!!}  (+-comm m n)
--         ^
-- Constraints
-- ?0 (n + m) =< even (n + m)
-- even (m + n) =< ?0 (m + n)
  = subst even (+-comm m n)

{-
------------------------------------------------------------------------------
-- Leibniz equality : TWO OBJECTS EQUAL IFF THEY SATISFY THE SAME PROPERTIES.

The form of asserting equality so far is due to Martin Löf (1975).

Another form is due to Leibniz (1686).

Define Leibniz equality and show that two terms satisfy Leibniz equality
IFF they satisfy Martin Löf equality.

x ≐ y
holds if
every property P that holds of x also holds of y
also ensures converse
every property P that holds of y also holds of x

Let x and y be objects of type A.
x ≐ y holds if for every predicate P over type A we have that P x implies P y:
-}

_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

{-
write _≐_ {A} x y (instead of infix) to provide access to the implicit parameter A

FIRST USE OF LEVELS

Cannot assign Set the type Set
- would lead to contradictions such as Russell’s Paradox and Girard’s Paradox

hierarchy of types, where Set : Set₁, Set₁ : Set₂, ...

'Set' is an abbreviation for 'Set₀'

Since the equation defining _≐_ mentions Set on the right-hand side,
the corresponding signature must use Set₁.

------------------------------------------------------------------------------
Leibniz equality is reflexive, transitive, symmetric
-}

-- reflexiviity follows by a variant of the identity function
refl-≐ : ∀ {A : Set} {x : A}
  → x ≐ x
refl-≐ P Px = Px

-- transitivity follows by a variant of function composition
trans-≐ : ∀ {A : Set} {x y z : A}
  → x ≐ y
  → y ≐ z
    -----
  → x ≐ z
trans-≐ x≐y y≐z P Px = y≐z P (x≐y P Px)

-- show that if P x implies P y for all predicates P
-- then         P y implies P x
sym-≐ : ∀ {A : Set} {x y : A}
  → x ≐ y           -- given x ≐ y
    -----
  → y ≐ x
sym-≐ {A} {x} {y} x≐y P = Qy -- TODO : where is 'P' in the signature?
  where
    Q : A → Set     -- instantiate the equality with a predicate Q such that Q z holds
    Q z = P z → P x -- if P z implies P x

    Qx : Q x        -- The property Q x is by reflexivity, and hence Q y follows from x ≐ y.
    Qx = refl-≐ P

    Qy : Q y        --  Q y is the required proof : P y implies P x
    Qy = x≐y Q Qx

{-
------------------------------------------------------------------------------
Martin Löf equality implies Leibniz equality

given x ≡ y
need for any P to take evidence of P x to evidence of P y

the equality of x and y implies that any proof of P x is also a proof of P y
follows from substitution
-}

≡-implies-≐ : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → x ≐ y
≡-implies-≐ x≡y P = subst P x≡y

{-
------------------------------------------------------------------------------
Leibniz equality implies Martin Löf equality

given for any P we can take a proof of P x to a proof of P y
show x ≡ y

proof is similar to that for symmetry of Leibniz equality
-}

≐-implies-≡ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → x ≡ y
≐-implies-≡ {A} {x} {y} x≐y = Qy
  where
    Q : A → Set   -- Q is predicate that holds of z if x ≡ z
    Q z = x ≡ z

    Qx : Q x      -- Q x by reflexivity of Martin Löf equality
    Qx = refl

    Qy : Q y      -- Q y follows from x ≐ y
    Qy = x≐y Q Qx -- Q y is required proof : x ≡ y

{-
This section adapted from
≐≃≡: Leibniz Equality is Isomorphic to Martin-Löf Identity, Parametrically
draft/2017
by Andreas Abel, Jesper Cockx, Dominique Devries, Andreas Nuyts, and Philip Wadler

------------------------------------------------------------------------------
UNIVERSE POLYMORPHISM (aka LEVELs)

every type belongs somewhere in the hierarchy Set₀, Set₁, Set₂, ...

Set abbreviates Set₀

Set₀ : Set₁
Set₁ : Set₂
...

to compare values of a type that belongs to Set ℓ for some arbitrary level ℓ?

via UNIVERSE POLYMORPHISM

definition is made with respect to an arbitrary level ℓ

to use levels:
-}

open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)

{-
rename constructors zero and suc to avoid confusion between levels and naturals

Levels are isomorphic to natural numbers, and have similar constructors:

lzero : Level
lsuc  : Level → Level

Set₀, Set₁, Set₂, ... abbreviations for

Set lzero
Set (lsuc lzero)
Set (lsuc (lsuc lzero))

_⊔_ : Level → Level → Level

that given two levels returns the larger of the two.
-}

-- equality, generalised to an arbitrary level:
data _≡′_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl′ : x ≡′ x

-- generalised definition of symmetry:
sym′ : ∀ {ℓ : Level} {A : Set ℓ} {x y : A}
  → x ≡′ y
    ------
  → y ≡′ x
sym′ refl′ = refl′

{-
For simplicity, this book avoids universe polymorphism.
Most definitions in the standard library are generalised to arbitrary levels as above.
-}

-- generalised definition of Leibniz equality:
_≐′_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
_≐′_ {ℓ} {A} x y = ∀ (P : A → Set ℓ) → P x → P y

{-
Before the signature used Set₁ as the type of a term that includes Set,
whereas here the signature uses Set (lsuc ℓ) as the type of a term that includes Set ℓ.

Most other functions in the standard library are also generalised to arbitrary levels.
-}

-- definition of composition.
_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
  → (B → C) → (A → B) → A → C
(g ∘ f) x = g (f x)

{-
------------------------------------------------------------------------------
Standard library

standard library defines _≡⟨_⟩_ as step-≡,
which reverses the order of the arguments

standard library defines a macro,imported when import step-≡
which recovers the original argument order:

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

------------------------------------------------------------------------------
Unicode

≡  U+2261  IDENTICAL TO                     (\==, \equiv)
⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET  (\<)
⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
∎  U+220E  END OF PROOF                     (\qed)
≐  U+2250  APPROACHES THE LIMIT             (\.=)
ℓ  U+2113  SCRIPT SMALL L                   (\ell)
⊔  U+2294  SQUARE CUP                       (\lub)
₀  U+2080  SUBSCRIPT ZERO                   (\_0)
₁  U+2081  SUBSCRIPT ONE                    (\_1)
₂  U+2082  SUBSCRIPT TWO                    (\_2)
-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module List where

  data List (a : Set) : Set where
    nil  : List a
    _::_ : a -> List a -> List a

  nil2 : (\x -> x) ({a : Set} -> List a)
  nil2 = nil {_}

  tt : Set1 -> Set2
  tt _ = Set1

  map : {a b : Set} -> (a -> b) -> List a -> List b
  map f nil       = nil
  map f (x :: xs) = f x :: map f xs

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
module Issue892a where

record R : Set₁ where
  field f : Set
  g : Set
  g = f

-- The type of R.g should print as (r : R) → Set
-- rather than ( : R) → Set.
bad : R.g
bad = ?


text:
{-# OPTIONS --exact-split #-}
module Thesis.SIRelBigStep.DOpSem where

open import Data.Nat
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Thesis.SIRelBigStep.DLangDerive public
open import Thesis.SIRelBigStep.OpSem public
open import Thesis.SIRelBigStep.DSyntax public

data DVal : Type → Set
import Base.Denotation.Environment
module D = Base.Denotation.Environment DType DVal

ChΔ : ∀ (Δ : Context) → Set
ChΔ Δ = D.⟦ Δ ⟧Context

data DVal where
  bang : ∀ {τ} → Val τ → DVal τ
  dclosure : ∀ {Γ σ τ} → (dt : DTerm (σ • Γ) τ) → (ρ : ⟦ Γ ⟧Context) →  (dρ : ChΔ Γ) → DVal (σ ⇒ τ)
  dnatV : ∀ (n : ℕ) → DVal nat
  dpairV : ∀ {σ τ} → DVal σ → DVal τ → DVal (pair σ τ)

_⊕_ : ∀ {τ} → (v1 : Val τ) (dv : DVal τ) → Val τ

_⊕ρ_ : ∀ {Γ} → ⟦ Γ ⟧Context → ChΔ Γ → ⟦ Γ ⟧Context
∅ ⊕ρ ∅ = ∅
(v • ρ1) ⊕ρ (dv • dρ) = v ⊕ dv • ρ1 ⊕ρ dρ

v1 ⊕ bang v2 = v2
closure {Γ} t ρ ⊕ dclosure {Γ1} dt ρ₁ dρ with Γ ≟Ctx Γ1
closure {Γ} t ρ ⊕ dclosure {.Γ} dt ρ₁ dρ | yes refl = closure t (ρ ⊕ρ dρ)
... | no ¬p = closure t ρ
natV n ⊕ dnatV dn = natV (n + dn)
pairV v1 v2 ⊕ dpairV dv1 dv2 = pairV (v1 ⊕ dv1) (v2 ⊕ dv2)

inv-Δτ-nat : ∀ τ → Δτ τ ≡ nat → τ ≡ nat
inv-Δτ-nat nat refl = refl
inv-Δτ-nat (τ ⇒ τ₁) ()
inv-Δτ-nat (pair τ τ₁) ()

deval-const : ∀ {τ} → Const (Δτ τ) → DVal τ
deval-const {σ} c with Δτ σ | inv-Δτ-nat σ
deval-const {σ} (lit n) | .nat | inv-σ with inv-σ refl
deval-const {.nat} (lit n) | .nat | inv-σ | refl = dnatV n

deval : ∀ {Γ τ} (sv : DSVal Γ τ) (ρ : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) → DVal τ
deval (dvar x) ρ dρ = D.⟦ x ⟧Var dρ
deval (dabs dt) ρ dρ = dclosure dt ρ dρ
deval (dcons dsv1 dsv2) ρ dρ = dpairV (deval dsv1 ρ dρ) (deval dsv2 ρ dρ)
deval (dconst c) ρ dρ = deval-const c

deval-primitive : ∀ {σ τ} → Primitive (σ ⇒ τ) → Val σ → DVal σ → DVal τ
deval-primitive succ (natV _) (bang (natV n2)) = bang (natV (suc n2))
deval-primitive succ (natV n) (dnatV dn) = dnatV dn
deval-primitive add (pairV _ _) (dpairV (dnatV da) (dnatV db)) = dnatV (da + db)
deval-primitive add (pairV _ _) (bang p2) = bang (eval-primitive add p2)
-- During the proof we need to know which clauses hold definitionally, and sadly we can't get a single equation here.
deval-primitive add p1 @ (pairV a1 b1) dp @ (dpairV (dnatV da) (bang b2)) = bang (eval-primitive add (p1 ⊕ dp))
deval-primitive add p1 @ (pairV a1 b1) dp @ (dpairV (bang a2) db) = bang (eval-primitive add (p1 ⊕ dp))

deval-derive-const-inv : ∀ {τ Γ} (c : Const τ) (ρ : ⟦ Γ ⟧Context) dρ → deval (derive-const c) ρ dρ ≡ deval (derive-const c) ∅ ∅
deval-derive-const-inv (lit n) ρ dρ = refl

data _D_⊢_↓_ {Γ} (ρ : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) : ∀ {τ} → DTerm Γ τ → DVal τ → Set where
  dval : ∀ {τ} (sv : DSVal Γ τ) →
    ρ D dρ ⊢ dval sv ↓ deval sv ρ dρ
  dprimapp : ∀ {σ τ} (p : Primitive (σ ⇒ τ)) (sv : SVal Γ σ) dsv →
    ρ D dρ ⊢ dprimapp p sv dsv ↓ deval-primitive p (eval sv ρ) (deval dsv ρ dρ)
  dapp : ∀ {hasIdx} {n : Idx hasIdx}
    {Γ′ σ τ ρ′ dρ′}
    {dvs} {vt} {dvt}
    {vtv} {dvtv}
    {dt : DTerm (σ • Γ′) τ} {dv} →
    ρ D dρ ⊢ dval dvs ↓ dclosure dt ρ′ dρ′ →
    ρ ⊢ val vt ↓[ n ] vtv →
    ρ D dρ ⊢ dval dvt ↓ dvtv →
    (vtv • ρ′) D (dvtv • dρ′) ⊢ dt ↓ dv →
    ρ D dρ ⊢ dapp dvs vt dvt ↓ dv
  dlett : ∀ {hasIdx} {n : Idx hasIdx}
    {σ τ} {s : Term Γ σ} {ds} {dt : DTerm (σ • Γ) τ}
    {vsv dvsv dv} →
    ρ ⊢ s ↓[ n ] vsv →
    ρ D dρ ⊢ ds ↓ dvsv →
    (vsv • ρ) D (dvsv • dρ) ⊢ dt ↓ dv →
    ρ D dρ ⊢ dlett s ds dt ↓ dv
  bangapp : ∀ {hasIdx1 hasIdx2}
    {n1 : Idx hasIdx1}
    {n2 : Idx hasIdx2}
    {Γ′ σ τ ρ′}
    {dvs} {vt} {dvt}
    {vtv1 dvtv}
    {t : Term (σ • Γ′) τ} {v2} →
    ρ D dρ ⊢ dval dvs ↓ bang (closure t ρ′) →
    ρ ⊢ val vt ↓[ n1 ] vtv1 →
    ρ D dρ ⊢ dval dvt ↓ dvtv →
    (vtv1 ⊕ dvtv • ρ′) ⊢ t ↓[ n2 ] v2 →
    ρ D dρ ⊢ dapp dvs vt dvt ↓ bang v2

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-# OPTIONS --cubical --safe #-}

module Cubical.Foundations.FunExtEquiv where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

-- Function extensionality is an equivalence.
module _ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {f g : (x : A) → B x} where
  private
    appl : f ≡ g → ∀ x → f x ≡ g x
    appl eq x i = eq i x

    fib : (p : f ≡ g) → fiber (funExt {B = B}) p
    fib p = (appl p , refl)

    funExt-fiber-isContr
      : (p : f ≡ g)
      → (fi : fiber (funExt {B = B}) p)
      → fib p ≡ fi
    funExt-fiber-isContr p (h , eq) i = (appl (eq (~ i)) , λ j → eq (~ i ∨ j))

  funExt-isEquiv : isEquiv (funExt {B = B})
  equiv-proof funExt-isEquiv p = (fib p , funExt-fiber-isContr p)

  funExtEquiv : (∀ x → f x ≡ g x) ≃ (f ≡ g)
  funExtEquiv = (funExt {B = B} , funExt-isEquiv)

  funExtPath : (∀ x → f x ≡ g x) ≡ (f ≡ g)
  funExtPath = ua funExtEquiv

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sums (disjoint unions)
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Sum where

open import Function
open import Data.Unit.Base using (⊤; tt)
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Level
open import Agda.Builtin.Equality

------------------------------------------------------------------------
-- Re-export content from base module

open import Data.Sum.Base public

------------------------------------------------------------------------
-- Additional functions

module _ {a b} {A : Set a} {B : Set b} where

  isInj₁ : A ⊎ B → Maybe A
  isInj₁ (inj₁ x) = just x
  isInj₁ (inj₂ y) = nothing

  isInj₂ : A ⊎ B → Maybe B
  isInj₂ (inj₁ x) = nothing
  isInj₂ (inj₂ y) = just y

  From-inj₁ : A ⊎ B → Set a
  From-inj₁ (inj₁ _) = A
  From-inj₁ (inj₂ _) = Lift a ⊤

  from-inj₁ : (x : A ⊎ B) → From-inj₁ x
  from-inj₁ (inj₁ x) = x
  from-inj₁ (inj₂ _) = _

  From-inj₂ : A ⊎ B → Set b
  From-inj₂ (inj₁ _) = Lift b ⊤
  From-inj₂ (inj₂ _) = B

  from-inj₂ : (x : A ⊎ B) → From-inj₂ x
  from-inj₂ (inj₁ _) = _
  from-inj₂ (inj₂ x) = x


text:
open import Agda.Primitive
open import Data.List
-- f1 : {l : Level} -> (a : Set l) -> (x : a) -> (y : x) -> x
-- f1 : (a : Set2) -> (x : a) -> (y : x) -> x
-- f1 a x y = ?

f0 : (a : Set) -> (x : a) -> a
f0 a x = x

f1 : (a : Set1) -> (x : a) -> a
f1 a x = x

myprod : (As : List Set) -> Set
myprod = {!!}

mysum : (As : List Set) -> Set
mysum = {!!}

hej : (tyOp : List Set -> Set) -> Set
hej = {!!}

test1 = hej myprod
test2 = hej mysum

Type = Set

data Dummy : Set where Dum : Dummy

-- Start of example

hej2 : List Type -> Type     -- Is universe-monomorphic in Agda, but polymorphic in Idris
hej2 (t ∷ ts) = t
hej2 _ = ?

test21 : Type
test21 = hej2 [ Type ]  -- test21 == Type in Idris, but Agda complains

test22 : Type
test22 = hej2 [ Dummy ]   -- test22 == Dummy

max_stars_repo_name: hjorthjort/IdrisToAgda

max_issues_repo_name: hjorthjort/IdrisToAgda

max_forks_repo_name: hjorthjort/IdrisToAgda


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.List hiding ( [_] )
open import finiteSet

module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where

-- open import nfa
open import Data.Nat
-- open import Data.Nat hiding ( _<_ ; _>_ )
-- open import Data.Fin hiding ( _<_ )
open import finiteSetUtil
open import automaton
open import logic
open import regex
open FiniteSet

-- whether a regex accepts empty input
--
empty? : Regex  Σ → Bool
empty?  ε       = true
empty?  φ       = false
empty? (x *)    = true
empty? (x & y)  = empty? x /\ empty? y
empty? (x || y) = empty? x \/ empty? y
empty? < x >    = false

derivative :  Regex  Σ → Σ → Regex  Σ
derivative ε s = φ
derivative φ s = φ
derivative (x *) s with derivative x s
... | ε = x *
... | φ = φ
... | t = t & (x *)
derivative (x & y) s with empty? x
... | true with derivative x s | derivative y s
... | ε | φ = φ
... | ε | t = y || t
... | φ | t = t
... | x1 | φ = x1 & y
... | x1 | y1 = (x1 & y) || y1
derivative (x & y) s | false with derivative x s
... | ε = y
... | φ = φ
... | t = t & y
derivative (x || y) s with derivative x s | derivative y s
... | φ | y1 = y1
... | x1 | φ = x1
... | x1 | y1 = x1 || y1
derivative < x > s with eq? x s
... | yes _ = ε
... | no  _ = φ

data regex-states (x : Regex  Σ ) : Regex  Σ → Set where
    unit   : regex-states x x
    derive : { y : Regex  Σ } → regex-states x y → (s : Σ)  → regex-states x ( derivative y s )

record Derivative (x : Regex  Σ ) : Set where
    field
       state : Regex  Σ
       is-derived : regex-states x state

open Derivative

open import Data.Fin hiding (_<_)

-- derivative generates   (x & y) || ... form. y and x part is a substerm of original regex
-- since subterm is finite, only finite number of state is generated for each operator
-- this does not work, becuase it depends on input sequences
-- finite-derivative : (r : Regex  Σ) → FiniteSet Σ  → FiniteSet (Derivative r)
-- order : Regex  Σ → ℕ
-- decline-derive : (x : Regex Σ ) (i : Σ ) → 0 < order x → order (derivative x i) < order x
--    is not so easy
-- in case of automaton, number of derivative is limited by iteration of input length, so it is finite.
-- so we cannot say derived automaton is finite i.e. regex-match is regular language now

regex→automaton : (r : Regex   Σ) → Automaton (Derivative r) Σ
regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive-step d s} ; aend = λ d → empty? (state d) }  where
    derive-step : (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s)
    derive-step d0 s = derive (is-derived d0) s

regex-match : (r : Regex   Σ) →  (List Σ) → Bool
regex-match ex is = accept ( regex→automaton ex ) record { state =  ex ; is-derived = unit } is

open import Relation.Binary.Definitions

cmp-regex : (x y : Regex Σ) → Dec ( x ≡ y )
cmp-regex ε ε = yes refl
cmp-regex ε φ = no (λ ())
cmp-regex ε (y *) = no (λ ())
cmp-regex ε (y & y₁) = no (λ ())
cmp-regex ε (y || y₁) = no (λ ())
cmp-regex ε < x > = no (λ ())
cmp-regex φ ε = no (λ ())
cmp-regex φ φ = yes refl
cmp-regex φ (y *) =  no (λ ())
cmp-regex φ (y & y₁) =  no (λ ())
cmp-regex φ (y || y₁) =  no (λ ())
cmp-regex φ < x > =  no (λ ())
cmp-regex (x *) ε =  no (λ ())
cmp-regex (x *) φ =  no (λ ())
cmp-regex (x *) (y *) with cmp-regex x y
... | yes refl = yes refl
... | no ne = no (λ x → ne (cmp1 x)) where
   cmp1 : (x *) ≡ (y *) → x ≡ y
   cmp1 refl = refl
cmp-regex (x *) (y & y₁) = no (λ ())
cmp-regex (x *) (y || y₁) = no (λ ())
cmp-regex (x *) < x₁ > = no (λ ())
cmp-regex (x & x₁) ε = no (λ ())
cmp-regex (x & x₁) φ = no (λ ())
cmp-regex (x & x₁) (y *) = no (λ ())
cmp-regex (x & x₁) (y & y₁) with cmp-regex x y | cmp-regex x₁ y₁
... | yes refl | yes refl = yes refl
... | no ne | _ = no (λ x → ne (cmp1 x)) where
   cmp1 :  x & x₁ ≡ y & y₁ → x ≡ y
   cmp1 refl = refl
... | _ | no ne  = no (λ x → ne (cmp1 x)) where
   cmp1 :  x & x₁ ≡ y & y₁ → x₁ ≡ y₁
   cmp1 refl = refl
cmp-regex (x & x₁) (y || y₁) = no (λ ())
cmp-regex (x & x₁) < x₂ > = no (λ ())
cmp-regex (x || x₁) ε = no (λ ())
cmp-regex (x || x₁) φ = no (λ ())
cmp-regex (x || x₁) (y *) = no (λ ())
cmp-regex (x || x₁) (y & y₁) = no (λ ())
cmp-regex (x || x₁) (y || y₁) with cmp-regex x y | cmp-regex x₁ y₁
... | yes refl | yes refl = yes refl
... | no ne | _ = no (λ x → ne (cmp1 x)) where
   cmp1 :  x || x₁ ≡ y || y₁ → x ≡ y
   cmp1 refl = refl
... | _ | no ne  = no (λ x → ne (cmp1 x)) where
   cmp1 :  x || x₁ ≡ y || y₁ → x₁ ≡ y₁
   cmp1 refl = refl
cmp-regex (x || x₁) < x₂ > = no (λ ())
cmp-regex < x > ε = no (λ ())
cmp-regex < x > φ = no (λ ())
cmp-regex < x > (y *) = no (λ ())
cmp-regex < x > (y & y₁) = no (λ ())
cmp-regex < x > (y || y₁) = no (λ ())
cmp-regex < x > < x₁ > with equal? fin x x₁ | inspect ( equal? fin x ) x₁
... | false | record { eq = eq } = no (λ x → ¬-bool eq (cmp1 x)) where
   cmp1 :  < x > ≡ < x₁ > →  equal? fin x x₁ ≡ true
   cmp1 refl = equal?-refl fin
... | true | record { eq = eq } with equal→refl fin eq
... | refl = yes refl

insert : List (Regex Σ) → (Regex Σ) → List (Regex Σ)
insert [] k = k ∷ []
insert (x ∷ t) k with cmp-regex k x
... | no n = x ∷ (insert t k)
... | yes y = x ∷ t

regex-derive : List (Regex Σ) → List (Regex Σ)
regex-derive t = regex-derive0 t t where
   regex-derive1 : Regex Σ → List Σ → List (Regex Σ) → List (Regex Σ)
   regex-derive1 x [] t = t
   regex-derive1 x (i ∷ t) r =  regex-derive1 x t (insert r (derivative x i))
   regex-derive0 :  List (Regex Σ)  → List (Regex Σ) → List (Regex Σ)
   regex-derive0 [] t = t
   regex-derive0 (x ∷ r) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true)) t)

--
-- if (Derivative r is finite,  regex→automaton is finite
--
drive-is-finite : (r : Regex   Σ) → FiniteSet (Derivative r)
drive-is-finite ε = {!!}
drive-is-finite φ = {!!}
drive-is-finite (r *) = {!!} where
   d1 :  FiniteSet (Derivative r )
   d1 = drive-is-finite r
drive-is-finite (r & r₁) = {!!}
drive-is-finite (r || r₁) = {!!}
drive-is-finite < x > = {!!}

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
-- Insertion sort

{-# OPTIONS --without-K --safe #-}

module Algorithms.List.Sort.Insertion where

-- agda-stdlib
open import Data.Bool hiding (_≤_; _≤?_; _<_)
open import Data.List
import      Data.Nat as ℕ
open import Relation.Binary as B
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary

module InsertionSortOperation
  {a r} {A : Set a} {_≤_ : Rel A r} (_≤?_ : B.Decidable _≤_)
  where

-- swap : A x A → A × A
-- swap ∘ swap ≡ id
-- ifTrueSwap : Bool → A × A → A × A
-- ifTrueSwap x ∘ ifTrueSwap y ≡ ifTrueSwap (xor x y)
-- x : A → A ≡ Unit ⊎ (Σ A (λ y → x ≢ y))

  insert : A → List A → List A
  insert x []           = [ x ]
  insert x (y ∷ ys) with x ≤? y
  ... | true  because _ = x ∷ y ∷ ys
  ... | false because _ = y ∷ insert x ys

  -- | Insertion sort
  sort : List A → List A
  sort = foldr insert []

private
  open InsertionSortOperation ℕ._≤?_

  _ : sort (5 ∷ 2 ∷ 4 ∷ 3 ∷ 1 ∷ []) ≡ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []
  _ = refl


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.Sets where

-- Category of (Agda) Sets, aka (types, functions, pointwise equality with implicit value)
-- Note the (explicit) levels in each

open import Level
open import Relation.Binary
open import Function using (_∘′_) renaming (id to idf)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open import Categories.Category

Sets : ∀ o → Category (suc o) o o
Sets o = record
  { Obj       = Set o
  ; _⇒_       = λ c d → c → d
  ; _≈_       = λ f g → ∀ {x} → f x ≡ g x
  ; id        = idf
  ; _∘_       = _∘′_
  ; assoc     = ≡.refl
  ; sym-assoc = ≡.refl
  ; identityˡ = ≡.refl
  ; identityʳ = ≡.refl
  ; identity² = ≡.refl
  ; equiv     = record
    { refl  = ≡.refl
    ; sym   = λ eq → ≡.sym eq
    ; trans = λ eq₁ eq₂ → ≡.trans eq₁ eq₂
    }
  ; ∘-resp-≈  = resp
  }
  where resp : ∀ {A B C : Set o} {f h : B → C} {g i : A → B} →
                 ({x : B} → f x ≡ h x) →
                 ({x : A} → g x ≡ i x) → {x : A} → f (g x) ≡ h (i x)
        resp {h = h} eq₁ eq₂ = ≡.trans eq₁ (≡.cong h eq₂)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --cubical --safe --postfix-projections #-}

open import Prelude
open import Relation.Binary

module Data.RBTree {e} {E : Type e} {r₁ r₂} (totalOrder : TotalOrder E r₁ r₂) where

open import Relation.Binary.Construct.Bounded totalOrder

open TotalOrder totalOrder using (_≤?_)

data Colour : Type where
  red black : Colour

add-black : Colour → ℕ → ℕ
add-black red = λ n → n
add-black black = suc

private
  variable
    n : ℕ

data Tree (lb ub : [∙]) : ℕ → Type (e ℓ⊔ r₂) where
  leaf : lb [≤] ub → Tree lb ub n
  node : (x : E) → (c : Colour) → Tree lb [ x ] n → Tree [ x ] ub n → Tree lb ub (add-black c n)

private
  variable
    lb ub : [∙]

IsBlack : Tree lb ub n → Type
IsBlack (leaf x) = ⊤
IsBlack (node x red tr tr₁) = ⊥
IsBlack (node x black tr tr₁) = ⊤

Valid-rec : Tree lb ub n → Type
Valid-rec (leaf x) = ⊤
Valid-rec (node x red   xs ys) = IsBlack xs × IsBlack ys × Valid-rec xs × Valid-rec ys
Valid-rec (node x black xs ys) = Valid-rec xs × Valid-rec ys

Valid : Tree lb ub n → Type
Valid tr = IsBlack tr × Valid-rec tr

-- insertWithin : (x : E) →
--                (lb [≤] [ x ]) →
--                ([ x ] [≤] ub) →
--                (tr : Tree lb ub n) →
--                Valid-rec tr →
--                ∃ c Σ (Tree lb ub (add-black c n)) Valid-rec
-- insertWithin x lb≤x x≤ub (leaf _) val = red , node x red (leaf lb≤x) (leaf x≤ub) , tt , tt , tt , tt
-- insertWithin x lb≤x x≤ub (node y c ls rs) val with x ≤? y
-- insertWithin x lb≤x x≤ub (node y red   ls rs) val | inl x≤y with insertWithin x lb≤x x≤y ls (fst (snd (snd val)))
-- insertWithin x lb≤x x≤ub (node y red   ls rs) val | inl x≤y | red    , ls′ , val′ = black , node y black ls′ rs , val′ , snd (snd (snd val))
-- insertWithin x lb≤x x≤ub (node y red   ls rs) val | inl x≤y | black  , ls′ , val′ = {!{!!} , node y {!!} ls′ rs , {!!}!}
-- insertWithin x lb≤x x≤ub (node y black ls rs) val | inl x≤y with insertWithin x lb≤x x≤y ls (fst val)
-- insertWithin x lb≤x x≤ub (node y black ls rs) val | inl x≤y | res = {!!}
-- insertWithin x lb≤x x≤ub (node y c ls rs) val | inr y≤x = {!!}

-- -- insertWithin x lb≤x x≤ub (node y ls rs) with x ≤? y
-- -- insertWithin x lb≤x x≤ub (node y ls rs) | inl x≤y = node y (insertWithin x lb≤x x≤y ls) rs
-- -- insertWithin x lb≤x x≤ub (node y ls rs) | inr y≤x = node y ls (insertWithin x y≤x x≤ub rs)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --safe #-}

module Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyList where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat using (ℕ ; zero ; suc)

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Polynomials.UnivariateList.Base
open import Cubical.Algebra.Polynomials.UnivariateList.Properties

private
  variable
    ℓ : Level

open CommRingStr

module _ (R : CommRing ℓ) where

  open PolyMod R
  open PolyModTheory R

  UnivariatePolyList : CommRing ℓ
  fst UnivariatePolyList = Poly R
  0r (snd UnivariatePolyList) = 0P
  1r (snd UnivariatePolyList) = 1P
  _+_ (snd UnivariatePolyList) = _Poly+_
  _·_ (snd UnivariatePolyList) = _Poly*_
  - snd UnivariatePolyList = Poly-
  isCommRing (snd UnivariatePolyList) = makeIsCommRing isSetPoly
                                    Poly+Assoc Poly+Rid Poly+Inverses Poly+Comm
                                    Poly*Associative Poly*Rid Poly*LDistrPoly+ Poly*Commutative

nUnivariatePolyList : (A' : CommRing ℓ) → (n : ℕ) → CommRing ℓ
nUnivariatePolyList A' zero = A'
nUnivariatePolyList A' (suc n) = UnivariatePolyList (nUnivariatePolyList A' n)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module SizedPolyIO.IOObject where

open import Data.Product

open import Level using (_⊔_) renaming (suc to lsuc)
open import Size

open import SizedPolyIO.Base
open import SizedPolyIO.Object

-- An IO object is like a simple object,
-- but the method returns IO applied to the result type of a simple object
-- which means the method returns an IO program which when terminating
-- returns the result of the simple object

module _  {γ ρ}  (ioi  : IOInterface γ ρ)  (let C  = Command ioi)  (let R   = Response ioi)
          {μ σ}  (oi   : Interface μ σ)   (let M  = Method oi)    (let Rt  = Result oi)
  where

  record IOObject (i : Size) : Set (ρ ⊔ γ ⊔ μ ⊔ σ) where
    coinductive
    field
      method : ∀{j : Size< i} (m : M) → IO ioi ∞ (Rt m × IOObject j)

open IOObject public

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Relator.Category where

open import Data
open import Data.Tuple
import      Lvl
open import Structure.Categorical.Properties
open import Structure.Category
open import Structure.Operator
open import Type

private variable ℓ : Lvl.Level

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Prelude.IO where

open import Prelude.Function
open import Prelude.Functor
open import Prelude.Applicative
open import Prelude.Monad
open import Prelude.List
open import Prelude.String
open import Prelude.Char
open import Prelude.Unit
open import Prelude.Show
open import Prelude.Nat

open import Agda.Builtin.IO public

postulate
  ioReturn : ∀ {a} {A : Set a} → A → IO A
  ioBind   : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B

{-# COMPILE GHC ioReturn = (\ _ _ -> return)    #-}
{-# COMPILE GHC ioBind =   (\ _ _ _ _ -> (>>=)) #-}

{-# COMPILE UHC ioReturn = (\ _ _ x -> UHC.Agda.Builtins.primReturn x) #-}
{-# COMPILE UHC ioBind =   (\ _ _ _ _ x y -> UHC.Agda.Builtins.primBind x y) #-}

ioMap : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → IO A → IO B
ioMap f m = ioBind m λ x → ioReturn (f x)

instance
  FunctorIO : ∀ {a} → Functor {a} IO
  fmap {{FunctorIO}} = ioMap

  ApplicativeIO : ∀ {a} → Applicative {a} IO
  pure {{ApplicativeIO}} = ioReturn
  _<*>_ {{ApplicativeIO}} = monadAp ioBind

  MonadIO : ∀ {a} → Monad {a} IO
  _>>=_ {{MonadIO}} = ioBind

  FunctorIO′ : ∀ {a b} → Functor′ {a} {b} IO
  fmap′ {{FunctorIO′}} = ioMap

  ApplicativeIO′ : ∀ {a b} → Applicative′ {a} {b} IO
  _<*>′_ {{ApplicativeIO′}} = monadAp′ ioBind

  MonadIO′ : ∀ {a b} → Monad′ {a} {b} IO
  _>>=′_ {{MonadIO′}} = ioBind

--- Terminal IO ---

postulate
  getChar  : IO Char
  putChar  : Char → IO Unit
  putStr   : String → IO Unit
  putStrLn : String → IO Unit

{-# FOREIGN GHC import qualified Data.Text    as Text #-}
{-# FOREIGN GHC import qualified Data.Text.IO as Text #-}

{-# COMPILE GHC getChar =  getChar   #-}
{-# COMPILE GHC putChar =  putChar   #-}
{-# COMPILE GHC putStr =   Text.putStr   #-}
{-# COMPILE GHC putStrLn = Text.putStrLn #-}

{-# COMPILE UHC putStr =   (UHC.Agda.Builtins.primPutStr) #-}
{-# COMPILE UHC putStrLn = (UHC.Agda.Builtins.primPutStrLn) #-}

print : ∀ {a} {A : Set a} {{ShowA : Show A}} → A → IO Unit
print = putStrLn ∘ show

--- Command line arguments ---

{-# FOREIGN GHC import System.Environment (getArgs, getProgName) #-}

postulate
  getArgs : IO (List String)
  getProgName : IO String

{-# COMPILE GHC getArgs =     fmap (map Text.pack) getArgs #-}
{-# COMPILE GHC getProgName = fmap Text.pack getProgName   #-}

--- Misc ---

{-# FOREIGN GHC import System.Exit #-}

data ExitCode : Set where
  Success : ExitCode
  -- TODO we probably should also enforce an upper limit?
  Failure : (n : Nat) → {p : NonZero n} → ExitCode

private
  {-# FOREIGN GHC exitWith' x = exitWith (if x == 0 then ExitSuccess else ExitFailure $ fromInteger x) #-}

  postulate
    exitWith' : ∀ {a} {A : Set a} → Nat → IO A
  {-# COMPILE GHC exitWith' = \ _ _ -> exitWith' #-}

exitWith : ∀ {a} {A : Set a} → ExitCode → IO A
exitWith Success = exitWith' 0
exitWith (Failure i) = exitWith' i

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
------------------------------------------------------------------------
-- The two methods used to specify the grammars are (language)
-- equivalent (for acyclic graphs)
------------------------------------------------------------------------

open import Mixfix.Expr
open import Mixfix.Acyclic.PrecedenceGraph
  using (acyclic; precedence)

module Mixfix.Equivalence
  (g : PrecedenceGraphInterface.PrecedenceGraph acyclic)
  where

open import Function using (_∘_)
open import Data.List using (List; []; _∷_)
open import Data.List.NonEmpty using (_∷_)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Product
open import Data.Vec using (Vec; []; _∷_)

open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics
open import TotalParserCombinators.Semantics.Continuation as ContSem
import StructurallyRecursiveDescentParsing.Simplified as Simplified
import StructurallyRecursiveDescentParsing.Simplified.Semantics as SSem

open import Mixfix.Fixity
open import Mixfix.Operator
import Mixfix.Acyclic.Grammar
import Mixfix.Cyclic.Grammar
import Mixfix.Acyclic.Lemma
private
  module Acyclic = Mixfix.Acyclic.Grammar        g
  module ALemma  = Mixfix.Acyclic.Lemma          g
  module Cyclic  = Mixfix.Cyclic.Grammar acyclic g
open import Mixfix.Acyclic.Lib as ALib
open ALib.Semantics-⊕ renaming (_⊕_∈⟦_⟧·_ to _⊕_∈⟦_⟧A·_)
open import Mixfix.Cyclic.Lib as CLib renaming (⟦_⟧ to ⟦_⟧C)
open CLib.Semantics-⊕ renaming (_⊕_∈⟦_⟧·_ to _⊕_∈⟦_⟧C·_)

open PrecedenceCorrect acyclic g

⟦_⟧A : ∀ {R} → ALib.ParserProg R → Parser NamePart R []
⟦ p ⟧A = Simplified.⟦_⟧ (ALib.⟦_⟧ p)

module AcyclicToCyclic where

  mutual

    precs : ∀ ps {s s′ e} →
            e ⊕ s′ ∈⟦ Acyclic.precs ps ⟧A· s →
            e ⊕ s′ ∈⟦  Cyclic.precs ps ⟧C· s
    precs []       ()
    precs (p ∷ ps) (∣ˡ (<$> e∈p))  = ∣ˡ (<$> prec  p  e∈p)
    precs (p ∷ ps) (∣ʳ (<$> e∈ps)) = ∣ʳ (<$> precs ps e∈ps)

    prec : ∀ p {s s′ e} →
           e ⊕ s′ ∈⟦ Acyclic.prec p ⟧A· s →
           e ⊕ s′ ∈⟦  Cyclic.prec p ⟧C· s
    prec (precedence ops sucs) e∈ = prec′ e∈
      where
      p = precedence ops sucs

      module A = Acyclic.Prec ops sucs
      module C =  Cyclic.Prec p

      preRight : ∀ {s s′ f} →
                 f ⊕ s′ ∈⟦ A.preRight ⟧A· s →
                 f ⊕ s′ ∈⟦ C.preRight ⟧C· s
      preRight (∣ˡ (<$>      i∈)) = ∣ˡ (<$>              inner _ i∈)
      preRight (∣ʳ (<$> ↑∈ ⊛ i∈)) = ∣ʳ (<$> precs _ ↑∈ ⊛ inner _ i∈)

      preRight⁺ : ∀ {s s′ s″ fs e} →
                 fs          ⊕ s′ ∈⟦ A.preRight +       ⟧A· s  →
                 e           ⊕ s″ ∈⟦ Acyclic.precs sucs ⟧A· s′ →
                 A.appʳ fs e ⊕ s″ ∈⟦ C.preRight⁺        ⟧C· s
      preRight⁺ {fs = _ ∷ ._} (+-[] f∈)     ↑∈ = preRight f∈ ⊛∞ ∣ʳ (<$> precs _ ↑∈)
      preRight⁺ {fs = _ ∷ ._} (+-∷  f∈ fs∈) ↑∈ = preRight f∈ ⊛∞ ∣ˡ (<$> preRight⁺ fs∈ ↑∈)

      postLeft : ∀ {s s′ f} →
                 f ⊕ s′ ∈⟦ A.postLeft ⟧A· s →
                 f ⊕ s′ ∈⟦ C.postLeft ⟧C· s
      postLeft (∣ˡ (<$> i∈     )) = ∣ˡ (<$> inner _ i∈)
      postLeft (∣ʳ (<$> i∈ ⊛ ↑∈)) = ∣ʳ (<$> inner _ i∈ ⊛ precs _ ↑∈)

      postLeft⁺ : ∀ {s s′ s″ o fs} →
                  o                ⊕ s′ ∈⟦ similar <$> C.postLeft⁺
                                         ∣ tighter <$> C.p↑ ⟧C· s →
                  fs               ⊕ s″ ∈⟦ A.postLeft +       ⟧A· s′ →
                  ALemma.appˡ o fs ⊕ s″ ∈⟦ C.postLeft⁺        ⟧C· s
      postLeft⁺ {fs = _ ∷ ._} o∈ (+-[] f∈)     =                     <$> o∈ ⊛∞ postLeft f∈
      postLeft⁺ {fs = _ ∷ ._} o∈ (+-∷  f∈ fs∈) = postLeft⁺ (∣ˡ (<$> (<$> o∈ ⊛∞ postLeft f∈))) fs∈

      prec′ : ∀ {s s′ assoc} {e : ExprIn p assoc} →
              (-, e) ⊕ s′ ∈⟦ Acyclic.prec p ⟧A· s →
              (-, e) ⊕ s′ ∈⟦  Cyclic.prec p ⟧C· s
      prec′ (∥ˡ (<$> i∈))                      = ∥ˡ (<$> inner _ i∈)
      prec′ (∥ʳ (∥ˡ (<$> ↑₁∈ ⊛ i∈ ⊛ ↑₂∈)))     = ∥ʳ (∥ˡ (<$> precs _ ↑₁∈ ⊛ inner _ i∈ ⊛∞ precs _ ↑₂∈ ))
      prec′ (∥ʳ (∥ʳ (∥ˡ (<$> fs∈ ⊛ ↑∈))))      = ∥ʳ (∥ʳ (∥ˡ (preRight⁺ fs∈ ↑∈)))
      prec′ (∥ʳ (∥ʳ (∥ʳ (∥ˡ (<$> ↑∈ ⊛ fs∈))))) = ∥ʳ (∥ʳ (∥ʳ (∥ˡ (postLeft⁺ (∣ʳ (<$> precs _ ↑∈)) fs∈))))
      prec′ (∥ʳ (∥ʳ (∥ʳ (∥ʳ ()))))

    inner : ∀ {fix} (ops : List (∃ (Operator fix))) {s s′ i} →
            i ⊕ s′ ∈⟦ Acyclic.inner ops ⟧A· s →
            i ⊕ s′ ∈⟦  Cyclic.inner ops ⟧C· s
    inner []               ()
    inner ((_ , op) ∷ ops) (∣ˡ (<$> i∈)) = ∣ˡ (<$> inner′ _ i∈)
    inner ((_ , op) ∷ ops) (∣ʳ (<$> i∈)) = ∣ʳ (<$> inner ops i∈)

    inner′ : ∀ {arity} (ns : Vec NamePart (1 + arity)) {s s′ i} →
             i ⊕ s′ ∈⟦ Acyclic.expr between ns ⟧A· s →
             i ⊕ s′ ∈⟦  Cyclic.expr between ns ⟧C· s
    inner′ (n ∷ .[]) between-[]           = between-[]
    inner′ (n ∷ ns)  (between-∷ e∈g es∈g) =
      between-∷ (precs g e∈g) (inner′ ns es∈g)

module CyclicToAcyclic where

  mutual

    precs : ∀ ps {s s′ e} →
            e ⊕ s′ ∈⟦  Cyclic.precs ps ⟧C· s →
            e ⊕ s′ ∈⟦ Acyclic.precs ps ⟧A· s
    precs []       ()
    precs (p ∷ ps) (∣ˡ (<$> e∈p))  = ∣ˡ (<$> prec  p  e∈p)
    precs (p ∷ ps) (∣ʳ (<$> e∈ps)) = ∣ʳ (<$> precs ps e∈ps)

    prec : ∀ p {s s′ e} →
           e ⊕ s′ ∈⟦  Cyclic.prec p ⟧C· s →
           e ⊕ s′ ∈⟦ Acyclic.prec p ⟧A· s
    prec (precedence ops sucs) e∈ = prec′ e∈
      where
      p = precedence ops sucs

      module A = Acyclic.Prec ops sucs
      module C =  Cyclic.Prec p

      preRight : ∀ {s s′ f} →
                 f ⊕ s′ ∈⟦ C.preRight ⟧C· s →
                 f ⊕ s′ ∈⟦ A.preRight ⟧A· s
      preRight (∣ˡ (<$>      i∈)) = ∣ˡ (<$>              inner _ i∈)
      preRight (∣ʳ (<$> ↑∈ ⊛ i∈)) = ∣ʳ (<$> precs _ ↑∈ ⊛ inner _ i∈)

      preRight⁺ : ∀ {s s′ e} →
                  e ⊕ s′ ∈⟦ C.preRight⁺                    ⟧C· s →
                  e ⊕ s′ ∈⟦ A.appʳ <$> A.preRight + ⊛ A.p↑ ⟧A· s
      preRight⁺ (f∈ ⊛∞ ∣ˡ (<$> pre∈)) with preRight⁺ pre∈
      preRight⁺ (f∈ ⊛∞ ∣ˡ (<$> pre∈)) | <$> fs∈ ⊛ ↑∈ = <$> +-∷  (preRight f∈) fs∈ ⊛ ↑∈
      preRight⁺ (f∈ ⊛∞ ∣ʳ (<$> ↑∈)  ) =                <$> +-[] (preRight f∈)     ⊛ precs _ ↑∈

      postLeft : ∀ {s s′ f} →
                 f ⊕ s′ ∈⟦ C.postLeft ⟧C· s →
                 f ⊕ s′ ∈⟦ A.postLeft ⟧A· s
      postLeft (∣ˡ (<$> i∈     )) = ∣ˡ (<$> inner _ i∈)
      postLeft (∣ʳ (<$> i∈ ⊛ ↑∈)) = ∣ʳ (<$> inner _ i∈ ⊛ precs _ ↑∈)

      postLeft⁺ : ∀ {s s′ e} →
                  e ⊕ s′ ∈⟦ C.postLeft⁺                    ⟧C· s →
                  e ⊕ s′ ∈⟦ A.appˡ <$> A.p↑ ⊛ A.postLeft + ⟧A· s
      postLeft⁺ (<$> ∣ˡ (<$> post∈) ⊛∞ f∈) with postLeft⁺ post∈
      postLeft⁺ (<$> ∣ˡ (<$> post∈) ⊛∞ f∈)
        | _⊛_ {x = fs} (<$> ↑∈) fs∈ = AS.cast∈ (ALemma.appˡ-∷ʳ _ fs _) (
                                             <$>         ↑∈ ⊛ AS.+-∷ʳ fs∈ (postLeft f∈))
        where module AS = ALib.Semantics-⊕
      postLeft⁺ (<$> ∣ʳ (<$> ↑∈)    ⊛∞ f∈) = <$> precs _ ↑∈ ⊛    +-[]     (postLeft f∈)

      prec′ : ∀ {s s′ assoc} {e : ExprIn p assoc} →
              (-, e) ⊕ s′ ∈⟦  Cyclic.prec p ⟧C· s →
              (-, e) ⊕ s′ ∈⟦ Acyclic.prec p ⟧A· s
      prec′ (∥ˡ (<$> i∈))                   = ∥ˡ (<$> inner _ i∈)
      prec′ (∥ʳ (∥ˡ (<$> ↑₁∈ ⊛ i∈ ⊛∞ ↑₂∈))) = ∥ʳ (∥ˡ (<$> precs _ ↑₁∈ ⊛ inner _ i∈ ⊛ precs _ ↑₂∈ ))
      prec′ (∥ʳ (∥ʳ (∥ˡ pre∈)))             = ∥ʳ (∥ʳ (∥ˡ (preRight⁺ pre∈)))
      prec′ (∥ʳ (∥ʳ (∥ʳ (∥ˡ post∈))))       = ∥ʳ (∥ʳ (∥ʳ (∥ˡ (postLeft⁺ post∈))))
      prec′ (∥ʳ (∥ʳ (∥ʳ (∥ʳ ()))))

    inner : ∀ {fix} (ops : List (∃ (Operator fix))) {s s′ i} →
            i ⊕ s′ ∈⟦  Cyclic.inner ops ⟧C· s →
            i ⊕ s′ ∈⟦ Acyclic.inner ops ⟧A· s
    inner []               ()
    inner ((_ , op) ∷ ops) (∣ˡ (<$> i∈)) = ∣ˡ (<$> inner′ _ i∈)
    inner ((_ , op) ∷ ops) (∣ʳ (<$> i∈)) = ∣ʳ (<$> inner ops i∈)

    inner′ : ∀ {arity} (ns : Vec NamePart (1 + arity)) {s s′ i} →
             i ⊕ s′ ∈⟦  Cyclic.expr between ns ⟧C· s →
             i ⊕ s′ ∈⟦ Acyclic.expr between ns ⟧A· s
    inner′ (n ∷ .[]) between-[]           = between-[]
    inner′ (n ∷ ns)  (between-∷ e∈g es∈g) =
      between-∷ (precs g e∈g) (inner′ ns es∈g)

acyclicToCyclic
  : ∀ {e s} → e ∈ Simplified.⟦_⟧ Acyclic.expression · s →
              e ∈                 Cyclic.expression · s
acyclicToCyclic =
  ContSem.sound               ∘
  CLib.Semantics-⊕.sound      ∘
  AcyclicToCyclic.precs _     ∘
  ALib.Semantics-⊕.complete _ ∘
  SSem.⊕-complete             ∘
  SSem.complete _

cyclicToAcyclic
  : ∀ {e s} → e ∈                 Cyclic.expression · s →
              e ∈ Simplified.⟦_⟧ Acyclic.expression · s
cyclicToAcyclic =
  SSem.sound                  ∘
  SSem.⊕-sound                ∘
  ALib.Semantics-⊕.sound      ∘
  CyclicToAcyclic.precs _     ∘
  CLib.Semantics-⊕.complete _ ∘
  ContSem.complete

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------------
-- Testing the η-expansion
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module Eta3 where

postulate
  D  : Set
  P² : D → D → Set

data ∃ (A : D → Set) : Set where
  _,_ : (t : D) → A t → ∃ A

-- Because Agda η-reduces the equations, the internal representation
-- of P corresponds to the predicate
--
-- P xs = ∃ (P² xs)
--
-- We η-expand the definition of P before the translation to FOL.

P : D → Set
P xs = ∃ λ ys → P² xs ys
{-# ATP definition P #-}

postulate bar : ∀ {xs} → P xs → (∃ λ ys → P² xs ys)
{-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Cat where

open import Agda.Builtin.Equality

{- A category is very much like a graph. It has vertices
   named objects and vertices named arrows. Each arrow goes
   from an object to an object (possibly the same!). -}
record Cat (obj : Set) (arr : obj -> obj -> Set) : Set where
  constructor MkCat
  field
    {- For each object, there is an arrow called `id` which
       goes from the object to itself. -}
    id : {o : obj} -> arr o o

    {- Given an arrow `f` from object `a` to `b` and an arrow
       `g` from `b` to `c`. We can compose these arrow. The
       result is an arrow from `a` to `c`. -}
    compose : {a b c : obj} -> arr a b -> arr b c -> arr a c

    -- Here comes some properties of `id` and `compose`

    {- For any arrow `f`, compose id f = f -}
    neutralLeft  : {a b : obj} -> (f : arr a b) -> compose id f ≡ f

    {- For any arrow `f`, compose f id = f  -}
    neutralRight : {a b : obj} -> (f : arr a b) -> compose f id ≡ f

    {- For any arrows `f`, `g` and `h`,
        composing f with g, and then the result with h
       gives exatctly the same result as
        composing f with the result of the composition of g and h

       Which means, like string concatenation than we can commpose
       the way we preserve the order of each element in the sequence.
    -}
    associativity : {a b c d : obj} ->
                    (f : arr a b) -> (g : arr b c) -> (h : arr c d) ->
                    compose f (compose g h) ≡ compose (compose f g) h

open import Agda.Builtin.Nat

{- `LE n m` encode the property that `n ≤ m`
    i.e. `n` is less or equal to `m` -}
data LE : Nat -> Nat -> Set where
  LERefl : {n : Nat} -> LE n n
  LENext : {n m : Nat} -> LE n m -> LE n (suc m)

{- Taking naturals as objects and `LE` as arrows,
   this actually forms a category! -}
natPoset : Cat Nat LE
natPoset = ???


text:
-- Checks that UHC FFI calls using non-magic datatypes work
module UHC-FFI where

data Nat : Set where
  Zero : Nat
  Suc : Nat -> Nat
{-# COMPILED_DATA_UHC Nat UHC.Agda.Builtins.Nat Zero Suc #-}

{-# IMPORT_UHC Data.Char #-}

open import Common.IO
open import Common.Unit
open import Common.String
open import Common.Char

postulate toLower : Char -> Char
{-# COMPILED_UHC toLower Data.Char.toLower #-}

main : IO Unit
main = putStr (charToStr (toLower 'A'))


text:
-- modular arithmetic

module nat-mod where

open import eq
open import nat

infix 8 _≡_mod_

data _≡_mod_ : ℕ → ℕ → ℕ → Set where
  mod-refl : ∀ {n k} → n ≡ n mod k
  mod-add : ∀ {n m k} → n ≡ m mod k → n + k ≡ m mod k
  mod-symm : ∀ {n m k} → n ≡ m mod k → m ≡ n mod k

{-
mod-trans : ∀ {n m o k} → n ≡ m mod k → m ≡ o mod k → n ≡ o mod k
mod-trans{n}{.n}{o}{k} mod-refl p2 = {!!}
mod-trans}{m}{o}{k} (mod-add p1) p2 = {!!}
mod-trans{n}{m}{o}{k} (mod-symm p1) p2 = {!!}
-}

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module Generic.Function.FoldMono where

open import Generic.Core

CurryAll : ∀ {α β} {A : Set α} -> (A -> Set β) -> List A -> Set β -> Set β
CurryAll B  []      C = C
CurryAll B (x ∷ xs) C = B x -> CurryAll B xs C

curryAll : ∀ {α β} {A : Set α} {B : A -> Set β} {C xs}
         -> (All B xs -> C) -> CurryAll B xs C
curryAll {xs = []}     g = g tt
curryAll {xs = x ∷ xs} g = curryAll ∘ curry g

mutual
  Hyp : ∀ {ι β} {I : Set ι} -> (I -> Set β) -> (D : Desc I β) -> Set β
  Hyp C (var i)   = C i
  Hyp C (π i q D) = Hypᵇ i C D q
  Hyp C (D ⊛ E)   = Hyp C D × Hyp C E

  Hypᵇ : ∀ {α ι β γ q} {I : Set ι} i
       -> (I -> Set β) -> Binder α β γ i q I -> α ≤ℓ β -> Set β
  Hypᵇ i C (coerce (A , D)) q = Coerce′ q $ Pi i A λ x -> Hyp C (D x)

mutual
  Fold : ∀ {ι β} {I : Set ι} -> (I -> Set β) -> (D : Desc I β) -> Set β
  Fold C (var i)   = C i
  Fold C (π i q D) = Foldᵇ i C D q
  Fold C (D ⊛ E)   = Hyp C D -> Fold C E

  Foldᵇ : ∀ {α ι β γ q} {I : Set ι} i
        -> (I -> Set β) -> Binder α β γ i q I -> α ≤ℓ β -> Set β
  Foldᵇ i C (coerce (A , D)) q = Coerce′ q $ Pi i A λ x -> Fold C (D x)

module _ {ι β} {I : Set ι} {D₀ : Data (Desc I β)} (C : I -> Set β) where
  module _ (hs : All (Fold C) (consTypes D₀)) where
    {-# TERMINATING #-}
    mutual
      foldHyp : (D : Desc I β) -> ⟦ D ⟧ (μ D₀) -> Hyp C D
      foldHyp (var i)    d      = foldMono d
      foldHyp (π i q D)  f      = foldHypᵇ i D f
      foldHyp (D ⊛ E)   (x , y) = foldHyp D x , foldHyp E y

      foldHypᵇ : ∀ {α γ q q′} i
               -> (D : Binder α β γ i q′ I) -> ⟦ i / D ⟧ᵇ q (μ D₀) -> Hypᵇ i C D q
      foldHypᵇ {q = q} i (coerce (A , D)) f =
        coerce′ q $ lamPi i λ x -> foldHyp (D x) (appPi i (uncoerce′ q f) x)

      foldExtend : ∀ {j} -> (D : Desc I β) -> Fold C D -> Extend D (μ D₀) j -> C j
      foldExtend (var i)   z  lrefl  = z
      foldExtend (π i q D) h  p      = foldExtendᵇ i D h p
      foldExtend (D ⊛ E)   h (d , e) = foldExtend E (h (foldHyp D d)) e

      foldExtendᵇ : ∀ {α γ q q′ j} i
                  -> (D : Binder α β γ i q′ I) -> Foldᵇ i C D q -> Extendᵇ i D q (μ D₀) j -> C j
      foldExtendᵇ {q = q} i (coerce (A , D)) h p with p | inspectUncoerce′ q p
      ... | _ | (x , e) , refl = foldExtend (D x) (appPi i (uncoerce′ q h) x) e

      foldAny : ∀ {j} (Ds : List (Desc I β)) d a b ns
              -> All (Fold C) Ds -> Node D₀ (packData d a b Ds ns) j -> C j
      foldAny  []          d a b  tt       tt       ()
      foldAny (D ∷ [])     d a b (_ , ns) (h , tt)  e       = foldExtend D h e
      foldAny (D ∷ E ∷ Ds) d a b (_ , ns) (h , hs) (inj₁ e) = foldExtend D h e
      foldAny (D ∷ E ∷ Ds) d a b (_ , ns) (h , hs) (inj₂ r) = foldAny (E ∷ Ds) d a b ns hs r

      foldMono : ∀ {j} -> μ D₀ j -> C j
      foldMono (node e) = foldAny (consTypes D₀)
                                  (dataName  D₀)
                                  (parsTele  D₀)
                                  (indsTele  D₀)
                                  (consNames D₀)
                                   hs
                                   e

  curryFoldMono : ∀ {j} -> μ D₀ j -> CurryAll (Fold C) (consTypes D₀) (C j)
  curryFoldMono d = curryAll λ hs -> foldMono hs d

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
{-# OPTIONS --termination-depth=2 #-}
module plfa-code.Quantifiers where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import plfa-code.Isomorphism using (_≃_; extensionality)

∀-elim : ∀ {A : Set} {B : A → Set}
  → (L : ∀ (x : A) → B x)
  → (M : A)
    --------------------------
  → B M
∀-elim L M = L M

---------- practice ----------
∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
  (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
∀-distrib-× =
  record
  { to      = λ fₗ → ⟨ (λ a → proj₁ (fₗ a)) , (λ a → proj₂ (fₗ a)) ⟩
  ; from    = λ x a → ⟨ (proj₁ x a) , (proj₂ x a) ⟩
  ; from∘to = λ fₗ → refl
  ; to∘from = λ x  → refl
  }

⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} →
    (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x)  →  ∀ (x : A) → B x ⊎ C x
⊎∀-implies-∀⊎ (inj₁ f₁) a = inj₁ (f₁ a)
⊎∀-implies-∀⊎ (inj₂ f₂) a = inj₂ (f₂ a)

-- the converse doesn't hold. If we construct a function
-- '∀ (x : A) → B x', we could build a '∀ (x : A) → B x ⊎ C x',
-- but '∀ (x : A) → C x' maybe doesn't hold.

data Tri : Set where
  aa : Tri
  bb : Tri
  cc : Tri

postulate
  ∀-extensionality :
    ∀ {A : Set} {B : A → Set} (f g : ∀ (x : A) → B x)
    → (∀ (x : A) → (f x ≡ g x))
    → f ≡ g

∀-× : {B : Tri → Set} → (∀ (x : Tri) → B x) ≃ (B aa × B bb × B cc)
∀-× {B} =
  record
  { to      = to′
  ; from    = from′
  ; from∘to = λ f → ∀-extensionality (from′ ⟨ f aa , ⟨ f bb , f cc ⟩ ⟩) f
                                     λ{aa → refl; bb → refl; cc → refl}
  ; to∘from = λ xx → refl
  }
  where
  to′ : (∀ (x : Tri) → B x) → (B aa × B bb × B cc)
  to′ f = ⟨ f aa , ⟨ f bb , f cc ⟩ ⟩
  from′ : (B aa × B bb × B cc) → (∀ (x : Tri) → B x)
  from′ xx aa = proj₁ xx
  from′ xx bb = proj₁ (proj₂ xx)
  from′ xx cc = proj₂ (proj₂ xx)

-- every λ expression has different types , wtf
------------------------------

data Σ (A : Set) (B : A → Set) : Set where
  ⟨_,_⟩ : (x : A) → B x → Σ A B

Σ-syntax = Σ
infix 2 Σ-syntax
syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

record Σ′ (A : Set) (B : A → Set) : Set where
  field
    proj₁′ : A
    proj₂′ : B proj₁′

∃ : ∀ {A : Set} (B : A → Set) → Set
∃ {A} B = Σ A B

∃-syntax = ∃
syntax ∃-syntax (λ x → B) = ∃[ x ] B

∃-elim : ∀ {A : Set} {B : A → Set} {C : Set}
  → (∀ x → B x → C)
  → ∃[ x ] B x
    ---------------
  → C
∃-elim f ⟨ x , y ⟩ = f x y

∀∃-currying : ∀ {A : Set} {B : A → Set} {C : Set}
  → (∀ x → B x → C) ≃ (∃[ x ] B x → C)
∀∃-currying =
  record
  { to      = λ{ f → λ{ ⟨ x , y ⟩ → f x y }}
  ; from    = λ{ g → λ{ x → λ{ y → g ⟨ x , y ⟩ }}}
  ; from∘to = λ f → refl
  ; to∘from = λ g → extensionality (λ{ ⟨ x , y ⟩ → refl})
  }

---------- practice ----------
∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
  ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
∃-distrib-⊎ =
  record
  { to      = λ{ ⟨ a , inj₁ b ⟩ → inj₁ ⟨ a , b ⟩
               ; ⟨ a , inj₂ c ⟩ → inj₂ ⟨ a , c ⟩
               }
  ; from    = λ{ (inj₁ ⟨ a , b ⟩) → ⟨ a , inj₁ b ⟩
               ; (inj₂ ⟨ a , c ⟩) → ⟨ a , inj₂ c ⟩
               }
  ; from∘to = λ{ ⟨ a , inj₁ b ⟩ → refl
               ; ⟨ a , inj₂ c ⟩ → refl
               }
  ; to∘from = λ{ (inj₁ ⟨ a , b ⟩) → refl
               ; (inj₂ ⟨ a , c ⟩) → refl
               }
  }

∃×-implies-×∃ : ∀ {A : Set} {B C : A → Set} →
  ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
∃×-implies-×∃ ⟨ a , ⟨ b , c ⟩ ⟩ = ⟨ ⟨ a , b ⟩ , ⟨ a , c ⟩ ⟩

-- the converse doesn't hold, because the x in ∃[ x ] B x is maybe not
-- the same 'x' in ∃[ x ] C x

∃-⊎ : ∀ {B : Tri → Set} → ∃[ x ] B x ≃ B aa ⊎ B bb ⊎ B cc
∃-⊎ =
  record
  { to      = λ{ ⟨ aa , a ⟩ → inj₁ a
               ; ⟨ bb , b ⟩ → inj₂ (inj₁ b)
               ; ⟨ cc , c ⟩ → inj₂ (inj₂ c)
               }
  ; from    = λ{ (inj₁ a) → ⟨ aa , a ⟩
               ; (inj₂ (inj₁ b)) → ⟨ bb , b ⟩
               ; (inj₂ (inj₂ c)) → ⟨ cc , c ⟩
               }
  ; from∘to = λ{ ⟨ aa , a ⟩ → refl
               ; ⟨ bb , b ⟩ → refl
               ; ⟨ cc , c ⟩ → refl
               }
  ; to∘from = λ{ (inj₁ a) → refl
               ; (inj₂ (inj₁ b)) → refl
               ; (inj₂ (inj₂ c)) → refl
               }
  }

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

even-∃ : ∀ {n : ℕ} → even n → ∃[ m ] (    m * 2 ≡ n)
odd-∃  : ∀ {n : ℕ} →  odd n → ∃[ m ] (1 + m * 2 ≡ n)

even-∃ even-zero                       =  ⟨ zero  , refl ⟩
even-∃ (even-suc o) with odd-∃ o
...                    | ⟨ m , refl ⟩  =  ⟨ suc m , refl ⟩

odd-∃  (odd-suc e)  with even-∃ e
...                    | ⟨ m , refl ⟩  =  ⟨ m , refl ⟩

∃-even : ∀ {n : ℕ} → ∃[ m ] (    m * 2 ≡ n) → even n
∃-odd  : ∀ {n : ℕ} → ∃[ m ] (1 + m * 2 ≡ n) →  odd n

∃-even ⟨  zero , refl ⟩  =  even-zero
∃-even ⟨ suc m , refl ⟩  =  even-suc (∃-odd ⟨ m , refl ⟩)

∃-odd  ⟨     m , refl ⟩  =  odd-suc (∃-even ⟨ m , refl ⟩)

--------- practice ----------
open import Data.Nat.Properties using (+-identityʳ; +-suc; +-assoc)
open Eq using (cong; sym; trans)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_)

open import plfa-code.Reasoning-legacy

∃-even′ : ∀ {n : ℕ} → ∃[ m ] (    2 * m ≡ n) → even n
∃-odd′  : ∀ {n : ℕ} → ∃[ m ] (2 * m + 1 ≡ n) →  odd n

dbl≡2* : ∀ n → n + n ≡ 2 * n
dbl≡2* n = cong (n +_) (sym (+-identityʳ n))

∃-even′ ⟨ zero , refl ⟩ = even-zero
∃-even′ ⟨ suc m , refl ⟩
  rewrite +-identityʳ m | +-suc m m | dbl≡2* m
                  = even-suc (odd-suc (∃-even′ ⟨ m , refl ⟩))

∃-odd′ ⟨ m , refl ⟩ rewrite +-suc (2 * m) 0
                          | +-identityʳ m
                          | +-identityʳ (m + m)
                          | dbl≡2* m           = odd-suc (∃-even′ ⟨ m , refl ⟩)

-- it's more difficult far away ...

open Data.Nat using (_≤_; z≤n; s≤s)
open Data.Nat.Properties using (≤-pred)

∃+⇒≤ : ∀ (y z : ℕ) → ∃[ x ] (x + y ≡ z) → y ≤ z
∃+⇒≤ zero .(x + 0) ⟨ x , refl ⟩ = z≤n
∃+⇒≤ (suc y) .(x + suc y) ⟨ x , refl ⟩ rewrite +-suc x y
                                = s≤s (∃+⇒≤ y (x + y) ⟨ x , refl ⟩)

≤⇒∃+ : ∀ (y z : ℕ) → y ≤ z → ∃[ x ] (x + y ≡ z)
≤⇒∃+ zero z y≤z = ⟨ z , (+-identityʳ z) ⟩
≤⇒∃+ (suc y) (suc z) y≤z with ≤⇒∃+ y z (≤-pred y≤z)
...         | ⟨ x , x+y≡z ⟩ = ⟨ x , trans (+-suc x y) (cong suc x+y≡z) ⟩

-----------------------------

¬∃≃∀¬ : ∀ {A : Set} {B : A → Set}
  → (¬ ∃[ x ] B x) ≃ ∀ x → ¬ B x
¬∃≃∀¬ =
  record
    { to      = λ{ ¬∃xy x y → ¬∃xy ⟨ x , y ⟩ }
    ; from    = λ{ ∀¬xy ⟨ x , y ⟩ → ∀¬xy x y }
    ; from∘to = λ{ ¬∃xy → extensionality λ{ ⟨ x , y ⟩ → refl } }
    ; to∘from = λ{ ∀¬xy → refl }
    }

---------- practice ----------
∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
  → ∃[ x ] (¬ B x)
    --------------
  → ¬ (∀ x → B x)
∃¬-implies-¬∀ ⟨ a , ¬b ⟩ = λ a→b → ¬b (a→b a)
-- the converse doesn't hold. we couldn't get a instance
-- of A to construct ∃[ x ] (¬ B x)

open import plfa-code.Bin using (Bin; Can; One;
                                zero; can-one; x0_; x1_; nil; one;
                                from; to; can-to-n; can-tf-eq; from-to-const)
open Eq using (subst₂; cong₂)
open import Data.Empty using (⊥-elim)
open import Function using (_∘_)

one-assim : ∀ {b : Bin} → (x : One b) → (y : One b) → x ≡ y
one-assim one one = refl
one-assim (x0 x) (x0 y) = sym (cong x0_ (one-assim y x))
one-assim (x1 x) (x1 y) = sym (cong x1_ (one-assim y x))

can-assim : ∀ {b : Bin} → (x : Can b) → (y : Can b) → x ≡ y
can-assim zero zero = refl
can-assim zero (can-one (x0 ()))
can-assim (can-one (x0 ())) zero
can-assim (can-one one) (can-one one) = refl
can-assim (can-one (x0 x)) (can-one (x0 y)) = cong (can-one ∘ x0_) (one-assim x y)
can-assim (can-one (x1 x)) (can-one (x1 y)) = cong (can-one ∘ x1_) (one-assim x y)

∃-proj₁ : {A : Set} {B : A → Set} → ∃[ x ] B x → A
∃-proj₁ ⟨ x , _ ⟩ = x

∃≡ : ∀ {A : Set} {B : A → Set} (p₁ : ∃[ x ](B x)) (p₂ : ∃[ y ](B y))
  → ∃-proj₁ p₁ ≡ ∃-proj₁ p₂ → (∀ (x) → (b₁ : B x) → (b₂ : B x) → b₁ ≡ b₂)
  → p₁ ≡ p₂
∃≡ ⟨ x , bx ⟩ ⟨ .x , by ⟩ refl f = sym (cong (⟨_,_⟩ x) (f x by bx))

Bin-isomorphism : ℕ ≃ ∃[ x ](Can x)
Bin-isomorphism =
  record
  { to      = to′
  ; from    = from′
  ; from∘to = from-to-const
  ; to∘from = to∘from′
  }
  where
  to′ : ℕ → ∃[ x ](Can x)
  to′ n = ⟨ to n , can-to-n n ⟩
  from′ : ∃[ x ](Can x) → ℕ
  from′ ⟨ b , can-b ⟩ = from b
  to∘from′ : ∀ y → to′ (from′ y) ≡ y
  to∘from′ ⟨ b , can-b ⟩  = ∃≡ ⟨ to (from b) , can-to-n (from b) ⟩ ⟨ b , can-b ⟩ (can-tf-eq can-b) (λ x → can-assim {x})

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code


text:
{-
  This is mostly for convenience, when working with ideals
  (which are defined for general rings) in a commutative ring.
-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.Ideal where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset renaming ( _∈_ to _∈p_ ; _⊆_ to _⊆p_
                                                  ; subst-∈ to subst-∈p )

open import Cubical.Functions.Logic

open import Cubical.Data.Nat using (ℕ ; zero ; suc ; tt)
                             renaming ( --zero to ℕzero ; suc to ℕsuc
                                        _+_ to _+ℕ_ ; _·_ to _·ℕ_
                                      ; +-assoc to +ℕ-assoc ; +-comm to +ℕ-comm
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm)

open import Cubical.Data.FinData hiding (rec ; elim)
open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.Ideal renaming (IdealsIn to IdealsInRing)
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.RingSolver.ReflectionSolving

private
  variable
    ℓ : Level

IdealsIn : (R : CommRing ℓ) → Type _
IdealsIn R = IdealsInRing (CommRing→Ring R)

module _ (Ring@(R , str) : CommRing ℓ) where
  open CommRingStr str
  makeIdeal : (I : R → hProp ℓ)
              → (+-closed : {x y : R} → x ∈p I → y ∈p I → (x + y) ∈p I)
              → (0r-closed : 0r ∈p I)
              → (·-closedLeft : {x : R} → (r : R) → x ∈p I → r · x ∈p I)
              → IdealsIn (R , str)
  makeIdeal I +-closed 0r-closed ·-closedLeft = I ,
    (record
       { +-closed = +-closed
       ; -closed = λ x∈pI → subst-∈p I (useSolver _)
                             (·-closedLeft (- 1r) x∈pI)
       ; 0r-closed = 0r-closed
       ; ·-closedLeft = ·-closedLeft
       ; ·-closedRight = λ r x∈pI →
                       subst-∈p I
                             (·-comm r _)
                             (·-closedLeft r x∈pI)
       })
       where useSolver : (x : R) → - 1r · x ≡ - x
             useSolver = solve Ring

-- better?
module CommIdeal (R' : CommRing ℓ) where
 private R = fst R'
 open CommRingStr (snd R')
 open Sum (CommRing→Ring R')
 open CommRingTheory R'
 open RingTheory (CommRing→Ring R')

 record isCommIdeal (I : ℙ R) : Type ℓ where
  constructor
   makeIsCommIdeal
  field
   +Closed : ∀ {x y : R} → x ∈p I → y ∈p I → (x + y) ∈p I
   contains0 : 0r ∈p I
   ·Closed : ∀ {x : R} (r : R) → x ∈p I → r · x ∈p I

  ·RClosed :  ∀ {x : R} (r : R) → x ∈p I → x · r ∈p I
  ·RClosed r x∈pI = subst-∈p I (·-comm _ _) (·Closed r x∈pI)

 open isCommIdeal
 isPropIsCommIdeal : (I : ℙ R) → isProp (isCommIdeal I)
 +Closed (isPropIsCommIdeal I ici₁ ici₂ i) x∈pI y∈pI =
         I _ .snd (ici₁ .+Closed x∈pI y∈pI) (ici₂ .+Closed x∈pI y∈pI) i
 contains0 (isPropIsCommIdeal I ici₁ ici₂ i) = I 0r .snd (ici₁ .contains0) (ici₂ .contains0) i
 ·Closed (isPropIsCommIdeal I ici₁ ici₂ i) r x∈pI =
         I _ .snd (ici₁ .·Closed r x∈pI) (ici₂ .·Closed r x∈pI) i

 CommIdeal : Type (ℓ-suc ℓ)
 CommIdeal = Σ[ I ∈ ℙ R ] isCommIdeal I

 --inclusion and containment of ideals
 _⊆_ : CommIdeal → CommIdeal → Type ℓ
 I ⊆ J = I .fst ⊆p J .fst

 infix 5 _∈_
 _∈_ : R → CommIdeal → Type ℓ
 x ∈ I = x ∈p I .fst

 subst-∈ : (I : CommIdeal) {x y : R} → x ≡ y → x ∈ I → y ∈ I
 subst-∈ I = subst-∈p (I .fst)

 CommIdeal≡Char : {I J : CommIdeal} → I ⊆ J → J ⊆ I → I ≡ J
 CommIdeal≡Char I⊆J J⊆I = Σ≡Prop isPropIsCommIdeal (⊆-extensionality _ _ (I⊆J , J⊆I))

 ∑Closed : (I : CommIdeal) {n : ℕ} (V : FinVec R n)
         → (∀ i → V i ∈ I) → ∑ V ∈ I
 ∑Closed I {n = zero} _ _ = I .snd .contains0
 ∑Closed I {n = suc n} V h = I .snd .+Closed (h zero) (∑Closed I (V ∘ suc) (h ∘ suc))

 0Ideal : CommIdeal
 fst 0Ideal x = (x ≡ 0r) , is-set _ _
 +Closed (snd 0Ideal) x≡0 y≡0 = cong₂ (_+_) x≡0 y≡0 ∙ +Rid _
 contains0 (snd 0Ideal) = refl
 ·Closed (snd 0Ideal) r x≡0 = cong (r ·_) x≡0 ∙ 0RightAnnihilates _

 1Ideal : CommIdeal
 fst 1Ideal x = ⊤
 +Closed (snd 1Ideal) _ _ = lift tt
 contains0 (snd 1Ideal) = lift tt
 ·Closed (snd 1Ideal) _ _ = lift tt

 contains1Is1 : (I : CommIdeal) → 1r ∈ I → I ≡ 1Ideal
 contains1Is1 I 1∈I = CommIdeal≡Char (λ _ _ → lift tt)
   λ x _ → subst-∈ I (·Rid _) (I .snd .·Closed x 1∈I) -- x≡x·1 ∈ I

 _+i_ : CommIdeal → CommIdeal → CommIdeal
 fst (I +i J) x =
     (∃[ (y , z) ∈ (R × R) ] ((y ∈ I) × (z ∈ J) × (x ≡ y + z))) --have a record for this?
     , isPropPropTrunc
 +Closed (snd (I +i J)) {x = x₁} {y = x₂} = map2 +ClosedΣ
  where
  +ClosedΣ : Σ[ (y₁ , z₁) ∈ (R × R) ] ((y₁ ∈ I) × (z₁ ∈ J) × (x₁ ≡ y₁ + z₁))
           → Σ[ (y₂ , z₂) ∈ (R × R) ] ((y₂ ∈ I) × (z₂ ∈ J) × (x₂ ≡ y₂ + z₂))
           → Σ[ (y₃ , z₃) ∈ (R × R) ] ((y₃ ∈ I) × (z₃ ∈ J) × (x₁ + x₂ ≡ y₃ + z₃))
  +ClosedΣ ((y₁ , z₁) , y₁∈I , z₁∈J , x₁≡y₁+z₁) ((y₂ , z₂) , y₂∈I , z₂∈J , x₂≡y₂+z₂) =
    (y₁ + y₂ , z₁ + z₂) , +Closed (snd I) y₁∈I y₂∈I , +Closed (snd J) z₁∈J z₂∈J
                      , cong₂ (_+_) x₁≡y₁+z₁ x₂≡y₂+z₂ ∙ +ShufflePairs _ _ _ _
 contains0 (snd (I +i J)) = ∣ (0r , 0r) , contains0 (snd I) , contains0 (snd J) , sym (+Rid _) ∣
 ·Closed (snd (I +i J)) {x = x} r = map ·ClosedΣ
  where
  ·ClosedΣ : Σ[ (y₁ , z₁) ∈ (R × R) ] ((y₁ ∈ I) × (z₁ ∈ J) × (x ≡ y₁ + z₁))
           → Σ[ (y₂ , z₂) ∈ (R × R) ] ((y₂ ∈ I) × (z₂ ∈ J) × (r · x ≡ y₂ + z₂))
  ·ClosedΣ ((y₁ , z₁) , y₁∈I , z₁∈J , x≡y₁+z₁) =
    (r · y₁ , r · z₁) , ·Closed (snd I) r y₁∈I , ·Closed (snd J) r z₁∈J
                     , cong (r ·_) x≡y₁+z₁ ∙ ·Rdist+ _ _ _

 infixl 6 _+i_

 +iComm⊆ : ∀ (I J : CommIdeal) → (I +i J) ⊆ (J +i I)
 +iComm⊆ I J x = map λ ((y , z) , y∈I , z∈J , x≡y+z) → (z , y) , z∈J , y∈I , x≡y+z ∙ +Comm _ _

 +iComm : ∀ (I J : CommIdeal) → I +i J ≡ J +i I
 +iComm I J = CommIdeal≡Char (+iComm⊆ I J)  (+iComm⊆ J I)

 +iLidLIncl : ∀ (I : CommIdeal) → (0Ideal +i I) ⊆ I
 +iLidLIncl I x = rec (I .fst x .snd) λ ((y , z) , y≡0 , z∈I , x≡y+z)
                                 → subst-∈ I (sym (x≡y+z ∙∙ cong (_+ z) y≡0 ∙∙ +Lid z)) z∈I

 +iLidRIncl : ∀ (I : CommIdeal) → I ⊆ (0Ideal +i I)
 +iLidRIncl I x x∈I = ∣ (0r , x) , refl , x∈I , sym (+Lid _) ∣

 +iLid : ∀ (I : CommIdeal) → 0Ideal +i I ≡ I
 +iLid I = CommIdeal≡Char (+iLidLIncl I) (+iLidRIncl I)

 +iLincl : ∀ (I J : CommIdeal) → I ⊆ (I +i J)
 +iLincl I J x x∈I = ∣ (x , 0r) , x∈I , J .snd .contains0 , sym (+Rid x) ∣

 +iRincl : ∀ (I J : CommIdeal) → J ⊆ (I +i J)
 +iRincl I J x x∈J = ∣ (0r , x) , I .snd .contains0 , x∈J ,  sym (+Lid x) ∣

 +iRespLincl : ∀ (I J K : CommIdeal) → I ⊆ J → (I +i K) ⊆ (J +i K)
 +iRespLincl I J K I⊆J x = map λ ((y , z) , y∈I , z∈K , x≡y+z) → ((y , z) , I⊆J y y∈I , z∈K , x≡y+z)

 +iAssocLIncl : ∀ (I J K : CommIdeal) → (I +i (J +i K)) ⊆ ((I +i J) +i K)
 +iAssocLIncl I J K x = elim (λ _ → ((I +i J) +i K) .fst x .snd) (uncurry3
           λ (y , z) y∈I → elim (λ _ → isPropΠ λ _ → ((I +i J) +i K) .fst x .snd)
             λ ((u , v) , u∈J , v∈K , z≡u+v) x≡y+z
               → ∣ (y + u , v) , ∣ _ , y∈I , u∈J , refl ∣ , v∈K
                                , x≡y+z ∙∙ cong (y +_) z≡u+v ∙∙ +Assoc _ _ _ ∣)

 +iAssocRIncl : ∀ (I J K : CommIdeal) → ((I +i J) +i K) ⊆ (I +i (J +i K))
 +iAssocRIncl I J K x = elim (λ _ → (I +i (J +i K)) .fst x .snd) (uncurry3
           λ (y , z) → elim (λ _ → isPropΠ2 λ _ _ → (I +i (J +i K)) .fst x .snd)
             λ ((u , v) , u∈I , v∈J , y≡u+v) z∈K x≡y+z
               → ∣ (u , v + z) , u∈I , ∣ _ , v∈J , z∈K , refl ∣
                                      , x≡y+z ∙∙ cong (_+ z) y≡u+v ∙∙ sym (+Assoc _ _ _) ∣)

 +iAssoc : ∀ (I J K : CommIdeal) → I +i (J +i K) ≡ (I +i J) +i K
 +iAssoc I J K = CommIdeal≡Char (+iAssocLIncl I J K) (+iAssocRIncl I J K)

 +iIdemLIncl : ∀ (I : CommIdeal) → (I +i I) ⊆ I
 +iIdemLIncl I x = rec (I .fst x .snd) λ ((y , z) , y∈I , z∈I , x≡y+z)
                                 → subst-∈ I (sym x≡y+z) (I .snd .+Closed y∈I z∈I)

 +iIdemRIncl : ∀ (I : CommIdeal) → I ⊆ (I +i I)
 +iIdemRIncl I x x∈I = ∣ (0r , x) , I .snd .contains0 , x∈I , sym (+Lid _) ∣

 +iIdem : ∀ (I : CommIdeal) → I +i I ≡ I
 +iIdem I = CommIdeal≡Char (+iIdemLIncl I) (+iIdemRIncl I)

 -- where to put this?
 mul++dist : ∀ {n m : ℕ} (α U : FinVec R n) (β V : FinVec R m) (j : Fin (n +ℕ m))
            → ((λ i → α i · U i) ++Fin (λ i → β i · V i)) j ≡ (α ++Fin β) j · (U ++Fin V) j
 mul++dist {n = zero} α U β V j = refl
 mul++dist {n = suc n} α U β V zero = refl
 mul++dist {n = suc n} α U β V (suc j) = mul++dist (α ∘ suc) (U ∘ suc) β V j

 -- define multiplication of ideals
 _·i_ : CommIdeal → CommIdeal → CommIdeal
 fst (I ·i J) x = (∃[ n ∈ ℕ ] Σ[ (α , β) ∈ (FinVec R n × FinVec R n) ]
                   (∀ i → α i ∈ I) × (∀ i → β i ∈ J) × (x ≡ ∑ λ i → α i · β i))
                    , isPropPropTrunc
 +Closed (snd (I ·i J)) = map2
  λ (n , (α , β) , ∀αi∈I , ∀βi∈J , x≡∑αβ) (m , (γ , δ) , ∀γi∈I , ∀δi∈J , y≡∑γδ)
   → n +ℕ m , (α ++Fin γ , β ++Fin δ) , ++FinPres∈ (I .fst) ∀αi∈I ∀γi∈I
                                      , ++FinPres∈ (J .fst) ∀βi∈J ∀δi∈J
    , cong₂ (_+_) x≡∑αβ y≡∑γδ ∙∙ sym (∑Split++ (λ i → α i · β i) (λ i → γ i · δ i))
                              ∙∙ ∑Ext (mul++dist α β γ δ)
 contains0 (snd (I ·i J)) = ∣ 0 , ((λ ()) , (λ ())) , (λ ()) , (λ ()) , refl ∣
 ·Closed (snd (I ·i J)) r = map
  λ (n , (α , β) , ∀αi∈I , ∀βi∈J , x≡∑αβ)
   → n , ((λ i → r · α i) , β) , (λ i → I .snd .·Closed r (∀αi∈I i)) , ∀βi∈J
    , cong (r ·_) x≡∑αβ ∙ ∑Mulrdist r (λ i → α i · β i) ∙ ∑Ext λ i → ·Assoc r (α i) (β i)

 infixl 7 _·i_

 prodInProd : ∀ (I J : CommIdeal) (x y : R) → x ∈ I → y ∈ J → (x · y) ∈ (I ·i J)
 prodInProd _ _ x y x∈I y∈J =
            ∣ 1 , ((λ _ → x) , λ _ → y) , (λ _ → x∈I) , (λ _ → y∈J) , sym (+Rid _) ∣

 ·iLincl : ∀ (I J : CommIdeal) → (I ·i J) ⊆ I
 ·iLincl I J x = elim (λ _ → I .fst x .snd)
   λ (_ , (α , β) , α∈I , _ , x≡∑αβ) → subst-∈ I (sym x≡∑αβ)
                                     (∑Closed I (λ i → α i · β i) λ i → ·RClosed (I .snd) _ (α∈I i))

 ·iComm⊆ : ∀ (I J : CommIdeal) → (I ·i J) ⊆ (J ·i I)
 ·iComm⊆ I J x = map λ (n , (α , β) , ∀αi∈I , ∀βi∈J , x≡∑αβ)
                      → (n , (β , α) , ∀βi∈J , ∀αi∈I , x≡∑αβ ∙ ∑Ext (λ i → ·-comm (α i) (β i)))

 ·iComm : ∀ (I J : CommIdeal) → I ·i J ≡ J ·i I
 ·iComm I J = CommIdeal≡Char (·iComm⊆ I J) (·iComm⊆ J I)

 I⊆I1 : ∀ (I : CommIdeal) → I ⊆ (I ·i 1Ideal)
 I⊆I1 I x x∈I = ∣ 1 , ((λ _ → x) , λ _ → 1r) , (λ _ → x∈I) , (λ _ → lift tt) , useSolver x ∣
  where
  useSolver : ∀ x → x ≡ x · 1r + 0r
  useSolver = solve R'

 ·iRid : ∀ (I : CommIdeal) → I ·i 1Ideal ≡ I
 ·iRid I = CommIdeal≡Char (·iLincl I 1Ideal) (I⊆I1 I)

 -- a useful corollary
 ·iRContains1id : ∀ (I J : CommIdeal) → 1r ∈ J → I ·i J ≡ I
 ·iRContains1id I J 1∈J = cong (I ·i_) (contains1Is1 J 1∈J) ∙ ·iRid I

 ·iAssocLIncl : ∀ (I J K : CommIdeal) → (I ·i (J ·i K)) ⊆ ((I ·i J) ·i K)
 ·iAssocLIncl I J K x = rec isPropPropTrunc
         λ (_ , (α , β) , α∈I , β∈JK , x≡∑αβ)
             → subst-∈ ((I ·i J) ·i K) (sym x≡∑αβ)
               (∑Closed ((I ·i J) ·i K) (λ i → α i · β i)
         λ i → rec isPropPropTrunc
               (λ (_ , (γ , δ) , γ∈J , δ∈K , βi≡∑γδ)
                  → subst-∈ ((I ·i J) ·i K) -- each αᵢβᵢ ≡...≡ ∑αᵢγⱼδⱼ ∈IJK
                             (sym (cong (α i ·_) βi≡∑γδ ∙∙ ∑Mulrdist (α i) (λ j → γ j · δ j)
                                                        ∙∙ ∑Ext (λ j → ·Assoc (α i) (γ j) (δ j))))
                             (∑Closed ((I ·i J) ·i K) (λ j → α i · γ j · δ j) -- each αᵢγⱼδⱼ∈IJK
                                      λ j → prodInProd (I ·i J) K _ _
                                              (prodInProd I J _ _ (α∈I i) (γ∈J j)) (δ∈K j)))
               (β∈JK i))

 ·iAssocRIncl : ∀ (I J K : CommIdeal) → ((I ·i J) ·i K) ⊆ (I ·i (J ·i K))
 ·iAssocRIncl I J K x = rec isPropPropTrunc
         λ (_ , (α , β) , α∈IJ , β∈K , x≡∑αβ)
             → subst-∈ (I ·i (J ·i K)) (sym x≡∑αβ)
               (∑Closed (I ·i (J ·i K)) (λ i → α i · β i)
         λ i → rec isPropPropTrunc
               (λ (_ , (γ , δ) , γ∈I , δ∈J , αi≡∑γδ)
                  → subst-∈ (I ·i (J ·i K))
                             (sym (cong (_· β i) αi≡∑γδ ∙∙ ∑Mulldist (β i) (λ j → γ j · δ j)
                                        ∙∙ ∑Ext (λ j → sym (·Assoc (γ j) (δ j) (β i)))))
                             (∑Closed (I ·i (J ·i K)) (λ j → γ j · (δ j · β i))
                                      λ j → prodInProd I (J ·i K) _ _ (γ∈I j)
                                              (prodInProd J K _ _ (δ∈J j) (β∈K i))))
               (α∈IJ i))

 ·iAssoc : ∀ (I J K : CommIdeal) → I ·i (J ·i K) ≡ (I ·i J) ·i K
 ·iAssoc I J K = CommIdeal≡Char (·iAssocLIncl I J K) (·iAssocRIncl I J K)

 ·iRdist+iLIncl : ∀ (I J K : CommIdeal) → (I ·i (J +i K)) ⊆ (I ·i J +i I ·i K)
 ·iRdist+iLIncl I J K x = rec isPropPropTrunc
   λ (n , (α , β) , α∈I , β∈J+K , x≡∑αβ) → subst-∈ ((I ·i J) +i (I ·i K)) (sym x≡∑αβ)
     (∑Closed ((I ·i J) +i (I ·i K)) (λ i → α i · β i) -- each αi·βi ∈ IJ+IK
     λ i → rec isPropPropTrunc
           (λ ((γi , δi) , γi∈J , δi∈K , βi≡γi+δi) →
              ∣ (α i · γi , α i · δi) , prodInProd I J _ _ (α∈I i) γi∈J
                                      , prodInProd I K _ _ (α∈I i) δi∈K
                                      , cong (α i ·_) βi≡γi+δi ∙ ·Rdist+ _ _ _ ∣)
           (β∈J+K i))

 ·iRdist+iRIncl : ∀ (I J K : CommIdeal) → ((I ·i J) +i (I ·i K)) ⊆ (I ·i (J +i K))
 ·iRdist+iRIncl I J K x = rec isPropPropTrunc λ ((y , z) , y∈IJ , z∈IK , x≡y+z)
         → subst-∈ (I ·i (J +i K)) (sym x≡y+z)
             ((I ·i (J +i K)) .snd .+Closed (inclHelperLeft _ y∈IJ) (inclHelperRight _ z∈IK))
  where
  inclHelperLeft : (I ·i J) ⊆ (I ·i (J +i K))
  inclHelperLeft x' = map (λ (n , (α , β) , α∈I , β∈J , x'≡∑αβ)
                    → n , (α , β) , α∈I , (λ i → +iLincl J K _ (β∈J i)) , x'≡∑αβ)

  inclHelperRight : (I ·i K) ⊆ (I ·i (J +i K))
  inclHelperRight x' = map (λ (n , (α , β) , α∈I , β∈K , x'≡∑αβ)
                     → n , (α , β) , α∈I , (λ i → +iRincl J K _ (β∈K i)) , x'≡∑αβ)

 ·iRdist+i : ∀ (I J K : CommIdeal) → I ·i (J +i K) ≡ I ·i J +i I ·i K
 ·iRdist+i I J K = CommIdeal≡Char (·iRdist+iLIncl I J K) (·iRdist+iRIncl I J K)

 -- only one absorption law, i.e. CommIdeal , +i , ·i does not form a dist. lattice
 ·iAbsorb+iLIncl : ∀ (I J : CommIdeal) → (I +i (I ·i J)) ⊆ I
 ·iAbsorb+iLIncl I J x = rec (I .fst x .snd) λ ((y , z) , y∈I , z∈IJ , x≡y+z)
         → subst-∈ I (sym x≡y+z) (I .snd .+Closed y∈I (·iLincl I J _ z∈IJ))

 ·iAbsorb+iRIncl : ∀ (I J : CommIdeal) → I ⊆ (I +i (I ·i J))
 ·iAbsorb+iRIncl I J = +iLincl I (I ·i J)

 ·iAbsorb+i : ∀ (I J : CommIdeal) → I +i (I ·i J) ≡ I
 ·iAbsorb+i I J = CommIdeal≡Char (·iAbsorb+iLIncl I J) (·iAbsorb+iRIncl I J)

max_stars_repo_name: dolio/cubical

max_issues_repo_name: dolio/cubical

max_forks_repo_name: dolio/cubical


text:
------------------------------------------------------------------------
-- Convenient syntax for "equational reasoning" using a partial order
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.PartialOrderReasoning (p : Poset) where

open Poset p
import Relation.Binary.PreorderReasoning as PreR
open PreR preorder public renaming (_∼⟨_⟩_ to _≤⟨_⟩_)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category.Monoidal

-- Monoidal natural transformations between lax and strong monoidal functors.
--
-- See
--  * John Baez, Some definitions everyone should know,
--    https://math.ucr.edu/home/baez/qg-fall2004/definitions.pdf
--  * https://ncatlab.org/nlab/show/monoidal+natural+transformation

module Categories.NaturalTransformation.Monoidal where

open import Level
open import Data.Product using (_,_)

open import Categories.Category using (module Commutation)
open import Categories.Category.Product
import Categories.Category.Monoidal.Reasoning as MonoidalReasoning
open import Categories.Functor.Monoidal
open import Categories.Functor.Monoidal.Properties using ()
  renaming (∘-Monoidal to _∘Fˡ_; ∘-StrongMonoidal to _∘Fˢ_)
import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning as MorphismReasoning
open import Categories.NaturalTransformation as NT using (NaturalTransformation)

open NaturalTransformation renaming (η to _[_])

module Lax where

  module _ {o ℓ e o′ ℓ′ e′}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′}
           (F G : MonoidalFunctor C D) where

    private
      module C = MonoidalCategory C
      module D = MonoidalCategory D
      module F = MonoidalFunctor F renaming (F to U)
      module G = MonoidalFunctor G renaming (F to U)
    open D hiding (U; id)
    open Commutation D.U

    -- Monoidal natural transformations between lax monoidal functors.

    record IsMonoidalNaturalTransformation (β : NaturalTransformation F.U G.U)
           : Set (o ⊔ ℓ′ ⊔ e′) where
      field
        ε-compat      : [ unit ⇒ G.₀ C.unit  ]⟨
                          F.ε          ⇒⟨ F.₀ C.unit ⟩
                          β [ C.unit ]
                        ≈ G.ε
                        ⟩
        ⊗-homo-compat : ∀ {X Y} →
                        [ F.₀ X ⊗₀ F.₀ Y ⇒ G.₀ (X C.⊗₀ Y) ]⟨
                          F.⊗-homo [ (X , Y) ]  ⇒⟨ F.₀ (X C.⊗₀ Y) ⟩
                          β [ X C.⊗₀ Y ]
                        ≈ β [ X ] ⊗₁ β [ Y ]    ⇒⟨ G.₀ X ⊗₀ G.₀ Y ⟩
                          G.⊗-homo [ (X , Y) ]
                        ⟩

    record MonoidalNaturalTransformation : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
      field
        U          : NaturalTransformation F.U G.U
        isMonoidal : IsMonoidalNaturalTransformation U

      open NaturalTransformation           U          public
      open IsMonoidalNaturalTransformation isMonoidal public

  -- To shorten some definitions
  private _⇛_ = MonoidalNaturalTransformation

  -- Identity and compositions

  module _ {o ℓ e o′ ℓ′ e′}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′} where

    private
      module C = MonoidalCategory C
      module D = MonoidalCategory D
    open D hiding (U; id)
    open MorphismReasoning D.U
    open MonoidalReasoning D.monoidal

    infixr 9 _∘ᵥ_

    id : {F : MonoidalFunctor C D} → F ⇛ F
    id {F} = record
      { U               = NT.id
      ; isMonoidal      = record
        { ε-compat      = D.identityˡ
        ; ⊗-homo-compat = λ {X Y} → begin
            D.id ∘ ⊗-homo.η (X , Y)          ≈⟨ id-comm-sym ⟩
            ⊗-homo.η (X , Y) ∘ D.id          ≈˘⟨ refl⟩∘⟨ ⊗.identity ⟩
            ⊗-homo.η (X , Y) ∘ D.id ⊗₁ D.id  ∎
        }
      }
      where open MonoidalFunctor F

    _∘ᵥ_ : {F G H : MonoidalFunctor C D} → G ⇛ H → F ⇛ G → F ⇛ H
    _∘ᵥ_ {F} {G} {H} αᵐ βᵐ = record
      { U               = α NT.∘ᵥ β
      ; isMonoidal      = record
        { ε-compat      = begin
            (α [ _ ] ∘ β [ _ ]) ∘ F.ε   ≈⟨ pullʳ (ε-compat βᵐ) ⟩
            α [ _ ] ∘ G.ε               ≈⟨ ε-compat αᵐ ⟩
            H.ε                         ∎
        ; ⊗-homo-compat = λ {X Y} → begin
              (α [ X C.⊗₀ Y ] ∘ β [ X C.⊗₀ Y ]) ∘ F.⊗-homo.η (X , Y)
            ≈⟨ pullʳ (⊗-homo-compat βᵐ) ⟩
              α [ X C.⊗₀ Y ] ∘ G.⊗-homo.η (X , Y) ∘ β [ X ] ⊗₁ β [ Y ]
            ≈⟨ extendʳ (⊗-homo-compat αᵐ) ⟩
              H.⊗-homo.η (X , Y) ∘ α [ X ] ⊗₁ α [ Y ] ∘ β [ X ] ⊗₁ β [ Y ]
            ≈˘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩
              H.⊗-homo.η (X , Y) ∘ (α [ X ] ∘ β [ X ]) ⊗₁ (α [ Y ] ∘ β [ Y ])
            ∎
        }
      }
      where
        open MonoidalNaturalTransformation
        α = U αᵐ
        β = U βᵐ
        module F = MonoidalFunctor F
        module G = MonoidalFunctor G
        module H = MonoidalFunctor H

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′}
           {E : MonoidalCategory o″ ℓ″ e″} where
    private
      module C = MonoidalCategory C
      module D = MonoidalCategory D
      module E = MonoidalCategory E
      open E hiding (U; id)
      open MorphismReasoning E.U
      open MonoidalReasoning E.monoidal

    infixr 9 _∘ₕ_ _∘ˡ_ _∘ʳ_

    _∘ₕ_ : {F G : MonoidalFunctor C D} {H I : MonoidalFunctor D E} →
            H ⇛ I → F ⇛ G → (H ∘Fˡ F) ⇛ (I ∘Fˡ G)
    _∘ₕ_ {F} {G} {H} {I} αᵐ βᵐ = record
      { U               = α NT.∘ₕ β
      ; isMonoidal      = record
        { ε-compat      = begin
            (I.₁ (β [ C.unit ]) ∘ α [ F.₀ C.unit ]) ∘ H.₁ F.ε ∘ H.ε
          ≈⟨ extend² (commute αᵐ F.ε) ⟩
            (I.₁ (β [ C.unit ]) ∘ I.₁ F.ε) ∘ α [ D.unit ] ∘ H.ε
          ≈˘⟨ I.homomorphism ⟩∘⟨refl ⟩
            I.₁ (β [ C.unit ] D.∘ F.ε) ∘ α [ D.unit ] ∘ H.ε
          ≈⟨ I.F-resp-≈ (ε-compat βᵐ) ⟩∘⟨ ε-compat αᵐ ⟩
            I.F₁ G.ε ∘ I.ε
          ∎
        ; ⊗-homo-compat = λ {X Y} → begin
            (I.₁ (β [ X C.⊗₀ Y ]) ∘ α [ F.₀ (X C.⊗₀ Y) ]) ∘
            H.₁ (F.⊗-homo.η (X , Y)) ∘ H.⊗-homo.η (F.₀ X , F.₀ Y)
          ≈⟨ extend² (commute αᵐ (F.⊗-homo.η (X , Y))) ⟩
            (I.₁ (β [ X C.⊗₀ Y ]) ∘ I.₁ (F.⊗-homo.η (X , Y))) ∘
            α [ F.₀ X D.⊗₀ F.₀ Y ] ∘ H.⊗-homo.η (F.₀ X , F.₀ Y)
          ≈˘⟨ I.homomorphism ⟩∘⟨refl ⟩
            (I.₁ (β [ X C.⊗₀ Y ] D.∘ F.⊗-homo.η (X , Y))) ∘
            α [ F.₀ X D.⊗₀ F.₀ Y ] ∘ H.⊗-homo.η (F.₀ X , F.₀ Y)
          ≈⟨ (I.F-resp-≈ (⊗-homo-compat βᵐ) ⟩∘⟨ ⊗-homo-compat αᵐ) ⟩
            (I.₁ (G.⊗-homo.η (X , Y) D.∘ β [ X ] D.⊗₁ β [ Y ])) ∘
            I.⊗-homo.η (F.₀ X , F.₀ Y) ∘ α [ F.₀ X ] ⊗₁ α [ F.₀ Y ]
          ≈⟨ I.homomorphism ⟩∘⟨refl ⟩
            (I.₁ (G.⊗-homo.η (X , Y)) ∘ I.₁ (β [ X ] D.⊗₁ β [ Y ])) ∘
            I.⊗-homo.η (F.₀ X , F.₀ Y) ∘ α [ F.₀ X ] ⊗₁ α [ F.₀ Y ]
          ≈˘⟨ extend² (I.⊗-homo.commute ((β [ X ]) , (β [ Y ]))) ⟩
            (I.₁ (G.⊗-homo.η (X , Y)) ∘ I.⊗-homo.η (G.₀ X , G.₀ Y)) ∘
            I.₁ (β [ X ]) ⊗₁ I.₁ (β [ Y ]) ∘ α [ F.₀ X ] ⊗₁ α [ F.₀ Y ]
          ≈˘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩
            (I.₁ (G.⊗-homo.η (X , Y)) ∘ I.⊗-homo.η (G.₀ X , G.₀ Y)) ∘
            (I.₁ (β [ X ]) ∘ α [ F.₀ X ]) ⊗₁ (I.₁ (β [ Y ]) ∘ α [ F.₀ Y ])
          ∎
        }
      }
      where
        open MonoidalNaturalTransformation
        α = U αᵐ
        β = U βᵐ
        module F = MonoidalFunctor F
        module G = MonoidalFunctor G
        module H = MonoidalFunctor H
        module I = MonoidalFunctor I

    _∘ˡ_ : {F G : MonoidalFunctor C D}
           (H : MonoidalFunctor D E) → F ⇛ G → (H ∘Fˡ F) ⇛ (H ∘Fˡ G)
    H ∘ˡ α = id {F = H} ∘ₕ α

    _∘ʳ_ : {G H : MonoidalFunctor D E} →
           G ⇛ H → (F : MonoidalFunctor C D) → (G ∘Fˡ F) ⇛ (H ∘Fˡ F)
    α ∘ʳ F = α ∘ₕ id {F = F}

module Strong where
  open StrongMonoidalFunctor
    using () renaming (F to UF; monoidalFunctor to laxF)

  module _ {o ℓ e o′ ℓ′ e′}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′}
           (F G : StrongMonoidalFunctor C D) where

    -- Monoidal natural transformations between strong monoidal functors.

    IsMonoidalNaturalTransformation : NaturalTransformation (UF F) (UF G) →
                                      Set (o ⊔ ℓ′ ⊔ e′)
    IsMonoidalNaturalTransformation α =
      Lax.IsMonoidalNaturalTransformation (laxF F) (laxF G) α

    -- NOTE. This record contains the same data as the lax version,
    -- but the type arguments are different.  This helps type
    -- inference by providing the right constraints.

    record MonoidalNaturalTransformation : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
      field
        U          : NaturalTransformation (UF F) (UF G)
        isMonoidal : IsMonoidalNaturalTransformation U

      laxNT : Lax.MonoidalNaturalTransformation (laxF F) (laxF G)
      laxNT = record { U = U ; isMonoidal = isMonoidal }
      open Lax.MonoidalNaturalTransformation laxNT public hiding (U; isMonoidal)

  private _⇛_ = MonoidalNaturalTransformation

  open MonoidalNaturalTransformation

  module _ {o ℓ e o′ ℓ′ e′}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′} where

    infixr 9 _∘ᵥ_

    -- Since they contain the same data, we can strengthen a lax
    -- monoidal transformation to a strong one.

    strengthen : {F G : StrongMonoidalFunctor C D} →
                 Lax.MonoidalNaturalTransformation (laxF F) (laxF G) → F ⇛ G
    strengthen α = record { U = L.U ; isMonoidal = L.isMonoidal }
      where module L = Lax.MonoidalNaturalTransformation α

    -- Identity and compositions

    id : {F : StrongMonoidalFunctor C D} → F ⇛ F
    id = strengthen Lax.id

    _∘ᵥ_ : {F G H : StrongMonoidalFunctor C D} → G ⇛ H → F ⇛ G → F ⇛ H
    α ∘ᵥ β = strengthen (laxNT α Lax.∘ᵥ laxNT β)

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′}
           {E : MonoidalCategory o″ ℓ″ e″} where

    open Lax.MonoidalNaturalTransformation

    infixr 9 _∘ₕ_ _∘ˡ_ _∘ʳ_

    _∘ₕ_ : {F G : StrongMonoidalFunctor C D} {H I : StrongMonoidalFunctor D E} →
            H ⇛ I → F ⇛ G → (H ∘Fˢ F) ⇛ (I ∘Fˢ G)
    -- FIXME: this definition is clearly equivalent to
    --
    --   α ∘ₕ β = strengthen (laxNT α Lax.∘ₕ laxNT β)
    --
    -- but the latter takes an unreasonably long time to typecheck,
    -- while the unfolded version typechecks almost immediately.
    α ∘ₕ β = record
      { U               = L.U
      ; isMonoidal      = record
        { ε-compat      = L.ε-compat
        ; ⊗-homo-compat = L.⊗-homo-compat }
        }
      where
        module L = Lax.MonoidalNaturalTransformation (laxNT α Lax.∘ₕ laxNT β)

    _∘ˡ_ : {F G : StrongMonoidalFunctor C D}
           (H : StrongMonoidalFunctor D E) → F ⇛ G → (H ∘Fˢ F) ⇛ (H ∘Fˢ G)
    H ∘ˡ α  = id {F = H} ∘ₕ α

    _∘ʳ_ : {G H : StrongMonoidalFunctor D E} →
           G ⇛ H → (F : StrongMonoidalFunctor C D) → (G ∘Fˢ F) ⇛ (H ∘Fˢ F)
    α ∘ʳ F = α ∘ₕ id {F = F}


text:
import      Lvl
open import Type

module Structure.Logic.Constructive.Functions {ℓₒ} (Domain : Type{ℓₒ}) where

private
  module Meta where
    open import Numeral.Finite           public
    open import Numeral.Natural                public

-- The type of a function. Functions on the domain in the meta-logic.
Function : Type{_}
Function = (Domain → Domain)

BinaryOperator : Type{_}
BinaryOperator = (Domain → Domain → Domain)

Tuple : Meta.ℕ → Type{_}
Tuple(n) = Meta.𝕟(n) → Domain

Sequence : Type{_}
Sequence = Meta.ℕ → Domain