text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Construction.Functors where

-- the "Functor Category", often denoted [ C , D ]

open import Level
open import Data.Product using (_,_; proj₁; uncurry′)

open import Categories.Category using (Category; _[_∘_])
open import Categories.Category.Equivalence using (StrongEquivalence)
open import Categories.Category.Product using (_※ⁿ_) renaming (Product to _×_)
open import Categories.Functor using (Functor; _∘F_)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Construction.Constant using (constNat)
open import Categories.NaturalTransformation
  using (NaturalTransformation; _∘ᵥ_; _∘ˡ_; _∘ₕ_) renaming (id to idN)
open import Categories.NaturalTransformation.Equivalence using (_≃_; ≃-isEquivalence)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism)
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e o′ ℓ′ e′ : Level
    C D C₁ C₂ : Category o ℓ e

-- The reason the proofs below are so easy is that _∘ᵥ_ 'computes' all the way down into
-- expressions in D, from which the properties follow.
Functors : Category o ℓ e → Category o′ ℓ′ e′ → Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
Functors C D = record
  { Obj       = Functor C D
  ; _⇒_       = NaturalTransformation
  ; _≈_       = _≃_
  ; id        = idN
  ; _∘_       = _∘ᵥ_
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = ≃-isEquivalence
  ; ∘-resp-≈  = λ eq eq′ → ∘-resp-≈ eq eq′
  }
  where module C = Category C
        module D = Category D
        open D

-- Part of the proof that Cats is a CCC:
eval : Bifunctor (Functors C D) C D
eval {C = C} {D = D} = record
  { F₀           = uncurry′ Functor.F₀
  ; F₁           = λ where
    {F , _} {_ , B} (α , f) →
      let open NaturalTransformation α
          open Functor F
      in η B ∘ F₁ f
  ; identity     = λ where
    {F , _} → elimʳ (Functor.identity F)
  ; homomorphism = λ where
    {F , _} {G , B} {_ , C} {α , f} {β , g} →
      let open NaturalTransformation
          open Functor
      in begin
        (η β C ∘ η α C) ∘ F₁ F (g C.∘ f)  ≈⟨ refl ⟩∘⟨ homomorphism F ⟩
        (η β C ∘ η α C) ∘ F₁ F g ∘ F₁ F f ≈⟨ assoc ⟩
        η β C ∘ η α C ∘ F₁ F g ∘ F₁ F f   ≈⟨ refl ⟩∘⟨ pullˡ (commute α g) ⟩
        η β C ∘ (F₁ G g ∘ η α B) ∘ F₁ F f ≈⟨ refl ⟩∘⟨ assoc ⟩
        η β C ∘ F₁ G g ∘ η α B ∘ F₁ F f   ≈˘⟨ assoc ⟩
        (η β C ∘ F₁ G g) ∘ η α B ∘ F₁ F f ∎
  ; F-resp-≈     = λ where
    {F , _} (comm , eq) → ∘-resp-≈ comm (Functor.F-resp-≈ F eq)
  }
  where module C = Category C
        module D = Category D
        open D
        open MR D
        open HomReasoning

-- Currying induces a functor between functor categories -- another
-- part of the proof that Cats is a catesian closed (bi)category.

curry : Functor (Functors (C₁ × C₂) D) (Functors C₁ (Functors C₂ D))
curry {C₁ = C₁} {C₂ = C₂} {D = D} = record
  { F₀ = curry₀
  ; F₁ = curry₁
  ; identity     = Equiv.refl D
  ; homomorphism = Equiv.refl D
  ; F-resp-≈     = λ F≈G {x₁} {x₂} → F≈G {x₁ , x₂}
  }
  where
    open Category

    curry₀ : Bifunctor C₁ C₂ D → Functor C₁ (Functors C₂ D)
    curry₀ F = record
      { F₀ = λ c → appˡ F c
      ; F₁ = λ f → F ∘ˡ (constNat f ※ⁿ idN)
      ; identity     = identity
      ; homomorphism = λ {_} {_} {_} {f} {g} → begin
          F₁ (C₁ [ g ∘ f ] , id C₂)
        ≈˘⟨ F-resp-≈ (Equiv.refl C₁ , identityˡ C₂) ⟩
          F₁ (C₁ [ g ∘ f ] , C₂ [ id C₂ ∘ id C₂ ])
        ≈⟨ homomorphism ⟩
          D [ F₁ (g , id C₂) ∘ F₁ (f , id C₂) ]
        ∎
      ; F-resp-≈ = λ f≈g → F-resp-≈ (f≈g , Equiv.refl C₂)
      }
      where
        open Functor F
        open HomReasoning D

    curry₁ : {F G : Bifunctor C₁ C₂ D} →
             NaturalTransformation F G →
             NaturalTransformation (curry₀ F) (curry₀ G)
    curry₁ α = record
      { η = λ c → record
        { η           = λ a → η α (c , a)
        ; commute     = λ f → commute α (id C₁  , f)
        ; sym-commute = λ f → sym-commute α (id C₁  , f)
        }
      ; commute       = λ f → commute α (f , id C₂)
      ; sym-commute   = λ f → sym-commute α (f , id C₂)
      }
      where open NaturalTransformation

module curry {o₁ e₁ ℓ₁} {C₁ : Category o₁ e₁ ℓ₁}
             {o₂ e₂ ℓ₂} {C₂ : Category o₂ e₂ ℓ₂}
             {o′ e′ ℓ′} {D  : Category o′ e′ ℓ′}
             where
  open Functor (curry {C₁ = C₁} {C₂ = C₂} {D = D}) public
  open Category
  open NaturalIsomorphism

  -- Currying preserves natural isos.
  -- This makes |curry.F₀| a map between the hom-setoids of Cats.

  resp-NI : {F G : Bifunctor C₁ C₂ D} →
            NaturalIsomorphism F G → NaturalIsomorphism (F₀ F) (F₀ G)
  resp-NI α = record
    { F⇒G = F₁ (F⇒G α)
    ; F⇐G = F₁ (F⇐G α)
    ; iso = λ x → record
      { isoˡ = iso.isoˡ α (x , _)
      ; isoʳ = iso.isoʳ α (x , _)
      }
    }

-- Godement product ?
product : {A B C : Category o ℓ e} → Bifunctor (Functors B C) (Functors A B) (Functors A C)
product {A = A} {B = B} {C = C} = record
  { F₀ = uncurry′ _∘F_
  ; F₁ = uncurry′ _∘ₕ_
  ; identity = λ {f} → identityʳ ○ identity {D = C} (proj₁ f)
  ; homomorphism = λ { {_ , F₂} {G₁ , G₂} {H₁ , _} {f₁ , f₂} {g₁ , g₂} {x} → begin
      F₁ H₁ (η g₂ x B.∘ η f₂ x) ∘ η g₁ (F₀ F₂ x) ∘ η f₁ (F₀ F₂ x)
          ≈⟨ ∘-resp-≈ˡ (homomorphism H₁) ○ assoc ○ ∘-resp-≈ʳ (⟺ assoc) ⟩
      F₁ H₁ (η g₂ x) ∘ (F₁ H₁ (η f₂ x) ∘ η g₁ (F₀ F₂ x)) ∘ η f₁ (F₀ F₂ x)
          ≈⟨  ⟺ ( refl⟩∘⟨ ( commute g₁ (η f₂ x) ⟩∘⟨refl) ) ⟩
      F₁ H₁ (η g₂ x) ∘ (η g₁ (F₀ G₂ x) ∘ F₁  G₁ (η f₂ x)) ∘ η f₁ (F₀ F₂ x)
          ≈⟨ ∘-resp-≈ʳ assoc ○ ⟺ assoc ⟩
      (F₁ H₁ (η g₂ x) ∘ η g₁ (F₀ G₂ x)) ∘ F₁ G₁ (η f₂ x) ∘ η f₁ (F₀ F₂ x) ∎ }
  ; F-resp-≈ = λ { {_} {g₁ , _} (≈₁ , ≈₂) → ∘-resp-≈ (F-resp-≈ g₁ ≈₂) ≈₁ }
  }
  where
    open Category C
    open HomReasoning
    open Functor
    module B = Category B
    open NaturalTransformation

-- op induces a Functor on the Functors category.
-- This is an instance where the proof-irrelevant version is simpler because (op op C) is
-- just C. Here we rather need to be more explicit.
opF⇒ : {A : Category o ℓ e} {B : Category o′ ℓ′ e′} →
      Functor (Category.op (Functors (Category.op A) (Category.op B))) (Functors A B)
opF⇒ {A = A} {B} = record
  { F₀ = Functor.op
  ; F₁ = NaturalTransformation.op
  ; identity = Equiv.refl
  ; homomorphism = Equiv.refl
  ; F-resp-≈ = λ eq → eq
  }
  where open Category B

opF⇐ : {A : Category o ℓ e} {B : Category o′ ℓ′ e′} →
      Functor (Functors A B) (Category.op (Functors (Category.op A) (Category.op B)))
opF⇐ {A = A} {B} = record
  { F₀           = Functor.op
  ; F₁           = NaturalTransformation.op
  ; identity     = Equiv.refl
  ; homomorphism = Equiv.refl
  ; F-resp-≈     = λ eq → eq
  }
  where open Category B

Functorsᵒᵖ-equiv : {A : Category o ℓ e} {B : Category o′ ℓ′ e′} →
                   StrongEquivalence (Category.op (Functors (Category.op A) (Category.op B))) (Functors A B)
Functorsᵒᵖ-equiv {B = B} = record
  { F            = opF⇒
  ; G            = opF⇐
  ; weak-inverse = record
    { F∘G≈id = record
      { F⇒G = record
        { η           = λ _ → idN
        ; commute     = λ _ → id-comm-sym
        ; sym-commute = λ _ → id-comm
        }
      ; F⇐G = record
        { η           = λ _ → idN
        ; commute     = λ _ → id-comm-sym
        ; sym-commute = λ _ → id-comm
        }
      ; iso = λ _ → record
        { isoˡ = identityˡ
        ; isoʳ = identityˡ
        }
      }
    ; G∘F≈id = record
      { F⇒G = record
        { η           = λ _ → idN
        ; commute     = λ _ → id-comm-sym
        ; sym-commute = λ _ → id-comm
        }
      ; F⇐G = record
        { η           = λ _ → idN
        ; commute     = λ _ → id-comm-sym
        ; sym-commute = λ _ → id-comm
        }
      ; iso = λ _ → record
        { isoˡ = identityˡ
        ; isoʳ = identityˡ
        }
      }
    }
  }
  where open Category B
        open HomReasoning
        open MR B

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


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

data D : Set → Set₁ where
  c : (@0 A : Set) → D A

ext: agda

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- Laws for weakenings and substitutions.

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

module Definition.Untyped.Properties where

open import Definition.Untyped

open import Tools.Nat
open import Tools.List
open import Tools.PropositionalEquality hiding (subst)

-- Weakening properties

-- Two weakenings ρ and ρ′ are extensionally equal if they agree on
-- all arguments when interpreted as functions mapping variables to
-- variables.  Formally, they are considered equal iff
--
--   (∀ x → wkVar ρ x ≡ wkVar ρ′ x)
--
-- Intensional (propositional) equality would be too fine.  For
-- instance,
--
--   lift id : Γ∙A ≤ Γ∙A
--
-- is extensionally equal to
--
--   id : Γ∙A ≤ Γ∙A
--
-- but syntactically different.

-- "lift" preserves equality of weakenings.  Or:
-- If two weakenings are equal under wkVar, then they are equal when lifted.

wkVar-lift : ∀ {ρ ρ′}
  → (∀ x → wkVar ρ x ≡ wkVar ρ′ x)
  → (∀ x → wkVar (lift ρ) x ≡ wkVar (lift ρ′) x)

wkVar-lift eq 0      = refl
wkVar-lift eq (1+ x) = cong 1+ (eq x)

wkVar-lifts : ∀ {ρ ρ′}
  → (∀ x → wkVar ρ x ≡ wkVar ρ′ x)
  → (∀ n x → wkVar (repeat lift ρ n) x ≡ wkVar (repeat lift ρ′ n) x)
wkVar-lifts eq 0 x = eq x
wkVar-lifts eq (1+ n) x = wkVar-lift (wkVar-lifts eq n) x

-- Extensionally equal weakenings, if applied to a term,
-- yield the same weakened term.  Or:
-- If two weakenings are equal under wkVar, then they are equal under wk.

mutual
  wkVar-to-wk : ∀ {ρ ρ′}
    → (∀ x → wkVar ρ x ≡ wkVar ρ′ x)
    → ∀ t → wk ρ t ≡ wk ρ′ t
  wkVar-to-wk eq (var x) = cong var (eq x)
  wkVar-to-wk eq (gen x c) = cong (gen x) (wkVar-to-wkGen eq c)

  wkVar-to-wkGen : ∀ {ρ ρ′}
    → (∀ x → wkVar ρ x ≡ wkVar ρ′ x)
    → ∀ t → wkGen ρ t ≡ wkGen ρ′ t
  wkVar-to-wkGen eq [] = refl
  wkVar-to-wkGen eq (⟦ l , t ⟧ ∷ g) =
    cong₂ _∷_ (cong (⟦_,_⟧ l) (wkVar-to-wk (wkVar-lifts eq l) t))
              (wkVar-to-wkGen eq g)

-- lift id  is extensionally equal to  id.

wkVar-lift-id : (x : Nat) → wkVar (lift id) x ≡ wkVar id x
wkVar-lift-id 0    = refl
wkVar-lift-id (1+ x) = refl

wkVar-lifts-id : (n x : Nat) → wkVar (repeat lift id n) x ≡ wkVar id x
wkVar-lifts-id 0 x = refl
wkVar-lifts-id (1+ n) 0 = refl
wkVar-lifts-id (1+ n) (1+ x) = cong 1+ (wkVar-lifts-id n x)

-- id is the identity renaming.

wkVar-id : (x : Nat) → wkVar id x ≡ x
wkVar-id x = refl

mutual
  wk-id : (t : Term) → wk id t ≡ t
  wk-id (var x) = refl
  wk-id (gen x c) = cong (gen x) (wkGen-id c)

  wkGen-id : ∀ x → wkGen id x ≡ x
  wkGen-id [] = refl
  wkGen-id (⟦ l , t ⟧ ∷ g) =
    cong₂ _∷_ (cong (⟦_,_⟧ l)
              (trans (wkVar-to-wk (wkVar-lifts-id l) t) (wk-id t))) (wkGen-id g)

-- lift id  is also the identity renaming.

wk-lift-id : (t : Term) → wk (lift id) t ≡ t
wk-lift-id t = trans (wkVar-to-wk wkVar-lift-id t) (wk-id t)

-- The composition of weakenings is correct...
--
-- ...as action on variables.

wkVar-comp : ∀ ρ ρ′ x → wkVar ρ (wkVar ρ′ x) ≡ wkVar (ρ • ρ′) x
wkVar-comp id       ρ′        x       = refl
wkVar-comp (step ρ) ρ′        x       = cong 1+ (wkVar-comp ρ ρ′ x)
wkVar-comp (lift ρ) id        x       = refl
wkVar-comp (lift ρ) (step ρ′) x       = cong 1+ (wkVar-comp ρ ρ′ x)
wkVar-comp (lift ρ) (lift ρ′) 0    = refl
wkVar-comp (lift ρ) (lift ρ′) (1+ x) = cong 1+ (wkVar-comp ρ ρ′ x)

wkVar-comps : ∀ n ρ ρ′ x
            → wkVar (repeat lift ρ n • repeat lift ρ′ n) x
            ≡ wkVar (repeat lift (ρ • ρ′) n) x
wkVar-comps 0 ρ ρ′ x = refl
wkVar-comps (1+ n) ρ ρ′ 0 = refl
wkVar-comps (1+ n) ρ ρ′ (1+ x) = cong 1+ (wkVar-comps n ρ ρ′ x)

-- ... as action on terms.

mutual
  wk-comp : ∀ ρ ρ′ t → wk ρ (wk ρ′ t) ≡ wk (ρ • ρ′) t
  wk-comp ρ ρ′ (var x) = cong var (wkVar-comp ρ ρ′ x)
  wk-comp ρ ρ′ (gen x c) = cong (gen x) (wkGen-comp ρ ρ′ c)

  wkGen-comp : ∀ ρ ρ′ g → wkGen ρ (wkGen ρ′ g) ≡ wkGen (ρ • ρ′) g
  wkGen-comp ρ ρ′ [] = refl
  wkGen-comp ρ ρ′ (⟦ l , t ⟧ ∷ g) =
    cong₂ _∷_ (cong (⟦_,_⟧ l) (trans (wk-comp (repeat lift ρ l) (repeat lift ρ′ l) t)
                                     (wkVar-to-wk (wkVar-comps l ρ ρ′) t)))
              (wkGen-comp ρ ρ′ g)

-- The following lemmata are variations on the equality
--
--   wk1 ∘ ρ = lift ρ ∘ wk1.
--
-- Typing:  Γ∙A ≤ Γ ≤ Δ  <==>  Γ∙A ≤ Δ∙A ≤ Δ.

lift-step-comp : (ρ : Wk) → step id • ρ ≡ lift ρ • step id
lift-step-comp id       = refl
lift-step-comp (step ρ) = cong step (lift-step-comp ρ)
lift-step-comp (lift ρ) = refl

wk1-wk : ∀ ρ t → wk1 (wk ρ t) ≡ wk (step ρ) t
wk1-wk ρ t = wk-comp (step id) ρ t

lift-wk1 : ∀ ρ t → wk (lift ρ) (wk1 t) ≡ wk (step ρ) t
lift-wk1 pr A = trans (wk-comp (lift pr) (step id) A)
                      (sym (cong (λ x → wk x A) (lift-step-comp pr)))

wk1-wk≡lift-wk1 : ∀ ρ t → wk1 (wk ρ t) ≡ wk (lift ρ) (wk1 t)
wk1-wk≡lift-wk1 ρ t = trans (wk1-wk ρ t) (sym (lift-wk1 ρ t))

-- Substitution properties.

-- Two substitutions σ and σ′ are equal if they are pointwise equal,
-- i.e., agree on all variables.
--
--   ∀ x →  σ x ≡ σ′ x

-- If  σ = σ′  then  lift σ = lift σ′.

substVar-lift : ∀ {σ σ′}
  → (∀ x → σ x ≡ σ′ x)
  → ∀ x → liftSubst σ x ≡ liftSubst σ′ x

substVar-lift eq 0    = refl
substVar-lift eq (1+ x) = cong wk1 (eq x)

substVar-lifts : ∀ {σ σ′}
  → (∀ x → σ x ≡ σ′ x)
  → ∀ n x → repeat liftSubst σ n x ≡ repeat liftSubst σ′ n x

substVar-lifts eq 0 x = eq x
substVar-lifts eq (1+ n) 0 = refl
substVar-lifts eq (1+ n) (1+ x) = cong wk1 (substVar-lifts eq n x)

-- If  σ = σ′  then  subst σ t = subst σ′ t.

mutual
  substVar-to-subst : ∀ {σ σ′}
    → ((x : Nat) → σ x ≡ σ′ x)
    → (t : Term) → subst σ t ≡ subst σ′ t
  substVar-to-subst eq (var x) = eq x
  substVar-to-subst eq (gen x c) = cong (gen x) (substVar-to-substGen eq c)

  substVar-to-substGen : ∀ {σ σ′}
    → ((x : Nat) → σ x ≡ σ′ x)
    → ∀ g → substGen σ g ≡ substGen σ′ g
  substVar-to-substGen eq [] = refl
  substVar-to-substGen eq (⟦ l , t ⟧ ∷ g) =
    cong₂ _∷_ (cong (⟦_,_⟧ l) (substVar-to-subst (substVar-lifts eq l) t))
              (substVar-to-substGen eq g)

-- lift id = id  (as substitutions)

subst-lift-id : (x : Nat) → (liftSubst idSubst) x ≡ idSubst x
subst-lift-id 0    = refl
subst-lift-id (1+ x) = refl

subst-lifts-id : (n x : Nat) → (repeat liftSubst idSubst n) x ≡ idSubst x
subst-lifts-id 0 x = refl
subst-lifts-id (1+ n) 0 = refl
subst-lifts-id (1+ n) (1+ x) = cong wk1 (subst-lifts-id n x)

-- Identity substitution.

mutual
  subst-id : (t : Term) → subst idSubst t ≡ t
  subst-id (var x) = refl
  subst-id (gen x c) = cong (gen x) (substGen-id c)

  substGen-id : ∀ g → substGen idSubst g ≡ g
  substGen-id [] = refl
  substGen-id (⟦ l , t ⟧ ∷ g) =
    cong₂ _∷_ (cong (⟦_,_⟧ l) (trans (substVar-to-subst (subst-lifts-id l) t)
                                     (subst-id t)))
              (substGen-id g)

-- Correctness of composition of weakening and substitution.

-- Composition of liftings is lifting of the composition.
-- lift ρ •ₛ lift σ = lift (ρ •ₛ σ)

subst-lift-•ₛ : ∀ {ρ σ} t
              → subst (lift ρ •ₛ liftSubst σ) t
              ≡ subst (liftSubst (ρ •ₛ σ)) t
subst-lift-•ₛ =
  substVar-to-subst (λ { 0 → refl ; (1+ x) → sym (wk1-wk≡lift-wk1 _ _)})

helper1 : ∀ {ρ σ} (n x : Nat) →
      (lift (repeat lift ρ n) •ₛ liftSubst (repeat liftSubst σ n)) x ≡
      liftSubst (repeat liftSubst (ρ •ₛ σ) n) x
helper1 0 0 = refl
helper1 0 (1+ x) = sym (wk1-wk≡lift-wk1 _ _)
helper1 (1+ n) 0 = refl
helper1 (1+ n) (1+ x) = trans (sym (wk1-wk≡lift-wk1 _ _)) (cong wk1 (helper1 n x))

subst-lifts-•ₛ : ∀ {ρ σ} n t
              → subst (repeat lift ρ n •ₛ repeat liftSubst σ n) t
              ≡ subst (repeat liftSubst (ρ •ₛ σ) n) t
subst-lifts-•ₛ 0 t = refl
subst-lifts-•ₛ (1+ n) t = substVar-to-subst (helper1 n) t

-- lift σ ₛ• lift ρ = lift (σ ₛ• ρ)

subst-lift-ₛ• : ∀ {ρ σ} t
              → subst (liftSubst σ ₛ• lift ρ) t
              ≡ subst (liftSubst (σ ₛ• ρ)) t
subst-lift-ₛ• = substVar-to-subst (λ { 0 → refl ; (1+ x) → refl})

helper2 : ∀ {ρ σ} (n x : Nat) →
      liftSubst (repeat liftSubst σ n) (wkVar (lift (repeat lift ρ n)) x) ≡
      liftSubst (repeat liftSubst (λ x₁ → σ (wkVar ρ x₁)) n) x
helper2 0 0 = refl
helper2 0 (1+ x) = refl
helper2 (1+ n) 0 = refl
helper2 (1+ n) (1+ x) = cong wk1 (helper2 n x)

subst-lifts-ₛ• : ∀ {ρ σ} n t
              → subst (repeat liftSubst σ n ₛ• repeat lift ρ n) t
              ≡ subst (repeat liftSubst (σ ₛ• ρ) n) t
subst-lifts-ₛ• 0 t = refl
subst-lifts-ₛ• (1+ n) t = substVar-to-subst (helper2 n) t

-- wk ρ ∘ subst σ = subst (ρ •ₛ σ)

mutual
  wk-subst : ∀ {ρ σ} t → wk ρ (subst σ t) ≡ subst (ρ •ₛ σ) t
  wk-subst (var x) = refl
  wk-subst (gen x c) = cong (gen x) (wkGen-substGen c)

  wkGen-substGen : ∀ {ρ σ} t → wkGen ρ (substGen σ t) ≡ substGen (ρ •ₛ σ) t
  wkGen-substGen [] = refl
  wkGen-substGen (⟦ l , t ⟧ ∷ c) =
    cong₂ _∷_ (cong (⟦_,_⟧ l) (trans (wk-subst t) (subst-lifts-•ₛ l t)))
              (wkGen-substGen c)

-- subst σ ∘ wk ρ = subst (σ •ₛ ρ)

mutual
  subst-wk : ∀ {ρ σ} t → subst σ (wk ρ t) ≡ subst (σ ₛ• ρ) t
  subst-wk (var x) = refl
  subst-wk (gen x c) = cong (gen x) (substGen-wkGen c)

  substGen-wkGen : ∀ {ρ σ} t → substGen σ (wkGen ρ t) ≡ substGen (σ ₛ• ρ) t
  substGen-wkGen [] = refl
  substGen-wkGen (⟦ l , t ⟧ ∷ c) =
    cong₂ _∷_ (cong (⟦_,_⟧ l) (trans (subst-wk t) (subst-lifts-ₛ• l t)))
              (substGen-wkGen c)

-- Composition of liftings is lifting of the composition.

wk-subst-lift : ∀ {ρ σ} G
              → wk (lift ρ) (subst (liftSubst σ) G)
              ≡ subst (liftSubst (ρ •ₛ σ)) G
wk-subst-lift G = trans (wk-subst G) (subst-lift-•ₛ G)

-- Renaming with ρ is the same as substituting with ρ turned into a substitution.

wk≡subst : ∀ ρ t → wk ρ t ≡ subst (toSubst ρ) t
wk≡subst ρ t = trans (cong (wk ρ) (sym (subst-id t))) (wk-subst t)

-- Composition of substitutions.

-- Composition of liftings is lifting of the composition.

substCompLift : ∀ {σ σ′} x
              → (liftSubst σ ₛ•ₛ liftSubst σ′) x
              ≡ (liftSubst (σ ₛ•ₛ σ′)) x
substCompLift          0    = refl
substCompLift {σ} {σ′} (1+ x) = trans (subst-wk (σ′ x)) (sym (wk-subst (σ′ x)))

substCompLifts : ∀ {σ σ′} n x
              → (repeat liftSubst σ n ₛ•ₛ repeat liftSubst σ′ n) x
              ≡ (repeat liftSubst (σ ₛ•ₛ σ′) n) x
substCompLifts 0 x = refl
substCompLifts (1+ n) 0 = refl
substCompLifts {σ} {σ′} (1+ n) (1+ x) =
  trans (substCompLift {repeat liftSubst σ n} {repeat liftSubst σ′ n} (1+ x))
        (cong wk1 (substCompLifts n x))

-- Soundness of the composition of substitutions.

mutual
  substCompEq : ∀ {σ σ′} (t : Term)
              → subst σ (subst σ′ t) ≡ subst (σ ₛ•ₛ σ′) t
  substCompEq (var x) = refl
  substCompEq (gen x c) = cong (gen x) (substGenCompEq c)

  substGenCompEq : ∀ {σ σ′} t
              → substGen σ (substGen σ′ t) ≡ substGen (σ ₛ•ₛ σ′) t
  substGenCompEq [] = refl
  substGenCompEq (⟦ l , t ⟧ ∷ c) =
    cong₂ _∷_ (cong (⟦_,_⟧ l) (trans (substCompEq t)
                                     (substVar-to-subst (substCompLifts l) t)))
              (substGenCompEq c)

-- Weakening single substitutions.

-- Pulling apart a weakening composition in specific context _[a].

wk-comp-subst : ∀ {a} ρ ρ′ G
  → wk (lift (ρ • ρ′)) G [ a ] ≡ wk (lift ρ) (wk (lift ρ′) G) [ a ]

wk-comp-subst {a} ρ ρ′ G =
  cong (λ x → x [ a ]) (sym (wk-comp (lift ρ) (lift ρ′) G))

-- Pushing a weakening into a single substitution.
-- ρ (t[a]) = ((lift ρ) t)[ρ a]

wk-β : ∀ {ρ a} t → wk ρ (t [ a ]) ≡ wk (lift ρ) t [ wk ρ a ]
wk-β t = trans (wk-subst t) (sym (trans (subst-wk t)
               (substVar-to-subst (λ { 0 → refl ; (1+ x) → refl}) t)))

-- Pushing a weakening into a single shifting substitution.
-- If  ρ′ = lift ρ  then  ρ′(t[a]↑) = ρ′(t) [ρ′(a)]↑

wk-β↑ : ∀ {ρ a} t → wk (lift ρ) (t [ a ]↑) ≡ wk (lift ρ) t [ wk (lift ρ) a ]↑
wk-β↑ t = trans (wk-subst t) (sym (trans (subst-wk t)
                (substVar-to-subst (λ { 0 → refl ; (1+ x) → refl}) t)))

-- A specific equation on weakenings used for the reduction of natrec.

wk-β-natrec : ∀ ρ G
  → Π ℕ ▹ (Π wk (lift ρ) G ▹ wk (lift (lift ρ)) (wk1 (G [ suc (var 0) ]↑)))
  ≡ Π ℕ ▹ (wk (lift ρ) G ▹▹ wk (lift ρ) G [ suc (var 0) ]↑)
wk-β-natrec ρ G =
  cong₂ Π_▹_ refl (cong₂ Π_▹_ refl
    (trans (wk-comp (lift (lift ρ)) (step id)
                    (subst (consSubst (wk1Subst var) (suc (var 0))) G))
       (trans (wk-subst G) (sym (trans (wk-subst (wk (lift ρ) G))
         (trans (subst-wk G)
                (substVar-to-subst (λ { 0 → refl ; (1+ x) → refl}) G)))))))

-- Composing a singleton substitution and a lifted substitution.
-- sg u ∘ lift σ = cons id u ∘ lift σ = cons σ u

substVarSingletonComp : ∀ {u σ} (x : Nat)
  → (sgSubst u ₛ•ₛ liftSubst σ) x ≡ (consSubst σ u) x
substVarSingletonComp 0 = refl
substVarSingletonComp {σ = σ} (1+ x) = trans (subst-wk (σ x)) (subst-id (σ x))

-- The same again, as action on a term t.

substSingletonComp : ∀ {a σ} t
  → subst (sgSubst a ₛ•ₛ liftSubst σ) t ≡ subst (consSubst σ a) t
substSingletonComp = substVar-to-subst substVarSingletonComp

-- A single substitution after a lifted substitution.
-- ((lift σ) G)[t] = (cons σ t)(G)

singleSubstComp : ∀ t σ G
                 → (subst (liftSubst σ) G) [ t ]
                 ≡ subst (consSubst σ t) G
singleSubstComp t σ G = trans (substCompEq G) (substSingletonComp G)

-- A single substitution after a lifted substitution (with weakening).
-- ((lift (ρ ∘ σ)) G)[t] = (cons (ρ ∘ σ) t)(G)

singleSubstWkComp : ∀ {ρ} t σ G
               → wk (lift ρ) (subst (liftSubst σ) G) [ t ]
               ≡ subst (consSubst (ρ •ₛ σ) t) G
singleSubstWkComp t σ G =
  trans (cong (subst (consSubst var t))
              (trans (wk-subst G) (subst-lift-•ₛ G)))
        (trans (substCompEq G) (substSingletonComp G))

-- Pushing a substitution into a single substitution.

singleSubstLift : ∀ {σ} G t
                → subst σ (G [ t ])
                ≡ subst (liftSubst σ) G [ subst σ t ]
singleSubstLift G t =
  trans (substCompEq G)
        (trans (trans (substVar-to-subst (λ { 0 → refl ; (1+ x) → refl}) G)
                      (sym (substSingletonComp G)))
               (sym (substCompEq G)))

-- More specific laws.

idWkLiftSubstLemma : ∀ σ G
  → wk (lift (step id)) (subst (liftSubst σ) G) [ var 0 ]
  ≡ subst (liftSubst σ) G
idWkLiftSubstLemma σ G =
  trans (singleSubstWkComp (var 0) σ G)
        (substVar-to-subst (λ { 0 → refl ; (1+ x) → refl}) G)

substVarComp↑ : ∀ {t} σ x
  → (consSubst (wk1Subst idSubst) (subst (liftSubst σ) t) ₛ•ₛ liftSubst σ) x
  ≡ (liftSubst σ ₛ•ₛ consSubst (wk1Subst idSubst) t) x
substVarComp↑ σ 0 = refl
substVarComp↑ σ (1+ x) = trans (subst-wk (σ x)) (sym (wk≡subst (step id) (σ x)))

singleSubstLift↑ : ∀ σ G t
                 → subst (liftSubst σ) (G [ t ]↑)
                 ≡ subst (liftSubst σ) G [ subst (liftSubst σ) t ]↑
singleSubstLift↑ σ G t =
  trans (substCompEq G)
        (sym (trans (substCompEq G) (substVar-to-subst (substVarComp↑ σ) G)))

substConsComp : ∀ {σ t G}
       → subst (consSubst (λ x → σ (1+ x)) (subst (tail σ) t)) G
       ≡ subst σ (subst (consSubst (λ x → var (1+ x)) (wk1 t)) G)
substConsComp {t = t} {G = G} =
  trans (substVar-to-subst (λ { 0 → sym (subst-wk t) ; (1+ x) → refl }) G)
        (sym (substCompEq G))

wkSingleSubstId : ∀ F → (wk (lift (step id)) F) [ var 0 ] ≡ F
wkSingleSubstId F =
  trans (subst-wk F)
        (trans (substVar-to-subst (λ { 0 → refl ; (1+ x) → refl}) F)
               (subst-id F))

cons-wk-subst : ∀ ρ σ a t
       → subst (sgSubst a ₛ• lift ρ ₛ•ₛ liftSubst σ) t
       ≡ subst (consSubst (ρ •ₛ σ) a) t
cons-wk-subst ρ σ a = substVar-to-subst
  (λ { 0 → refl
     ; (1+ x) → trans (subst-wk (σ x)) (sym (wk≡subst ρ (σ x))) })

natrecSucCaseLemma : ∀ {σ} (x : Nat)
  → (step id •ₛ consSubst (wk1Subst idSubst) (suc (var 0)) ₛ•ₛ liftSubst σ) x
  ≡ (liftSubst (liftSubst σ) ₛ• step id ₛ•ₛ consSubst (wk1Subst idSubst) (suc (var 0))) x
natrecSucCaseLemma 0 = refl
natrecSucCaseLemma {σ} (1+ x) =
  trans (subst-wk (σ x))
           (sym (trans (wk1-wk (step id) _)
                             (wk≡subst (step (step id)) (σ x))))

natrecSucCase : ∀ σ F
  → Π ℕ ▹ (Π subst (liftSubst σ) F
                ▹ subst (liftSubst (liftSubst σ)) (wk1 (F [ suc (var 0) ]↑)))
  ≡ Π ℕ ▹ (subst (liftSubst σ) F ▹▹ subst (liftSubst σ) F [ suc (var 0) ]↑)
natrecSucCase σ F =
  cong₂ Π_▹_ refl
    (cong₂ Π_▹_ refl
       (trans (trans (subst-wk (F [ suc (var 0) ]↑))
                           (substCompEq F))
                 (sym (trans (wk-subst (subst (liftSubst σ) F))
                                   (trans (substCompEq F)
                                             (substVar-to-subst natrecSucCaseLemma F))))))

natrecIrrelevantSubstLemma : ∀ F z s m σ (x : Nat)
  → (sgSubst (natrec (subst (liftSubst σ) F) (subst σ z) (subst σ s) m)
     ₛ•ₛ liftSubst (sgSubst m)
     ₛ•ₛ liftSubst (liftSubst σ)
     ₛ•  step id
     ₛ•ₛ consSubst (tail idSubst) (suc (var 0))) x
  ≡ (consSubst σ (suc m)) x
natrecIrrelevantSubstLemma F z s m σ 0 =
  cong suc (trans (subst-wk m) (subst-id m))
natrecIrrelevantSubstLemma F z s m σ (1+ x) =
  trans (subst-wk (wk (step id) (σ x)))
           (trans (subst-wk (σ x))
                     (subst-id (σ x)))

natrecIrrelevantSubst : ∀ F z s m σ
  → subst (consSubst σ (suc m)) F
  ≡ subst (liftSubst (sgSubst m))
          (subst (liftSubst (liftSubst σ))
                 (wk1 (F [ suc (var 0) ]↑)))
                   [ natrec (subst (liftSubst σ) F) (subst σ z) (subst σ s) m ]
natrecIrrelevantSubst F z s m σ =
  sym (trans (substCompEq (subst (liftSubst (liftSubst σ))
        (wk (step id)
         (subst (consSubst (tail idSubst) (suc (var 0))) F))))
         (trans (substCompEq (wk (step id)
        (subst (consSubst (tail idSubst) (suc (var 0))) F)))
        (trans
           (subst-wk (subst (consSubst (tail idSubst) (suc (var 0))) F))
           (trans (substCompEq F)
                     (substVar-to-subst (natrecIrrelevantSubstLemma F z s m σ) F)))))

natrecIrrelevantSubstLemma′ : ∀ F z s n (x : Nat)
  → (sgSubst (natrec F z s n)
     ₛ•ₛ liftSubst (sgSubst n)
     ₛ•  step id
     ₛ•ₛ consSubst (tail idSubst) (suc (var 0))) x
  ≡ (consSubst var (suc n)) x
natrecIrrelevantSubstLemma′ F z s n 0 =
  cong suc (trans (subst-wk n) (subst-id n))
natrecIrrelevantSubstLemma′ F z s n (1+ x) = refl

natrecIrrelevantSubst′ : ∀ F z s n
  → subst (liftSubst (sgSubst n))
      (wk1 (F [ suc (var 0) ]↑))
      [ natrec F z s n ]
  ≡ F [ suc n ]
natrecIrrelevantSubst′ F z s n =
  trans (substCompEq (wk (step id)
                         (subst (consSubst (tail idSubst) (suc (var 0))) F)))
        (trans (subst-wk (subst (consSubst (tail idSubst) (suc (var 0))) F))
               (trans (substCompEq F)
                      (substVar-to-subst (natrecIrrelevantSubstLemma′ F z s n) F)))

cons0wkLift1-id : ∀ σ G
    → subst (sgSubst (var 0))
            (wk (lift (step id)) (subst (liftSubst σ) G))
    ≡ subst (liftSubst σ) G
cons0wkLift1-id σ G =
  trans (subst-wk (subst (liftSubst σ) G))
        (trans (substVar-to-subst (λ { 0 → refl ; (1+ x) → refl })
                                  (subst (liftSubst σ) G))
               (subst-id (subst (liftSubst σ) G)))

substConsId : ∀ {σ t} G
        → subst (consSubst σ (subst σ t)) G
        ≡ subst σ (subst (sgSubst t) G)
substConsId G =
  sym (trans (substCompEq G)
             (substVar-to-subst (λ { 0 → refl ; (1+ x) → refl}) G))

substConsTailId : ∀ {G t σ}
                → subst (consSubst (tail σ) (subst σ t)) G
                ≡ subst σ (subst (consSubst (tail idSubst) t) G)
substConsTailId {G} {t} {σ} =
  trans (substVar-to-subst (λ { 0 → refl
                            ; (1+ x) → refl }) G)
        (sym (substCompEq G))

substConcatSingleton′ : ∀ {a σ} t
                      → subst (σ ₛ•ₛ sgSubst a) t
                      ≡ subst (consSubst σ (subst σ a)) t
substConcatSingleton′ t = substVar-to-subst (λ { 0 → refl ; (1+ x) → refl}) t

wk1-tailId : ∀ t → wk1 t ≡ subst (tail idSubst) t
wk1-tailId t = trans (sym (subst-id (wk1 t))) (subst-wk t)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module index where

-- For a brief presentation of every single module, head over to
import Everything

-- Otherwise, here is an exhaustive, stern list of all the available modules.

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The empty binary relation
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Never where

open import Relation.Binary
open import Relation.Binary.Construct.Constant
open import Data.Empty using (⊥)
open import Level using (Lift; lift)

------------------------------------------------------------------------
-- Definition

Never : ∀ {a ℓ} {A : Set a} → Rel A ℓ
Never = Const (Lift _ ⊥)


text:
module Section6 where

open import Section5 public

-- 6. Application to terms
-- =======================
--
-- In practice we may not want to work with proof trees but rather well-typed terms.  As an
-- application of the results above we show how to give semantics to a formulation of Martin-
-- Löf’s substitution calculus [13, 20] in the simply typed setting.  In this calculus we have a
-- set of untyped terms, `𝕋`, and we define when a term in `𝕋` is well-typed and when two terms
-- of a given type are convertible with each other.
--
-- In order to give semantics to untyped terms, we first define an erasure function that
-- translates a proof tree `M` to an untyped term, denoted `M ⁻`.  The main theorem is then to prove
-- that if two proof trees `M, N` erase to the same term, `M ⁻ ≡ N ⁻`, then `M ≅ N`; it follows that
-- `M` and `N` have the same semantics.  For this we first prove that `nf M ⁻ ≡ nf N ⁻` implies
-- `M ≅ N`.  We also define a reduction on the untyped terms `Γ ⊢ t₁ ⇓ t₂ ∷ A` that is deterministic
-- (i.e., if `Γ ⊢ t ⇓ t₁ ∷ A` and `Γ ⊢ t ⇓ t₂ ∷ A`, then `t₁ ≡ t₂`) such that `Γ ⊢ M ⁻ ⇓ nf M ⁻ ∷ A`.
-- We then prove that if a proof tree `M` erases to a well-typed term `t`, then `t ⇓ nf M ⁻`.  Now,
-- if two proof trees `M` and `N` erase to the same well-typed term `t`, then `t ⇓ nf M ⁻` and
-- `t ⇓ nf N ⁻`.  Since the reduction is deterministic we have that `nf M ⁻` and `nf N ⁻` are the
-- same, and hence `M ≅ N`.  The idea of this proof comes from Streicher [19] (chapter IV).

-- 6.1. Definition of terms
-- ------------------------
--
-- We mutually define the set of terms, `𝕋 : Set`, and substitutions, `𝕊 : Set`.  (…)

mutual
  data 𝕋 : Set where
    ν   : Name → 𝕋
    ƛ   : Name → 𝕋 → 𝕋
    _∙_ : 𝕋 → 𝕋 → 𝕋
    _▶_ : 𝕋 → 𝕊 → 𝕋

  data 𝕊 : Set where
    []      : 𝕊
    [_,_≔_] : 𝕊 → Name → 𝕋 → 𝕊
    _●_     : 𝕊 → 𝕊 → 𝕊

-- 6.2. Typing rules
-- -----------------
--
-- We give the typing rules for terms and substitutions mutually inductively.  (…)

mutual
  infix 3 _⊢_∷_
  data _⊢_∷_ : 𝒞 → 𝕋 → 𝒯 → Set where
    ↑⟨_⟩⊢∷ : ∀ {Γ Δ A t} →
                Γ ⊇ Δ → Δ ⊢ t ∷ A →
                Γ ⊢ t ∷ A
    ν       : ∀ {Γ A} →
                (x : Name) → Γ ∋ x ∷ A →
                Γ ⊢ ν x ∷ A
    ƛ       : ∀ {Γ A B t} →
                (x : Name) {{_ : T (fresh x Γ)}} → [ Γ , x ∷ A ] ⊢ t ∷ B →
                Γ ⊢ ƛ x t ∷ A ⊃ B
    _∙_     : ∀ {Γ A B t₁ t₂} →
                Γ ⊢ t₁ ∷ A ⊃ B → Γ ⊢ t₂ ∷ A →
                Γ ⊢ t₁ ∙ t₂ ∷ B
    _▶_     : ∀ {Γ Δ A s t} →
                Δ ⊢ t ∷ A → Γ ⋙ s ∷ Δ →
                Γ ⊢ t ▶ s ∷ A

  infix 3 _⋙_∷_
  data _⋙_∷_ : 𝒞 → 𝕊 → 𝒞 → Set where
    ↑⟨_⟩⋙∷ : ∀ {Γ Δ Θ s} →
                Θ ⊇ Γ → Γ ⋙ s ∷ Δ →
                Θ ⋙ s ∷ Δ
    ↓⟨_⟩⋙∷ : ∀ {Γ Δ Θ s} →
                Δ ⊇ Θ → Γ ⋙ s ∷ Δ →
                Γ ⋙ s ∷ Θ
    refl⋙∷ : ∀ {Γ} →
                Γ ⋙ [] ∷ Γ
    [_,_≔_] : ∀ {Γ Δ A s t} →
                Γ ⋙ s ∷ Δ → (x : Name) {{_ : T (fresh x Δ)}} → Γ ⊢ t ∷ A →
                Γ ⋙ [ s , x ≔ t ] ∷ [ Δ , x ∷ A ]
    _●_     : ∀ {Γ Δ Θ s₁ s₂} →
                Δ ⋙ s₂ ∷ Θ → Γ ⋙ s₁ ∷ Δ →
                Γ ⋙ s₂ ● s₁ ∷ Θ

module _ where
  instance
    raise⊢∷ : ∀ {A t} → Raiseable (_⊢ t ∷ A)
    raise⊢∷ = record { ↑⟨_⟩ = ↑⟨_⟩⊢∷ }

    raise⋙∷ : ∀ {Γ s} → Raiseable (_⋙ s ∷ Γ)
    raise⋙∷ = record { ↑⟨_⟩ = ↑⟨_⟩⋙∷ }

    lower⋙∷ : ∀ {Δ s} → Lowerable (Δ ⋙ s ∷_)
    lower⋙∷ = record { ↓⟨_⟩ = ↓⟨_⟩⋙∷ }

-- 6.3. Convertibility of terms
-- ----------------------------
--
-- We mutually inductively define when two terms are convertible with each other together
-- with the definition of convertibility between substitutions.  (…)

mutual
  infix 3 _⊢_≊_∷_
  data _⊢_≊_∷_ : 𝒞 → 𝕋 → 𝕋 → 𝒯 → Set where
    refl≊  : ∀ {Γ A t} →
               Γ ⊢ t ≊ t ∷ A
    sym≊   : ∀ {Γ A t t′} →
               Γ ⊢ t ≊ t′ ∷ A →
               Γ ⊢ t′ ≊ t ∷ A
    trans≊ : ∀ {Γ A t t′ t″} →
               Γ ⊢ t ≊ t′ ∷ A → Γ ⊢ t′ ≊ t″ ∷ A →
               Γ ⊢ t ≊ t″ ∷ A

    congƛ≊ : ∀ {Γ A B t t′ x} {{_ : T (fresh x Γ)}} →
               [ Γ , x ∷ A ] ⊢ t ≊ t′ ∷ B →
               Γ ⊢ ƛ x t ≊ ƛ x t′ ∷ A ⊃ B
    cong∙≊ : ∀ {Γ A B t t′ u u′} →
               Γ ⊢ t ≊ t′ ∷ A ⊃ B → Γ ⊢ u ≊ u′ ∷ A →
               Γ ⊢ t ∙ u ≊ t′ ∙ u′ ∷ B
    cong▶≊ : ∀ {Γ Δ A t t′ s s′} →
               Γ ⊢ t ≊ t′ ∷ A → Δ ⋙ s ≊ₛ s′ ∷ Γ →
               Γ ⊢ t ▶ s ≊ t′ ▶ s′ ∷ A

    conv₁≊ : ∀ {Γ A t} →
               Γ ⊢ t ∷ A →
               Γ ⊢ t ≊ t ∷ A
    conv₂≊ : ∀ {Γ Δ A B s t₁ t₂ x} {{_ : T (fresh x Δ)}} →
               Γ ⋙ s ∷ Δ → [ Δ , x ∷ A ] ⊢ t₁ ∷ B → Γ ⊢ t₂ ∷ A →
               Γ ⊢ (ƛ x t₁ ▶ s) ∙ t₂ ≊ t₁ ▶ [ s , x ≔ t₂ ] ∷ B
    conv₃≊ : ∀ {Γ A B t x} {{_ : T (fresh x Γ)}} →
               Γ ⊢ t ∷ A ⊃ B →
               Γ ⊢ t ≊ ƛ x (t ∙ ν x) ∷ A ⊃ B
    conv₄≊ : ∀ {Γ Δ A t₁ t₂} →
               Γ ⊇ Δ → Δ ⊢ t₁ ≊ t₂ ∷ A →
               Γ ⊢ t₁ ≊ t₂ ∷ A
    conv₅≊ : ∀ {Γ Δ A s t x} {{_ : T (fresh x Δ)}} →
               Γ ⋙ s ∷ Δ → Γ ⊢ t ∷ A →
               Γ ⊢ ν x ▶ [ s , x ≔ t ] ≊ t ∷ A
    conv₆≊ : ∀ {Γ A t} →
               Γ ⊢ t ∷ A →
               Γ ⊢ t ▶ [] ≊ t ∷ A
    conv₇≊ : ∀ {Γ Δ A B s t₁ t₂} →
               Δ ⊢ t₁ ∷ A ⊃ B → Δ ⊢ t₂ ∷ A → Γ ⋙ s ∷ Δ →
               Γ ⊢ (t₁ ∙ t₂) ▶ s ≊ (t₁ ▶ s) ∙ (t₂ ▶ s) ∷ B
    conv₈≊ : ∀ {Γ₁ Γ₂ Γ₃ A s₁ s₂ t} →
               Γ₂ ⋙ s₁ ∷ Γ₃ → Γ₁ ⋙ s₂ ∷ Γ₂ → Γ₃ ⊢ t ∷ A →
               Γ₁ ⊢ (t ▶ s₁) ▶ s₂ ≊ t ▶ (s₁ ● s₂) ∷ A

  data _⋙_≊ₛ_∷_ : 𝒞 → 𝕊 → 𝕊 → 𝒞 → Set where
    refl≊ₛ  : ∀ {Γ Δ s} →
                Δ ⋙ s ≊ₛ s ∷ Γ
    sym≊ₛ   : ∀ {Γ Δ s s′} →
                Δ ⋙ s ≊ₛ s′ ∷ Γ →
                Δ ⋙ s′ ≊ₛ s ∷ Γ
    trans≊ₛ : ∀ {Γ Δ s s′ s″} →
                Δ ⋙ s ≊ₛ s′ ∷ Γ → Δ ⋙ s′ ≊ₛ s″ ∷ Γ →
                Δ ⋙ s ≊ₛ s″ ∷ Γ

    cong≔≊ₛ : ∀ {Γ Δ A s s′ t t′ x} {{_ : T (fresh x Δ)}} →
                Γ ⋙ s ≊ₛ s′ ∷ Δ → Γ ⊢ t ≊ t′ ∷ A →
                Γ ⋙ [ s , x ≔ t ] ≊ₛ [ s′ , x ≔ t′ ] ∷ [ Δ , x ∷ A ]
    cong●≊ₛ : ∀ {Γ Δ Θ s₁ s₁′ s₂ s₂′} →
                Δ ⋙ s₂ ≊ₛ s₂′ ∷ Θ → Γ ⋙ s₁ ≊ₛ s₁′ ∷ Δ →
                Γ ⋙ s₂ ● s₁ ≊ₛ s₂′ ● s₁′ ∷ Θ

    conv₁≊ₛ : ∀ {Γ₁ Γ₂ Δ s₁ s₂} →
                Γ₁ ⊇ Γ₂ → Γ₂ ⋙ s₁ ≊ₛ s₂ ∷ Δ →
                Γ₁ ⋙ s₁ ≊ₛ s₂ ∷ Δ
    conv₂≊ₛ : ∀ {Γ Δ₁ Δ₂ s₁ s₂} →
                Δ₁ ⊇ Δ₂ → Γ ⋙ s₁ ≊ₛ s₂ ∷ Δ₁ →
                Γ ⋙ s₁ ≊ₛ s₂ ∷ Δ₂
    conv₃≊ₛ : ∀ {Γ Δ s} →
                Γ ⋙ s ∷ Δ →
                Γ ⋙ s ● [] ≊ₛ s ∷ Δ
    conv₄≊ₛ : ∀ {Γ₁ Γ₂ Γ₃ Δ s₁ s₂ s₃} →
                Γ₁ ⋙ s₃ ∷ Γ₂ → Γ₂ ⋙ s₂ ∷ Γ₃ → Γ₃ ⋙ s₁ ∷ Δ →
                Γ₃ ⋙ (s₁ ● s₂) ● s₃ ≊ₛ s₁ ● (s₂ ● s₃) ∷ Δ
    conv₅≊ₛ : ∀ {Γ₁ Γ₂ Δ A s₁ s₂ t x} {{_ : T (fresh x Δ)}} →
                Γ₁ ⋙ s₂ ∷ Γ₂ → Γ₂ ⋙ s₁ ∷ Δ → Γ₂ ⊢ t ∷ A →
                Γ₁ ⋙ [ s₁ , x ≔ t ] ● s₂ ≊ₛ [ s₁ ● s₂ , x ≔ t ▶ s₂ ] ∷ [ Δ , x ∷ A ]
    conv₆≊ₛ : ∀ {Γ s} →
                Γ ⋙ s ∷ [] →
                Γ ⋙ s ≊ₛ [] ∷ []
    conv₇≊ₛ : ∀ {Γ Δ A s x} {{_ : T (fresh x Δ)}} →
                Γ ⋙ s ∷ [ Δ , x ∷ A ] →
                Γ ⋙ s ≊ₛ [ s , x ≔ ν x ▶ s ] ∷ [ Δ , x ∷ A ]
    conv₈≊ₛ : ∀ {Γ Δ A s t x} {{_ : T (fresh x Δ)}} →
                Γ ⋙ s ∷ Δ → Δ ⊢ t ∷ A →
                Γ ⋙ [ s , x ≔ t ] ≊ₛ s ∷ Δ
    conv₉≊ₛ : ∀ {Γ Δ s} →
                Γ ⋙ s ∷ Δ →
                Γ ⋙ [] ● s ≊ₛ s ∷ Δ

-- It is straightforward to prove that if two terms (substitutions) are convertible with each
-- other, then they are also well-typed.

-- TODO: What to do about the above paragraph?

max_stars_repo_name: mietek/coquand

max_issues_repo_name: mietek/coquand

max_forks_repo_name: mietek/coquand


text:
{-# OPTIONS --cubical #-}
module _ where

module _ where
  import Agda.Primitive
  open import Agda.Primitive.Cubical public
  open import Agda.Builtin.Cubical.Path public

  refl : ∀ {a} {A : Set a} {x : A} → x ≡ x
  refl {x = x} = \ _ → x

testPath : ∀ {A : Set} {b a : A} (let H : b ≡ b; H = _) → ∀ i → H i ≡ b
testPath i = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Type.Cubical where

import      Lvl
open import Type

open import Agda.Primitive public
  using (SSet)

open import Agda.Primitive.Cubical public
  using ()
  renaming (I to Interval) -- _ : SSet(Lvl.𝟎). Inhabitants can be seen as points on a closed unit interval.

module Interval where
  open Agda.Primitive.Cubical public
    using (
      Partial ; -- _ : ∀{ℓ} → Interval → Type{ℓ} → SSet(ℓ)
      PartialP -- _ : ∀{ℓ} → (i : Interval) → (.(Is-𝟏 i) → Type{ℓ}) → SSet(ℓ)
    )
    renaming (
      i0 to 𝟎 ; -- _ : Interval. 0 (the initial point) in the interval.
      i1 to 𝟏 ; -- _ : Interval. 1 (the terminal point) in the interval.
      primIMin to min ; -- _ : Interval → Interval → Interval. Chooses the point nearest 𝟎. Also called: _∧_ (from lattice structure).
      primIMax to max ; -- _ : Interval → Interval → Interval. Chooses the point nearest 𝟏. Also called: _∨_ (from lattice structure).
      primINeg to flip ; -- _ : Interval → Interval. Flips a point in the interval around the point of symmetry (the middle). Essentially (p ↦ 𝟏 − p).
      IsOne to Is-𝟏 ; -- _ : Interval → SSet(Lvl.𝟎). The predicate stating that a point is 𝟏.
      itIsOne to 𝟏-is-𝟏 ; -- _ : Is-𝟏(𝟏). Proof of 𝟏 being 𝟏.
      primComp to comp ; -- _ : ∀{ℓ : Interval → Lvl.Level} → (P : (i : Interval) → Type{ℓ(i)}) → ∀{i : Interval} → ((j : Interval) → .(Is-𝟏 i) → P(j)) → (P(𝟎) → P(𝟏))
      primHComp to hComp ; -- _ : ∀{ℓ}{A : Type{ℓ}}{i : Interval} → (Interval → .(Is-𝟏 i) → A) → (A → A)
      primTransp to transp -- _ : ∀{ℓ : Interval → Lvl.Level}(A : (i : Interval) → Type{ℓ(i)}) → Interval → A(𝟎)→ A(𝟏).
    )

  -- The distance to the nearest boundary.
  nearBound : Interval → Interval
  nearBound x = min x (flip x)

  -- The distance to the furthest boundary.
  farBound : Interval → Interval
  farBound x = max x (flip x)

  -- Proof of maximum of 𝟏 being 𝟏.
  maxₗ-is-𝟏 : ∀{x y} → Is-𝟏(x) → Is-𝟏(max x y)
  maxₗ-is-𝟏 {x}{y} = Agda.Primitive.Cubical.IsOne1 x y

  -- Proof of maximum of 𝟏 being 𝟏.
  maxᵣ-is-𝟏 : ∀{x y} → Is-𝟏(y) → Is-𝟏(max x y)
  maxᵣ-is-𝟏 {x}{y} = Agda.Primitive.Cubical.IsOne2 x y

  -- The predicate stating that a point is 𝟎.
  Is-𝟎 : Interval → SSet(Lvl.𝟎)
  Is-𝟎 i = Is-𝟏(flip i)

  -- Proof of 𝟎 being 𝟎.
  𝟎-is-𝟎 : Is-𝟎(𝟎)
  𝟎-is-𝟎 = 𝟏-is-𝟏

  -- Proof of minimum of 𝟎 being 𝟎.
  minₗ-is-𝟎 : ∀{x y} → Is-𝟎(x) → Is-𝟎(min x y)
  minₗ-is-𝟎 {x}{y} = maxₗ-is-𝟏 {flip x} {flip y}

  -- Proof of minimum of 𝟎 being 𝟎.
  minᵣ-is-𝟎 : ∀{x y} → Is-𝟎(y) → Is-𝟎(min x y)
  minᵣ-is-𝟎 {x}{y} = maxᵣ-is-𝟏 {flip x} {flip y}

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:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Incrementalization as term-to-term transformation (Fig. 4g).
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type
import Parametric.Syntax.Term as Term
import Parametric.Change.Type as ChangeType

module Parametric.Change.Derive
    {Base : Type.Structure}
    (Const : Term.Structure Base)
    (ΔBase : ChangeType.Structure Base)
  where

open Type.Structure Base
open Term.Structure Base Const
open ChangeType.Structure Base ΔBase

-- Extension point: Incrementalization of primitives.
Structure : Set
Structure = ∀ {τ} →
  Const τ →
  Term ∅ (ΔType τ)

module Structure (derive-const : Structure) where
  fit : ∀ {τ Γ} → Term Γ τ → Term (ΔContext Γ) τ
  fit = weaken Γ≼ΔΓ

  -- In the paper, we transform "x" to "dx". Here, we work with
  -- de Bruijn indices, so we have to manipulate the indices to
  -- account for a bigger context after transformation.
  deriveVar : ∀ {τ Γ} → Var Γ τ → Var (ΔContext Γ) (ΔType τ)
  deriveVar this = this
  deriveVar (that x) = that (that (deriveVar x))

  -- We provide: Incrementalization of arbitrary terms.
  derive : ∀ {τ Γ} → Term Γ τ → Term (ΔContext Γ) (ΔType τ)
  derive (var x) = var (deriveVar x)
  derive (app s t) = app (app (derive s) (fit t)) (derive t)
  derive (abs t) = abs (abs (derive t))
  derive {Γ = Γ} (const c) = weaken (∅≼Γ {ΔContext Γ}) (derive-const c)

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:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Impl.OBM.Rust.RustTypes
open import Util.ByteString

module LibraBFT.Impl.OBM.ConfigHardCoded where

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

postulate -- TODO-1 ePOCHCHANGE
  ePOCHCHANGE : ByteString
--ePOCHCHANGE = "EPOCHCHANGE"

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

maxPrunedBlocksInMem : Usize
maxPrunedBlocksInMem = 10

roundInitialTimeoutMS : U64
roundInitialTimeoutMS = 3000

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


text:
{- Auxiliary functions for temporal operators. -}
module TemporalOps.Common where

open import TemporalOps.Common.Rewriting public
open import TemporalOps.Common.Compare public
open import TemporalOps.Common.Other public

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
open import Level
open import Relation.Binary.PropositionalEquality
open import Relation.Binary using (Setoid)
import Function.Equality
import Relation.Binary.Reasoning.Setoid as SetoidR

import Categories.Category
import Categories.Functor
import Categories.NaturalTransformation
import Categories.Category.Instance.Setoids

import Categories.Category.Cocartesian

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.Term
import SecondOrder.VRenaming

module SecondOrder.MRenaming
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Signature.Signature Σ
  open SecondOrder.Metavariable Σ
  open SecondOrder.Term Σ
  open SecondOrder.VRenaming Σ

  -- a metarenaming maps metavariables between contexts in an arity-preserving way
  _⇒ᵐ_ : ∀ (Θ ψ : MContext) → Set ℓ
  Θ ⇒ᵐ ψ = ∀ {Δ A} → [ Δ , A ]∈ Θ → [ Δ , A ]∈ ψ

  infix 4 _⇒ᵐ_

  -- equality of metarenamings

  _≡ᵐ_ : ∀ {Θ ψ} (ι μ : Θ ⇒ᵐ ψ) → Set ℓ
  _≡ᵐ_ {Θ} ι μ = ∀ {Δ A} (M : [ Δ , A ]∈ Θ) → ι M ≡ μ M

  infixl 3 _≡ᵐ_

  ≡ᵐ-refl : ∀ {Θ ψ} {ι : Θ ⇒ᵐ ψ} → ι ≡ᵐ ι
  ≡ᵐ-refl = λ M → refl

  ≡ᵐ-sym : ∀ {Θ ψ} {ι μ : Θ ⇒ᵐ ψ}
          → ι ≡ᵐ μ
          → μ ≡ᵐ ι
  ≡ᵐ-sym eq M = sym (eq M)

  ≡ᵐ-trans : ∀ {Θ ψ} {ι μ δ : Θ ⇒ᵐ ψ}
           → ι ≡ᵐ μ
           → μ ≡ᵐ δ
           → ι ≡ᵐ δ
  ≡ᵐ-trans eq1 eq2 M = trans (eq1 M) (eq2 M)

  -- meta-variable renamings form a setoid

  Mrenaming-setoid : ∀ (Θ ψ : MContext) → Setoid ℓ ℓ
  Mrenaming-setoid Θ ψ =
    record
      { Carrier = Θ ⇒ᵐ ψ
      ;  _≈_ = λ ι μ → ι ≡ᵐ μ
      ; isEquivalence =
                      record
                        { refl = λ {ι} M → ≡ᵐ-refl {Θ} {ψ} {ι} M
                        ; sym = ≡ᵐ-sym
                        ; trans = ≡ᵐ-trans
                        }
      }

  -- the identity renaming

  idᵐ : ∀ {Θ : MContext} → Θ ⇒ᵐ Θ
  idᵐ M = M

  -- equal metavariable renaming act the same on metavariables

  -- composition of renamings
  _∘ᵐ_ : ∀ {Θ ψ Ω} → ψ ⇒ᵐ Ω → Θ ⇒ᵐ ψ → Θ ⇒ᵐ Ω
  (ι ∘ᵐ μ) M = ι (μ M)

  infix 7 _∘ᵐ_

  -- composition respects equality
  ∘ᵐ-resp-≡ᵐ : ∀ {Γ Δ Ξ} {τ₁ τ₂ : Δ ⇒ᵐ Ξ} {σ₁ σ₂ : Γ ⇒ᵐ Δ} →
                 τ₁ ≡ᵐ τ₂ → σ₁ ≡ᵐ σ₂ → τ₁ ∘ᵐ σ₁ ≡ᵐ τ₂ ∘ᵐ σ₂
  ∘ᵐ-resp-≡ᵐ {τ₁ = τ₁} {σ₂ = σ₂} ζ ξ x = trans (cong τ₁ (ξ x)) (ζ (σ₂ x))

  -- the identity is the unit

  identity-leftᵐ : ∀ {Γ Δ} {ρ : Γ ⇒ᵐ Δ} → idᵐ ∘ᵐ ρ ≡ᵐ ρ
  identity-leftᵐ ρ = refl

  identity-rightᵐ : ∀ {Γ Δ} {ρ : Γ ⇒ᵐ Δ} → ρ ∘ᵐ idᵐ ≡ᵐ ρ
  identity-rightᵐ ρ = refl

  -- composition is associative

  assocᵐ : ∀ {Γ Δ Ξ Ψ} {τ : Γ ⇒ᵐ Δ} {ρ : Δ ⇒ᵐ Ξ} {σ : Ξ ⇒ᵐ Ψ} →
             (σ ∘ᵐ ρ) ∘ᵐ τ ≡ᵐ σ ∘ᵐ (ρ ∘ᵐ τ)
  assocᵐ x = refl

  sym-assocᵐ : ∀ {Γ Δ Ξ Ψ} {τ : Γ ⇒ᵐ Δ} {ρ : Δ ⇒ᵐ Ξ} {σ : Ξ ⇒ᵐ Ψ} →
             σ ∘ᵐ (ρ ∘ᵐ τ) ≡ᵐ (σ ∘ᵐ ρ) ∘ᵐ τ
  sym-assocᵐ x = refl

  -- contexts and renamings form a category
  module _ where
    open Categories.Category

    MContexts : Category ℓ ℓ ℓ
    MContexts =
      record
        { Obj = MContext
        ; _⇒_ = _⇒ᵐ_
        ; _≈_ = _≡ᵐ_
        ; id = idᵐ
        ; _∘_ = _∘ᵐ_
        ; assoc = λ {_} {_} {_} {_} {f} {g} {h} {_} → assocᵐ {τ = f} {ρ = g} {σ = h}
        ; sym-assoc = λ {_} {_} {_} {_} {f} {g} {h} {_} → sym-assocᵐ {τ = f} {ρ = g} {σ = h}
        ; identityˡ = λ x → refl
        ; identityʳ = λ x → refl
        ; identity² = λ x → refl
        ; equiv = record { refl = λ {ι} {_} → ≡ᵐ-refl {ι = ι} ; sym = ≡ᵐ-sym ; trans = ≡ᵐ-trans }
        ; ∘-resp-≈ = ∘ᵐ-resp-≡ᵐ
        }

  -- the coproduct structure of the category
  module _ where

    infixl 7 [_,_]ᵐ

    [_,_]ᵐ : ∀ {Γ Δ Ξ} → Γ ⇒ᵐ Ξ → Δ ⇒ᵐ Ξ → Γ ,, Δ ⇒ᵐ Ξ
    [ σ , τ ]ᵐ (var-inl x) = σ x
    [ σ , τ ]ᵐ (var-inr y) = τ y

    inlᵐ : ∀ {Γ Δ} → Γ ⇒ᵐ Γ ,, Δ
    inlᵐ = var-inl

    inrᵐ : ∀ {Γ Δ} → Δ ⇒ᵐ Γ ,, Δ
    inrᵐ = var-inr

    uniqueᵐ : ∀ {Γ Δ Ξ} {τ : Γ ,, Δ ⇒ᵐ Ξ} {ρ : Γ ⇒ᵐ Ξ} {σ : Δ ⇒ᵐ Ξ}
              → τ ∘ᵐ inlᵐ ≡ᵐ ρ
              → τ ∘ᵐ inrᵐ ≡ᵐ σ
              → [ ρ , σ ]ᵐ ≡ᵐ τ
    uniqueᵐ ξ ζ (var-inl x) = sym (ξ x)
    uniqueᵐ ξ ζ (var-inr y) = sym (ζ y)

    MContext-+ : Categories.Category.Cocartesian.BinaryCoproducts MContexts
    MContext-+ =
      record {
        coproduct =
          λ {Γ Δ} →
          record
            { A+B = Γ ,, Δ
            ; i₁ = inlᵐ
            ; i₂ = inrᵐ
            ; [_,_] = [_,_]ᵐ
            ; inject₁ = λ x → refl
            ; inject₂ = λ x → refl
            ; unique = uniqueᵐ
            }
      }

  open Categories.Category.Cocartesian.BinaryCoproducts MContext-+

  -- the renaming from the empty context

  inᵐ : ∀ {Γ} → ctx-empty ⇒ᵐ Γ
  inᵐ ()

  -- extension of a renaming is summing with identity
  ⇑ᵐ : ∀ {Θ Ψ Ω} → Θ ⇒ᵐ Ψ → Θ ,, Ω ⇒ᵐ Ψ ,, Ω
  ⇑ᵐ ρ = ρ +₁ idᵐ

  -- a renaming can also be extended on the right
  ᵐ⇑ᵐ : ∀ {Θ Ψ} → Θ ⇒ᵐ Ψ → ∀ {Ω} → Ω ,, Θ ⇒ᵐ Ω ,, Ψ
  ᵐ⇑ᵐ ρ = idᵐ +₁ ρ

  -- the action of a metavariable renaming on terms
  infix 6 [_]ᵐ_

  [_]ᵐ_ : ∀ {Θ Ψ Γ A} → Θ ⇒ᵐ Ψ → Term Θ Γ A → Term Ψ Γ A
  [ ι ]ᵐ (tm-var x) = tm-var x
  [ ι ]ᵐ (tm-meta M ts) = tm-meta (ι M) (λ i → [ ι ]ᵐ ts i)
  [ ι ]ᵐ (tm-oper f es) = tm-oper f (λ i → [ ι ]ᵐ es i)

  -- The sum of identities is an identity
  idᵐ+idᵐ : ∀ {Θ Ψ} → idᵐ {Θ = Θ} +₁ idᵐ {Θ = Ψ} ≡ᵐ idᵐ {Θ = Θ ,, Ψ}
  idᵐ+idᵐ (var-inl x) = refl
  idᵐ+idᵐ (var-inr y) = refl

  -- The action of a renaming respects equality of terms
  []ᵐ-resp-≈ : ∀ {Θ Ψ Γ A} {s t : Term Θ Γ A} {ι : Θ ⇒ᵐ Ψ} → s ≈ t → [ ι ]ᵐ s ≈ [ ι ]ᵐ t
  []ᵐ-resp-≈ (≈-≡ refl) = ≈-≡ refl
  []ᵐ-resp-≈ (≈-meta ξ) = ≈-meta (λ i → []ᵐ-resp-≈ (ξ i))
  []ᵐ-resp-≈ (≈-oper ξ) = ≈-oper (λ i → []ᵐ-resp-≈ (ξ i))

  -- The action of a renaming respects equality of renamings
  []ᵐ-resp-≡ᵐ : ∀ {Θ Ψ Γ A} {ι μ : Θ ⇒ᵐ Ψ} {t : Term Θ Γ A} → ι ≡ᵐ μ → [ ι ]ᵐ t ≈ [ μ ]ᵐ t
  []ᵐ-resp-≡ᵐ {t = tm-var x} ξ = ≈-≡ refl
  []ᵐ-resp-≡ᵐ {Θ} {Ψ} {Γ} {A} {ι = ι} {μ = μ} {t = tm-meta M ts} ξ =
    let open SetoidR (Term-setoid Ψ Γ A) in
    begin
    tm-meta (ι M) (λ i → [ ι ]ᵐ ts i) ≈⟨ ≈-meta (λ i → []ᵐ-resp-≡ᵐ ξ) ⟩
    tm-meta (ι M) (λ i → [ μ ]ᵐ ts i) ≈⟨ ≈-≡ ((cong λ N → tm-meta N (λ i → [ μ ]ᵐ ts i)) (ξ M)) ⟩
    tm-meta (μ M) (λ i → [ μ ]ᵐ ts i) ≈⟨ ≈-≡ refl ⟩
    tm-meta (μ M) (λ i → [ μ ]ᵐ ts i)
    ∎
  []ᵐ-resp-≡ᵐ {t = tm-oper f es} ξ = ≈-oper λ i → []ᵐ-resp-≡ᵐ ξ

  -- The action of the identity is trival
  [idᵐ] : ∀ {Θ Γ A} {t : Term Θ Γ A} → [ idᵐ ]ᵐ t ≈ t
  [idᵐ] {t = tm-var x} = ≈-refl
  [idᵐ] {t = tm-meta M ts} = ≈-meta λ i → [idᵐ]
  [idᵐ] {t = tm-oper f es} = ≈-oper λ i → [idᵐ]

  -- Extension respects composition
  ⇑ᵐ-resp-∘ᵐ : ∀ {Γ Δ Ξ Ψ} {ρ : Γ ⇒ᵐ Δ} {τ : Δ ⇒ᵐ Ξ} → ⇑ᵐ {Ω = Ψ} (τ ∘ᵐ ρ) ≡ᵐ (⇑ᵐ τ) ∘ᵐ (⇑ᵐ ρ)
  ⇑ᵐ-resp-∘ᵐ (var-inl x) = refl
  ⇑ᵐ-resp-∘ᵐ (var-inr y) = refl

  ᵐ⇑ᵐ-resp-∘ᵐ : ∀ {Θ Ψ Ω Ξ} {ρ : Θ ⇒ᵐ Ψ} {τ : Ψ ⇒ᵐ Ω}
    → ᵐ⇑ᵐ {Θ} {Ω} (τ ∘ᵐ ρ) {Ξ} ≡ᵐ (ᵐ⇑ᵐ τ) ∘ᵐ (ᵐ⇑ᵐ ρ)
  ᵐ⇑ᵐ-resp-∘ᵐ (var-inl M) = refl
  ᵐ⇑ᵐ-resp-∘ᵐ (var-inr N) = refl

  -- Extension of the identity renaming is the identity
  ⇑ᵐ-resp-idᵐ : ∀ {Θ Ψ} → (⇑ᵐ {Θ} {Θ} {Ψ}) (idᵐ {Θ}) ≡ᵐ idᵐ
  ⇑ᵐ-resp-idᵐ (var-inl M) = refl
  ⇑ᵐ-resp-idᵐ (var-inr N) = refl

  ᵐ⇑ᵐ-resp-idᵐ : ∀ {Θ Ψ} → (ᵐ⇑ᵐ {Θ} {Θ}) (idᵐ {Θ}) {Ψ} ≡ᵐ idᵐ
  ᵐ⇑ᵐ-resp-idᵐ (var-inl M) = refl
  ᵐ⇑ᵐ-resp-idᵐ (var-inr N) = refl

  -- Extension preserves equality of metavariable renamings
  ᵐ⇑ᵐ-resp-≡ᵐ : ∀ {Θ Ψ Ω} {ι μ : Θ ⇒ᵐ Ψ} → ι ≡ᵐ μ → ᵐ⇑ᵐ ι {Ω} ≡ᵐ ᵐ⇑ᵐ μ
  ᵐ⇑ᵐ-resp-≡ᵐ ι≡μ (var-inl M) = refl
  ᵐ⇑ᵐ-resp-≡ᵐ {ι = ι} ι≡μ (var-inr N) = cong (inrᵐ) (ι≡μ N)

  ⇑ᵐ-resp-≡ᵐ : ∀ {Θ Ψ Ω} {ι μ : Θ ⇒ᵐ Ψ} → ι ≡ᵐ μ → ⇑ᵐ {Ω = Ω} ι ≡ᵐ ⇑ᵐ μ
  ⇑ᵐ-resp-≡ᵐ ι≡μ (var-inl M) = cong var-inl (ι≡μ M)
  ⇑ᵐ-resp-≡ᵐ {ι = ι} ι≡μ (var-inr N) = refl

  -- The action of a renaming is functorial
  [∘ᵐ] : ∀ {Θ Ψ Ω Γ} {ι : Θ ⇒ᵐ Ψ} {μ : Ψ ⇒ᵐ Ω} {A} {t : Term Θ Γ A}
    → [ μ ∘ᵐ ι ]ᵐ t ≈ [ μ ]ᵐ ([ ι ]ᵐ t)
  [∘ᵐ] {t = tm-var x} = ≈-refl
  [∘ᵐ] {t = tm-meta M ts} = ≈-meta (λ i → [∘ᵐ])
  [∘ᵐ] {t = tm-oper f es} = ≈-oper (λ i → [∘ᵐ])

  ᵐ∘ᵛ≈ᵛ∘ᵐ : ∀ {Θ Ψ Γ Δ A} {ρ : Γ ⇒ᵛ Δ} {ι : Θ ⇒ᵐ Ψ} {t : Term Θ Γ A}
    → [ ι ]ᵐ ([ ρ ]ᵛ t) ≈ [ ρ ]ᵛ ([ ι ]ᵐ t)
  ᵐ∘ᵛ≈ᵛ∘ᵐ {t = tm-var x} = ≈-refl
  ᵐ∘ᵛ≈ᵛ∘ᵐ {t = tm-meta M ts} = ≈-meta (λ i → ᵐ∘ᵛ≈ᵛ∘ᵐ {t = ts i})
  ᵐ∘ᵛ≈ᵛ∘ᵐ {t = tm-oper f es} = ≈-oper (λ i → ᵐ∘ᵛ≈ᵛ∘ᵐ {t = es i})

  split-sum : ∀ {Θ Ψ Ξ Ω} {ι : Θ ⇒ᵐ Ψ} {μ : Ξ ⇒ᵐ Ω}
    → (μ +₁ ι) ≡ᵐ (⇑ᵐ μ) ∘ᵐ (ᵐ⇑ᵐ ι)
  split-sum (var-inl M) = refl
  split-sum (var-inr N) = refl

  split-sum2 : ∀ {Θ Ψ Ξ Ω} {ι : Θ ⇒ᵐ Ψ} {μ : Ξ ⇒ᵐ Ω}
    → (μ +₁ ι) ≡ᵐ (ᵐ⇑ᵐ ι) ∘ᵐ (⇑ᵐ μ)
  split-sum2 (var-inl M) = refl
  split-sum2 (var-inr N) = refl

  ⇑-resp-+ : ∀ {Θ Ψ Ξ Ω Γ A} {ι : Θ ⇒ᵐ Ψ} {μ : Ξ ⇒ᵐ Ω} {t : Term (Ξ + Θ) Γ A}
    → [ (⇑ᵐ μ) ]ᵐ ([ (ᵐ⇑ᵐ ι) ]ᵐ t) ≈ [ (ᵐ⇑ᵐ ι) ]ᵐ ([ (⇑ᵐ μ) ]ᵐ t)
  ⇑-resp-+ {Θ} {Ψ} {Ξ} {Ω} {Γ} {A} {ι} {μ} {t = t} =
    let open SetoidR (Term-setoid (Ω ,, Ψ) Γ A) in
    begin
    [ ⇑ᵐ μ ]ᵐ ([ ᵐ⇑ᵐ ι ]ᵐ t) ≈⟨ ≈-sym [∘ᵐ] ⟩
    [ (⇑ᵐ μ) ∘ᵐ (ᵐ⇑ᵐ ι) ]ᵐ t  ≈⟨ ≈-sym ([]ᵐ-resp-≡ᵐ split-sum) ⟩
    [ (μ +₁ ι) ]ᵐ t ≈⟨ []ᵐ-resp-≡ᵐ split-sum2 ⟩
    [(ᵐ⇑ᵐ ι) ∘ᵐ (⇑ᵐ μ)  ]ᵐ t ≈⟨ [∘ᵐ] ⟩
    [ ᵐ⇑ᵐ ι ]ᵐ ([ ⇑ᵐ μ ]ᵐ t)
    ∎

  ∘ᵐ-resp-⇑ : ∀ {Θ Ψ Ξ Ω} {ι : Θ ⇒ᵐ Ψ} {μ : Ψ ⇒ᵐ Ω}
    → ⇑ᵐ {Ω = Ξ}  (μ ∘ᵐ ι) ≡ᵐ ⇑ᵐ μ ∘ᵐ ⇑ᵐ ι
  ∘ᵐ-resp-⇑ (var-inl M) = refl
  ∘ᵐ-resp-⇑ (var-inr N) = refl

  ∘ᵐ-resp-⇑-term : ∀ {Θ Ψ Ξ Ω Γ A} {ι : Θ ⇒ᵐ Ψ} {μ : Ψ ⇒ᵐ Ω} {t : Term (Θ ,, Ξ) Γ A}
    → [ ⇑ᵐ {Ω = Ξ} (μ ∘ᵐ ι) ]ᵐ t ≈  [ ⇑ᵐ μ ]ᵐ ([ ⇑ᵐ ι ]ᵐ t)
  ∘ᵐ-resp-⇑-term {Θ} {Ψ} {Ξ} {Ω} {Γ} {A} {ι} {μ} {t = t} =
      let open SetoidR (Term-setoid (Ω ,, Ξ) Γ A) in
      begin
      [ ⇑ᵐ {Ω = Ξ} (μ ∘ᵐ ι) ]ᵐ t ≈⟨ []ᵐ-resp-≡ᵐ ∘ᵐ-resp-⇑ ⟩
      [ ⇑ᵐ μ ∘ᵐ ⇑ᵐ ι ]ᵐ t ≈⟨ [∘ᵐ] ⟩
      [ ⇑ᵐ μ ]ᵐ ([ ⇑ᵐ ι ]ᵐ t)
      ∎

  ∘ᵐ-resp-ᵐ⇑ : ∀ {Θ Ψ Ξ Ω} {ι : Θ ⇒ᵐ Ψ} {μ : Ψ ⇒ᵐ Ω}
    → ᵐ⇑ᵐ (μ ∘ᵐ ι) {Ω = Ξ} ≡ᵐ ᵐ⇑ᵐ μ ∘ᵐ ᵐ⇑ᵐ ι
  ∘ᵐ-resp-ᵐ⇑ (var-inl M) = refl
  ∘ᵐ-resp-ᵐ⇑ (var-inr N) = refl

  ∘ᵐ-resp-ᵐ⇑-term : ∀ {Θ Ψ Ξ Ω Γ A} {ι : Θ ⇒ᵐ Ψ} {μ : Ψ ⇒ᵐ Ω} {t : Term (Ξ ,, Θ) Γ A}
    → [ ᵐ⇑ᵐ  (μ ∘ᵐ ι) {Ω = Ξ} ]ᵐ t ≈  [ ᵐ⇑ᵐ μ ]ᵐ ([ ᵐ⇑ᵐ ι ]ᵐ t)
  ∘ᵐ-resp-ᵐ⇑-term {Θ} {Ψ} {Ξ} {Ω} {Γ} {A} {ι} {μ} {t = t} =
      let open SetoidR (Term-setoid (Ξ ,, Ω) Γ A) in
      begin
      [ ᵐ⇑ᵐ (μ ∘ᵐ ι) {Ω = Ξ} ]ᵐ t ≈⟨ []ᵐ-resp-≡ᵐ ∘ᵐ-resp-ᵐ⇑ ⟩
      [ ᵐ⇑ᵐ μ ∘ᵐ ᵐ⇑ᵐ ι ]ᵐ t ≈⟨ [∘ᵐ] ⟩
      [ ᵐ⇑ᵐ μ ]ᵐ ([ ᵐ⇑ᵐ ι ]ᵐ t)
      ∎

  vr-comm-mr : ∀ {Θ Ψ Γ Δ A} {ρ : Γ ⇒ᵛ Δ} {ι : Θ ⇒ᵐ Ψ} {t : Term Θ Γ A}
    → [ ι ]ᵐ ([ ρ ]ᵛ t) ≈ [ ρ ]ᵛ ([ ι ]ᵐ t)
  vr-comm-mr {t = tm-var x} = ≈-refl
  vr-comm-mr {t = tm-meta M ts} = ≈-meta (λ i → vr-comm-mr)
  vr-comm-mr {t = tm-oper f es} = ≈-oper (λ i → vr-comm-mr)

  mr-comm-vr : ∀ {Θ Ψ Γ Δ A} {ρ : Γ ⇒ᵛ Δ} {ι : Θ ⇒ᵐ Ψ} {t : Term Θ Γ A}
    → [ ρ ]ᵛ ([ ι ]ᵐ t) ≈  [ ι ]ᵐ ([ ρ ]ᵛ t)
  mr-comm-vr {t = tm-var x} = ≈-refl
  mr-comm-vr {t = tm-meta M ts} = ≈-meta (λ i → mr-comm-vr)
  mr-comm-vr {t = tm-oper f es} = ≈-oper (λ i → mr-comm-vr)

  module _ {Θ Ψ : MContext} {A : sort} where
    open Categories.Category
    open Categories.Category.Instance.Setoids
    open Categories.Functor
    open Categories.NaturalTransformation

    MRenaming-NT : ∀ (ι : Θ ⇒ᵐ Ψ) → NaturalTransformation (Term-Functor {Θ} {A}) (Term-Functor {Ψ} {A})
    MRenaming-NT ι =
      record
      { η = λ Γ → record { _⟨$⟩_ = [ ι ]ᵐ_ ; cong = []ᵐ-resp-≈ }
      ; commute = λ ρ t≈s → ≈-trans ([]ᵐ-resp-≈ ([]ᵛ-resp-≈ t≈s)) (ᵐ∘ᵛ≈ᵛ∘ᵐ)
      ; sym-commute = λ ρ t≈s → ≈-trans (≈-sym ᵐ∘ᵛ≈ᵛ∘ᵐ) ([]ᵐ-resp-≈ ([]ᵛ-resp-≈ t≈s))
      }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module UntypingPairs where

open import Relation.Binary.PropositionalEquality

open import Function using (id)
open import Data.Empty
open import Data.Unit
open import Relation.Nullary
open import Data.Nat
open import Data.Fin
open import Data.Vec
open import Data.Sum
open import Data.Product
open import Data.List
open import Data.Maybe

-- Rather tedious --- stuff grows quadratically.  Get this to go
-- through and then see if we can generalize to codes for constructors
-- or something like that.

------------------------------------------------------------
-- Types
------------------------------------------------------------

-- A universe of types for STLC + natural numbers + pairs.
data Type : Set where
  Nat : Type
  _⇒_ : Type → Type → Type
  _⊗_ : Type → Type → Type

infixr 80 _⇒_
infixr 90 _⊗_

-- The function type constructor is injective.
⇒-inj : ∀ {τ₁ τ₂ τ₃ τ₄} → (τ₁ ⇒ τ₂ ≡ τ₃ ⇒ τ₄) → (τ₁ ≡ τ₃) × (τ₂ ≡ τ₄)
⇒-inj refl = refl , refl

⊗-inj : ∀ {τ₁ τ₂ τ₃ τ₄} → (τ₁ ⊗ τ₂ ≡ τ₃ ⊗ τ₄) → (τ₁ ≡ τ₃) × (τ₂ ≡ τ₄)
⊗-inj refl = refl , refl

-- Equality of types is decidable.
_≡?_ : (τ₁ τ₂ : Type) → (τ₁ ≡ τ₂) ⊎ (τ₁ ≢ τ₂)
Nat ≡? Nat = inj₁ refl
Nat ≡? (_ ⇒ _) = inj₂ (λ ())
Nat ≡? (_ ⊗ _) = inj₂ (λ ())
(_ ⇒ _) ≡? Nat = inj₂ (λ ())
(_ ⇒ _) ≡? (_ ⊗ _) = inj₂ (λ ())
(_ ⊗ _) ≡? Nat = inj₂ (λ ())
(_ ⊗ _) ≡? (_ ⇒ _) = inj₂ (λ ())
(τ₁ ⇒ τ₂) ≡? (τ₃ ⇒ τ₄) with τ₁ ≡? τ₃ | τ₂ ≡? τ₄
(τ₁ ⇒ τ₂) ≡? (.τ₁ ⇒ .τ₂) | inj₁ refl | inj₁ refl = inj₁ refl
(τ₁ ⇒ τ₂) ≡? (τ₃ ⇒ τ₄) | inj₂ τ₁≢τ₃ | _ = inj₂ (λ eq → τ₁≢τ₃ (proj₁ (⇒-inj eq)))
(τ₁ ⇒ τ₂) ≡? (τ₃ ⇒ τ₄) | _ | inj₂ τ₂≢τ₄ = inj₂ (λ eq → τ₂≢τ₄ (proj₂ (⇒-inj eq)))
(τ₁ ⊗ τ₂) ≡? (τ₃ ⊗ τ₄) with τ₁ ≡? τ₃ | τ₂ ≡? τ₄
(τ₁ ⊗ τ₂) ≡? (.τ₁ ⊗ .τ₂) | inj₁ refl | inj₁ refl = inj₁ refl
(τ₁ ⊗ τ₂) ≡? (τ₃ ⊗ τ₄) | inj₂ τ₁≢τ₃ | _ = inj₂ (λ x → τ₁≢τ₃ (proj₁ (⊗-inj x)))
(τ₁ ⊗ τ₂) ≡? (τ₃ ⊗ τ₄) | _ | inj₂ τ₂≢τ₄ = inj₂ (λ eq → τ₂≢τ₄ (proj₂ (⊗-inj eq)))

≢-cong-⇒ : ∀ {τ₁ τ₂ τ₃ τ₄} → (τ₁ ⇒ τ₂ ≢ τ₃ ⇒ τ₄) → (τ₁ ≢ τ₃) ⊎ (τ₂ ≢ τ₄)
≢-cong-⇒ {τ₁} {τ₂} {τ₃} {τ₄} neq with τ₁ ≡? τ₃ | τ₂ ≡? τ₄
≢-cong-⇒ neq | inj₂ τ₁≢τ₃ | _ = inj₁ τ₁≢τ₃
≢-cong-⇒ neq | _ | inj₂ τ₂≢τ₄ = inj₂ τ₂≢τ₄
≢-cong-⇒ neq | inj₁ refl | inj₁ refl = ⊥-elim (neq refl)

≢-cong-⊗ : ∀ {τ₁ τ₂ τ₃ τ₄} → (τ₁ ⊗ τ₂ ≢ τ₃ ⊗ τ₄) → (τ₁ ≢ τ₃) ⊎ (τ₂ ≢ τ₄)
≢-cong-⊗ {τ₁} {τ₂} {τ₃} {τ₄} neq with τ₁ ≡? τ₃ | τ₂ ≡? τ₄
≢-cong-⊗ neq | inj₂ τ₁≢τ₃ | _ = inj₁ τ₁≢τ₃
≢-cong-⊗ neq | _ | inj₂ τ₂≢τ₄ = inj₂ τ₂≢τ₄
≢-cong-⊗ neq | inj₁ refl | inj₁ refl = ⊥-elim (neq refl)

-- A type of explicit evidence explaining *why* two types are unequal.
data _≁_ : Type → Type → Set where
  Nat≁⇒ : ∀ {τ₁ τ₂} → Nat ≁ (τ₁ ⇒ τ₂)
  Nat≁⊗ : ∀ {τ₁ τ₂} → Nat ≁ (τ₁ ⊗ τ₂)
  ⇒≁⊗   : ∀ {τ₁ τ₂ τ₃ τ₄} → (τ₁ ⇒ τ₂) ≁ (τ₃ ⊗ τ₄)
  ⇒ˡ-≁  : ∀ {τ₁ τ₂ τ₃ τ₄} → τ₁ ≁ τ₂ → (τ₁ ⇒ τ₃) ≁ (τ₂ ⇒ τ₄)
  ⇒ʳ-≁  : ∀ {τ₁ τ₂ τ₃ τ₄} → τ₃ ≁ τ₄ → (τ₁ ⇒ τ₃) ≁ (τ₂ ⇒ τ₄)
  ⊗ˡ-≁  : ∀ {τ₁ τ₂ τ₃ τ₄} → τ₁ ≁ τ₂ → (τ₁ ⊗ τ₃) ≁ (τ₂ ⊗ τ₄)
  ⊗ʳ-≁  : ∀ {τ₁ τ₂ τ₃ τ₄} → τ₃ ≁ τ₄ → (τ₁ ⊗ τ₃) ≁ (τ₂ ⊗ τ₄)

  ≁-sym   : ∀ {τ₁ τ₂} → τ₁ ≁ τ₂ → τ₂ ≁ τ₁

-- Given such a proof we can show the types are unequal.
≁-≢ : ∀ {τ₁ τ₂} → (τ₁ ≁ τ₂) → (τ₁ ≢ τ₂)
≁-≢ Nat≁⇒ = λ ()
≁-≢ Nat≁⊗ = λ ()
≁-≢ ⇒≁⊗ = λ ()
≁-≢ (⇒ˡ-≁ τ₁≁τ₂)  refl = ≁-≢ τ₁≁τ₂ refl
≁-≢ (⇒ʳ-≁ τ₃≁τ₄)  refl = ≁-≢ τ₃≁τ₄ refl
≁-≢ (⊗ˡ-≁ τ₁≁τ₂)  refl = ≁-≢ τ₁≁τ₂ refl
≁-≢ (⊗ʳ-≁ τ₃≁τ₄)  refl = ≁-≢ τ₃≁τ₄ refl
≁-≢ (≁-sym τ₂≁τ₁) refl = ≁-≢ τ₂≁τ₁ refl

-- Since our universe of types is closed, we can actually go the other
-- way too. That is, ≢ is equivalent to ≁ ; the point is that the
-- latter is more immediately informative (by pattern-matching etc.)
-- which can be used to produce error messages and so on.
--
-- Note, however, that there might be *multiple* terms of type τ₁ ≁
-- τ₂: each corresponds to a different explanation of why the types
-- are not equal.  We might actually care which one we have.
-- Round-tripping through (τ₁ ≢ τ₂) is not the identity.

≢-≁ : ∀ {τ₁ τ₂} → (τ₁ ≢ τ₂) → (τ₁ ≁ τ₂)
≢-≁ {Nat} {Nat} τ₁≢τ₂ with τ₁≢τ₂ refl
... | ()
≢-≁ {Nat} {τ₂ ⇒ τ₃} _ = Nat≁⇒
≢-≁ {Nat} {τ₂ ⊗ τ₃} _ = Nat≁⊗
≢-≁ {τ₁ ⇒ τ₂} {Nat} _ = ≁-sym Nat≁⇒
≢-≁ {τ₁ ⇒ τ₂} {τ₃ ⊗ τ₄} _ = ⇒≁⊗
≢-≁ {τ₁ ⊗ τ₂} {Nat} _ = ≁-sym Nat≁⊗
≢-≁ {τ₁ ⊗ τ₂} {τ₃ ⇒ τ₄} _ = ≁-sym ⇒≁⊗
≢-≁ {τ₁ ⇒ τ₂} {τ₃ ⇒ τ₄} τ₁⇒τ₂≢τ₃⇒τ₄ with ≢-cong-⇒ τ₁⇒τ₂≢τ₃⇒τ₄
≢-≁ {τ₁ ⇒ τ₂} {τ₃ ⇒ τ₄} τ₁⇒τ₂≢τ₃⇒τ₄ | inj₁ τ₁≢τ₃ = ⇒ˡ-≁ (≢-≁ τ₁≢τ₃)
≢-≁ {τ₁ ⇒ τ₂} {τ₃ ⇒ τ₄} τ₁⇒τ₂≢τ₃⇒τ₄ | inj₂ τ₂≢τ₄ = ⇒ʳ-≁ (≢-≁ τ₂≢τ₄)
≢-≁ {τ₁ ⊗ τ₂} {τ₃ ⊗ τ₄} τ₁⊗τ₂≢τ₃⊗τ₄ with ≢-cong-⊗ τ₁⊗τ₂≢τ₃⊗τ₄
≢-≁ {τ₁ ⊗ τ₂} {τ₃ ⊗ τ₄} τ₁⊗τ₂≢τ₃⊗τ₄ | inj₁ τ₁≢τ₃ = ⊗ˡ-≁ (≢-≁ τ₁≢τ₃)
≢-≁ {τ₁ ⊗ τ₂} {τ₃ ⊗ τ₄} τ₁⊗τ₂≢τ₃⊗τ₄ | inj₂ τ₂≢τ₄ = ⊗ʳ-≁ (≢-≁ τ₂≢τ₄)

-- Sometimes it's convenient to decide equality of types using ≁ in place of ≢.
_∼?_ : (τ₁ τ₂ : Type) → (τ₁ ≡ τ₂) ⊎ (τ₁ ≁ τ₂)
τ₁ ∼? τ₂ = Data.Sum.map id ≢-≁ (τ₁ ≡? τ₂)

-- Evidence that a type is not an arrow type.
data not⇒_ : Type → Set where
  not⇒Nat : not⇒ Nat
  not⇒⊗   : ∀ {τ₁ τ₂} → not⇒ (τ₁ ⊗ τ₂)

data not⊗_ : Type → Set where
  not⊗Nat : not⊗ Nat
  not⊗⇒   : ∀ {τ₁ τ₂} → not⊗ (τ₁ ⇒ τ₂)

⇒? : (τ : Type) → (Σ[ τ₁ ∈ Type ] Σ[ τ₂ ∈ Type ] τ ≡ τ₁ ⇒ τ₂) ⊎ (not⇒ τ)
⇒? Nat       = inj₂ not⇒Nat
⇒? (_ ⊗ _) = inj₂ not⇒⊗
⇒? (τ₁ ⇒ τ₂) = inj₁ (τ₁ , τ₂ , refl)

------------------------------------------------------------
-- Expressions
------------------------------------------------------------

-- (Untyped) expressions of STLC + arithmetic + pairs.
data Expr (n : ℕ) : Set where
  lit : ℕ → Expr n
  _⊕_ : Expr n → Expr n → Expr n

  ⟨_,_⟩ : Expr n → Expr n → Expr n
  π₁ : Expr n
  π₂ : Expr n

  var : Fin n → Expr n
  ƛ   : Type → Expr (suc n) → Expr n
  _·_ : Expr n → Expr n → Expr n

Ctx : ℕ → Set
Ctx n = Vec Type n

------------------------------------------------------------
-- Typing
------------------------------------------------------------

-- Typing derivations.
data _⊢_∶_ : ∀ {n} → Ctx n → Expr n → Type → Set where
  lit  : ∀ {n} {Γ : Ctx n} {m}
       → Γ ⊢ lit m ∶ Nat
  _⊕_  : ∀ {n} {Γ : Ctx n} {t₁ t₂}
       → Γ ⊢ t₁        ∶ Nat
       → Γ ⊢ t₂        ∶ Nat
       → Γ ⊢ (t₁ ⊕ t₂) ∶ Nat
  ⟨_,_⟩ : ∀ {n} {Γ : Ctx n} {t₁ t₂} {τ₁ τ₂}
       → Γ ⊢ t₁        ∶ τ₁
       → Γ ⊢ t₂        ∶ τ₂
       → Γ ⊢ ⟨ t₁ , t₂ ⟩ ∶ τ₁ ⊗ τ₂
  π₁   : ∀ {n} {Γ : Ctx n} {τ₁ τ₂}
       → Γ ⊢ π₁ ∶ (τ₁ ⊗ τ₂) ⇒ τ₁
  π₂   : ∀ {n} {Γ : Ctx n} {τ₁ τ₂}
       → Γ ⊢ π₂ ∶ (τ₁ ⊗ τ₂) ⇒ τ₂
  var  : ∀ {n} {Γ : Ctx n} {i}
       → Γ ⊢ var i ∶ lookup i Γ
  ƛ    : ∀ {n} {Γ : Ctx n} {t} {τ₁ τ₂}
       → (τ₁ ∷ Γ) ⊢ t ∶ τ₂
       → Γ ⊢ ƛ τ₁ t ∶ (τ₁ ⇒ τ₂)
  _·_  : ∀ {n} {Γ : Ctx n} {t₁ t₂} {τ₁ τ₂}
       → Γ ⊢ t₁ ∶ τ₁ ⇒ τ₂
       → Γ ⊢ t₂ ∶ τ₁
       → Γ ⊢ t₁ · t₂ ∶ τ₂

-- Explicit, constructive evidence for the *untypability* of a term.
data _⊬_∶_ : ∀ {n} → Ctx n → Expr n → Type → Set where

  -- Explicitly build in uniqueness of typing as an axiom.  t is not
  -- typeable at type τ₂ if t is typeable at some different type.
  mismatch : ∀ {n} {Γ : Ctx n} {t} {τ₁ τ₂}
             → Γ ⊢ t ∶ τ₁
             → τ₁ ≁ τ₂
             → Γ ⊬ t ∶ τ₂

  -- There are three ways for a + term to fail to have a given type τ:
  -- either the left or right sides do not have type Nat, or the type
  -- τ itself is not Nat.
  ⊕ˡ       : ∀ {n} {Γ : Ctx n} {t₁ t₂} {τ}
             → Γ ⊬ t₁ ∶ Nat
             → Γ ⊬ (t₁ ⊕ t₂) ∶ τ
  ⊕ʳ       : ∀ {n} {Γ : Ctx n} {t₁ t₂} {τ}
             → Γ ⊬ t₂ ∶ Nat
             → Γ ⊬ (t₁ ⊕ t₂) ∶ τ
  ⊕≁Nat    : ∀ {n} {Γ : Ctx n} {t₁ t₂} {τ}
             → τ ≁ Nat → Γ ⊬ (t₁ ⊕ t₂) ∶ τ

  ⟨⟩-ty    : ∀ {n} {Γ : Ctx n} {t₁ t₂} {τ}
             → not⊗ τ → Γ ⊬ ⟨ t₁ , t₂ ⟩ ∶ τ
  ⟨⟩ˡ      : ∀ {n} {Γ : Ctx n} {t₁ t₂} {τ₁ τ₂}
             → Γ ⊬ t₁ ∶ τ₁
             → Γ ⊬ ⟨ t₁ , t₂ ⟩ ∶ τ₁ ⊗ τ₂
  ⟨⟩ʳ      : ∀ {n} {Γ : Ctx n} {t₁ t₂} {τ₁ τ₂}
             → Γ ⊬ t₂ ∶ τ₂
             → Γ ⊬ ⟨ t₁ , t₂ ⟩ ∶ τ₁ ⊗ τ₂

  π₁-⇒     : ∀ {n} {Γ : Ctx n} {τ}
             → not⇒ τ
             → Γ ⊬ π₁ ∶ τ
  π₁-⊗     : ∀ {n} {Γ : Ctx n} {τ₁ τ₂}
             → not⊗ τ₁
             → Γ ⊬ π₁ ∶ τ₁ ⇒ τ₂
  π₁-∼     : ∀ {n} {Γ : Ctx n} {τ₁ τ₂ τ₃}
             → τ₁ ≁ τ₃
             → Γ ⊬ π₁ ∶ (τ₁ ⊗ τ₂) ⇒ τ₃

  π₂-⇒     : ∀ {n} {Γ : Ctx n} {τ}
             → not⇒ τ
             → Γ ⊬ π₂ ∶ τ
  π₂-⊗     : ∀ {n} {Γ : Ctx n} {τ₁ τ₂}
             → not⊗ τ₁
             → Γ ⊬ π₂ ∶ τ₁ ⇒ τ₂
  π₂-∼     : ∀ {n} {Γ : Ctx n} {τ₁ τ₂ τ₃}
             → τ₂ ≁ τ₃
             → Γ ⊬ π₂ ∶ (τ₁ ⊗ τ₂) ⇒ τ₃

  -- ƛ-funty holds if τ is not a function type at all, or if it is a
  -- function type whose input type is not τ₁.
  ƛ-funty  : ∀ {n} {Γ : Ctx n} {t} {τ₁ τ}
             → (∀ {τ₂} → τ ≁ τ₁ ⇒ τ₂)
             → Γ ⊬ ƛ τ₁ t ∶ τ

  -- Otherwise, τ is of the form (τ₁ ⇒ τ₂) but the body t does not
  -- have type τ₂.  Note this could be either because t is not typable
  -- at all, or because it has some type other than τ₂.
  ƛ        : ∀ {n} {Γ : Ctx n} {t} {τ₁ τ₂}
             → (τ₁ ∷ Γ) ⊬ t ∶ τ₂
             → Γ ⊬ ƛ τ₁ t ∶ (τ₁ ⇒ τ₂)

  -- Had this ƛ-resty constructor, but it turns out we don't need it:
  -- it is not used in inference or checking, and isn't needed to
  -- prove equivalence of ⊬ and ¬ ⊢ .  It handles *only* the case
  -- where t is typable but has a type different than the output type
  -- of the whole expression; but the ƛ constructor handles this case
  -- as well as the case where t is not typeable at all.

  -- ƛ-resty  : ∀ {n} {Γ : Ctx n} {t} {τ₁ τ₂ τ₃}
  --            → (τ₁ ∷ Γ) ⊢ t ∶ τ₂
  --            → τ₂ ≁ τ₃
  --            → Γ ⊬ ƛ τ₁ t ∶ τ₁ ⇒ τ₃

  -- Finally, there are two cases when an application is not typeable.
  -- Either the function does not have an appropriate function type,
  -- or the argument does not have a type that matches the function's
  -- input type.
  ·-fun    : ∀ {n} {Γ : Ctx n} {t₁ t₂} {τ₂}
             → (∀ {τ₁} → Γ ⊬ t₁ ∶ τ₁ ⇒ τ₂)
             → Γ ⊬ t₁ · t₂ ∶ τ₂
  ·-arg    : ∀ {n} {Γ : Ctx n} {t₁ t₂} {τ₁ τ₂}
             → Γ ⊢ t₁ ∶ τ₁ ⇒ τ₂
             → Γ ⊬ t₂ ∶ τ₁
             → Γ ⊬ t₁ · t₂ ∶ τ₂

-- ------------------------------------------------------------
-- -- Type inference and checking
-- ------------------------------------------------------------

-- -- Type inference for a term in a given context returns either a type
-- -- and a valid typing derivation, or a constructive proof that the
-- -- term has no type.  Note that in this system, ALL terms can be
-- -- inferred.  In a bidirectional system we would have to restrict this
-- -- to only take inferrable terms as inputs.
-- infer : ∀ {n} → (Γ : Ctx n) → (t : Expr n) → (∃ λ τ → Γ ⊢ t ∶ τ) ⊎ (∀ τ → Γ ⊬ t ∶ τ)
-- infer Γ (lit n)   = inj₁ (Nat , lit)
-- infer Γ (t₁ ⊕ t₂) with infer Γ t₁ | infer Γ t₂
-- infer Γ (t₁ ⊕ t₂) | inj₁ (Nat , Γ⊢t₁∶Nat) | inj₁ (Nat , Γ⊢t₂∶Nat) = inj₁ (Nat , (Γ⊢t₁∶Nat ⊕ Γ⊢t₂∶Nat))
-- infer Γ (t₁ ⊕ t₂) | inj₁ (τ₁ ⇒ τ₂ , Γ⊢t₁∶τ₁⇒τ₂) | inj₁ _ = inj₂ (λ _ → ⊕ˡ (mismatch Γ⊢t₁∶τ₁⇒τ₂ (≁-sym Nat≁⇒)))
-- infer Γ (t₁ ⊕ t₂) | inj₁ _ | inj₁ (τ₃ ⇒ τ₄ , Γ⊢t₂∶τ₃⇒τ₄) = inj₂ (λ _ → ⊕ʳ (mismatch Γ⊢t₂∶τ₃⇒τ₄ (≁-sym Nat≁⇒)))
-- infer Γ (t₁ ⊕ t₂) | inj₂ Γ⊬t₁∶ | _ = inj₂ (λ _ → ⊕ˡ (Γ⊬t₁∶ Nat))
-- infer Γ (t₁ ⊕ t₂) | _ | inj₂ Γ⊬t₂∶ = inj₂ (λ _ → ⊕ʳ (Γ⊬t₂∶ Nat))
-- infer Γ (var i)   = inj₁ (lookup i Γ , var)
-- infer Γ (ƛ τ₁ t) with infer (τ₁ ∷ Γ) t
-- infer Γ (ƛ τ₁ t) | inj₁ (τ₂ , τ₁∷Γ⊢t∶τ₂) = inj₁ (τ₁ ⇒ τ₂ , ƛ τ₁∷Γ⊢t∶τ₂)
-- infer Γ (ƛ τ₁ t) | inj₂ τ₁∷Γ⊬t∶ = inj₂ lemma
--   where
--     lemma : (τ : Type) → Γ ⊬ ƛ τ₁ t ∶ τ
--     lemma Nat        = ƛ-funty Nat≁⇒
--     lemma (τ₁′ ⇒ τ₂) with τ₁′ ∼? τ₁
--     lemma (.τ₁ ⇒ τ₂) | inj₁ refl = ƛ (τ₁∷Γ⊬t∶ τ₂)
--     lemma (τ₁′ ⇒ τ₂) | inj₂ τ₁′≁τ₁ = ƛ-funty (λ {τ₃} → ⇒ˡ-≁ τ₁′≁τ₁)
-- infer Γ (t₁ · t₂) with infer Γ t₁ | infer Γ t₂
-- infer Γ (t₁ · t₂) | inj₁ (Nat , Γ⊢t₁∶Nat) | _ = inj₂ (λ _ → ·-fun (mismatch Γ⊢t₁∶Nat Nat≁⇒))
-- infer Γ (t₁ · t₂) | inj₁ (τ₁ ⇒ τ₂ , Γ⊢t₁∶τ₁⇒τ₂) | inj₁ (τ₁′ , Γ⊢t₂∶τ₁′) with τ₁ ∼? τ₁′
-- infer Γ (t₁ · t₂) | inj₁ (τ₁ ⇒ τ₂ , Γ⊢t₁∶τ₁⇒τ₂) | inj₁ (.τ₁ , Γ⊢t₂∶τ₁ ) | inj₁ refl = inj₁ (τ₂ , (Γ⊢t₁∶τ₁⇒τ₂ · Γ⊢t₂∶τ₁))
-- infer Γ (t₁ · t₂) | inj₁ (τ₁ ⇒ τ₂ , Γ⊢t₁∶τ₁⇒τ₂) | inj₁ (τ₁′ , Γ⊢t₂∶τ₁′) | inj₂ τ₁≁τ₁′ = inj₂ lemma2
--   where
--     lemma2 : ∀ τ → Γ ⊬ t₁ · t₂ ∶ τ
--     lemma2 τ with τ ∼? τ₂
--     lemma2 τ | inj₁ τ≡τ₂ rewrite τ≡τ₂ = ·-arg Γ⊢t₁∶τ₁⇒τ₂ (mismatch Γ⊢t₂∶τ₁′ (≁-sym τ₁≁τ₁′))
--     lemma2 τ | inj₂ τ≁τ₂ = ·-fun (mismatch Γ⊢t₁∶τ₁⇒τ₂ (⇒ʳ-≁ (≁-sym τ≁τ₂)))
-- infer Γ (t₁ · t₂) | inj₁ (τ₁ ⇒ τ₂ , Γ⊢t₁∶τ₁⇒τ₂) | inj₂ Γ⊬t₂ = inj₂ lemma3
--   where
--     lemma3 : ∀ τ → Γ ⊬ t₁ · t₂ ∶ τ
--     lemma3 τ with τ ∼? τ₂
--     lemma3 τ | inj₁ τ≡τ₂ rewrite τ≡τ₂ = ·-arg Γ⊢t₁∶τ₁⇒τ₂ (Γ⊬t₂ τ₁)
--     lemma3 τ | inj₂ τ≁τ₂ = ·-fun (mismatch Γ⊢t₁∶τ₁⇒τ₂ (⇒ʳ-≁ (≁-sym τ≁τ₂)))
-- infer Γ (t₁ · t₂) | inj₂ Γ⊬t₁∶ | _ = inj₂ (λ τ₂ → ·-fun (λ {τ₁} → Γ⊬t₁∶ (τ₁ ⇒ τ₂)))

-- -- Check whether a given term has a *given* type.
-- check : ∀ {n} → (Γ : Ctx n) → (t : Expr n) → (τ : Type) → (Γ ⊢ t ∶ τ) ⊎ (Γ ⊬ t ∶ τ)
-- check Γ (lit _)   (τ ⇒ τ₁) = inj₂ (mismatch lit Nat≁⇒)
-- check Γ (lit _)   Nat      = inj₁ lit
-- check Γ (_  ⊕ _ ) (τ ⇒ τ₁) = inj₂ (⊕≁Nat (≁-sym Nat≁⇒))
-- check Γ (t₁ ⊕ t₂) Nat with check Γ t₁ Nat | check Γ t₂ Nat
-- check Γ (t₁ ⊕ t₂) Nat | inj₁ Γ⊢t₁∶Nat | inj₁ Γ⊢t₂∶Nat = inj₁ (Γ⊢t₁∶Nat ⊕ Γ⊢t₂∶Nat)
-- check Γ (t₁ ⊕ t₂) Nat | inj₂ Γ⊬t₁∶Nat | _             = inj₂ (⊕ˡ Γ⊬t₁∶Nat)
-- check Γ (t₁ ⊕ t₂) Nat | _             | inj₂ Γ⊬t₂∶Nat = inj₂ (⊕ʳ Γ⊬t₂∶Nat)
-- check Γ (var i)   τ with τ ∼? lookup i Γ
-- check Γ (var i) τ | inj₁ τ≡iΓ rewrite τ≡iΓ = inj₁ var
-- check Γ (var i) τ | inj₂ τ≁iΓ = inj₂ (mismatch var (≁-sym τ≁iΓ))
-- check Γ (ƛ τ₁ t) Nat = inj₂ (ƛ-funty Nat≁⇒)
-- check Γ (ƛ τ₁ t) (τ ⇒ τ₂) with τ ∼? τ₁ | check (τ₁ ∷ Γ) t τ₂
-- check Γ (ƛ τ₁ t) (τ ⇒ τ₂) | inj₂ τ≁τ₁ | _ = inj₂ (ƛ-funty (⇒ˡ-≁ τ≁τ₁))
-- check Γ (ƛ τ₁ t) (.τ₁ ⇒ τ₂) | inj₁ refl | inj₂ τ₁∷Γ⊬t∶τ₂ = inj₂ (ƛ τ₁∷Γ⊬t∶τ₂)
-- check Γ (ƛ τ₁ t) (.τ₁ ⇒ τ₂) | inj₁ refl | inj₁ τ₁∷Γ⊢t∶τ₂ = inj₁ (ƛ τ₁∷Γ⊢t∶τ₂)
--   --- Note that in order to check an application we have to use type inference on t₁.
-- check Γ (t₁ · t₂) τ with infer Γ t₁
-- check Γ (t₁ · t₂) τ | inj₂ Γ⊬t₁∶ = inj₂ (·-fun (λ {τ₁} → Γ⊬t₁∶ (τ₁ ⇒ τ)))
-- check Γ (t₁ · t₂) τ | inj₁ (Nat , Γ⊢t₁∶τ₁) = inj₂ (·-fun (mismatch Γ⊢t₁∶τ₁ Nat≁⇒))
-- check Γ (t₁ · t₂) τ | inj₁ (τ₁ ⇒ τ₂ , Γ⊢t₁∶τ₁) with τ ∼? τ₂
-- check Γ (t₁ · t₂) τ | inj₁ (τ₁ ⇒ τ₂ , Γ⊢t₁∶τ₁) | inj₂ τ≁τ₂ = inj₂ (·-fun (mismatch Γ⊢t₁∶τ₁ (⇒ʳ-≁ (≁-sym τ≁τ₂))))
-- check Γ (t₁ · t₂) τ | inj₁ (τ₁ ⇒ τ₂ , Γ⊢t₁∶τ₁) | inj₁ τ≡τ₂ rewrite τ≡τ₂ with check Γ t₂ τ₁
-- check Γ (t₁ · t₂) τ | inj₁ (τ₁ ⇒ τ₂ , Γ⊢t₁∶τ₁) | inj₁ τ≡τ₂ | inj₂ Γ⊬t₂∶τ₁ = inj₂ (·-arg Γ⊢t₁∶τ₁ Γ⊬t₂∶τ₁)
-- check Γ (t₁ · t₂) τ | inj₁ (τ₁ ⇒ τ₂ , Γ⊢t₁∶τ₁) | inj₁ τ≡τ₂ | inj₁ Γ⊢t₂∶τ₁ = inj₁ (Γ⊢t₁∶τ₁ · Γ⊢t₂∶τ₁)

-- ------------------------------------------------------------
-- -- Correctness
-- ------------------------------------------------------------

-- -- The whole idea is that ⊬ is a more explicit/constructive, yet
-- -- equivalent, way to represent the negation of ⊢ .  We can actually
-- -- prove the equivalence.

-- -- First, straightforward induction on typing derivations shows that
-- -- we really do have unique types, as assumed by the 'mismatch'
-- -- constructor.

-- ⊢-unique : ∀ {n} {Γ : Ctx n} {t : Expr n} {τ₁ τ₂ : Type} → (Γ ⊢ t ∶ τ₁) → (Γ ⊢ t ∶ τ₂) → (τ₁ ≡ τ₂)
-- ⊢-unique lit lit = refl
-- ⊢-unique (_ ⊕ _) (_ ⊕ _) = refl
-- ⊢-unique var var = refl
-- ⊢-unique (ƛ Γ⊢t∶τ₁) (ƛ Γ⊢t∶τ₂) rewrite ⊢-unique Γ⊢t∶τ₁ Γ⊢t∶τ₂ = refl
-- ⊢-unique (Γ⊢t∶τ₁ · _) (Γ⊢t∶τ₂ · _) = proj₂ (⇒-inj (⊢-unique Γ⊢t∶τ₁ Γ⊢t∶τ₂))

-- -- Now we can do one direction of the equivalence.  This direction is
-- -- just induction over derivations, making use of uniqueness of
-- -- typing.
-- ⊬-¬⊢ : ∀ {n} {Γ : Ctx n} {t : Expr n} {τ : Type} → (Γ ⊬ t ∶ τ) → (¬ (Γ ⊢ t ∶ τ))

-- ⊬-¬⊢ (mismatch Γ⊢t∶τ₁ τ₁≁τ) Γ⊢t∶τ = ≁-≢ τ₁≁τ (⊢-unique Γ⊢t∶τ₁ Γ⊢t∶τ)

-- ⊬-¬⊢ (⊕ˡ Γ⊬t₁∶N)     (Γ⊢t₁∶N ⊕ _     ) = ⊬-¬⊢ Γ⊬t₁∶N Γ⊢t₁∶N
-- ⊬-¬⊢ (⊕ʳ Γ⊬t₂∶N)     (_      ⊕ Γ⊢t₂∶N) = ⊬-¬⊢ Γ⊬t₂∶N Γ⊢t₂∶N
-- ⊬-¬⊢ (⊕≁Nat τ≁N)     (_      ⊕ _     ) = ≁-≢ τ≁N refl

-- ⊬-¬⊢ (ƛ-funty τ≁τ₁⇒) (ƛ _)      = ≁-≢ τ≁τ₁⇒ refl
-- ⊬-¬⊢ (ƛ Γ⊬t∶τ₂)      (ƛ Γ⊢t∶τ₂) = ⊬-¬⊢ Γ⊬t∶τ₂ Γ⊢t∶τ₂

-- ⊬-¬⊢ (·-fun Γ⊬t₁) (Γ⊢t₁ · _) = ⊬-¬⊢ Γ⊬t₁ Γ⊢t₁
-- ⊬-¬⊢ (·-arg Γ⊢t₁∶τ₁⇒τ Γ⊬t₂∶τ) (Γ⊢t₁∶τ₂⇒τ · Γ⊢t₂)
--   rewrite proj₁ (⇒-inj (⊢-unique Γ⊢t₁∶τ₁⇒τ Γ⊢t₁∶τ₂⇒τ)) = ⊬-¬⊢ Γ⊬t₂∶τ Γ⊢t₂

-- -- The other direction follows straightforwardly from type checking.
-- ¬⊢-⊬ : ∀ {n} {Γ : Ctx n} {t : Expr n} {τ : Type} → (¬ (Γ ⊢ t ∶ τ)) → (Γ ⊬ t ∶ τ)
-- ¬⊢-⊬ {_} {Γ} {t} {τ} ¬Γ⊢t∶τ with check Γ t τ
-- ¬⊢-⊬ ¬Γ⊢t∶τ | inj₁ Γ⊢t∶τ = ⊥-elim (¬Γ⊢t∶τ Γ⊢t∶τ)
-- ¬⊢-⊬ ¬Γ⊢t∶τ | inj₂ Γ⊬t∶τ = Γ⊬t∶τ

-- ------------------------------------------------------------
-- -- Take 2
-- ------------------------------------------------------------

-- -- XXX these need to be dependent somehow?  e.g. consider the ƛ case
-- -- below.  If τ is not an arrow type the whole thing fails; but if it
-- -- does, we need to know what τ₁ and τ₂ are in order to refer to them
-- -- in the rest of the conditions.

-- data many : List (Set × Set) → Set where
--   empty : many []
--   here  : ∀ {Tₗ Tᵣ Ts} → Tₗ → many Ts → many ((Tₗ , Tᵣ) ∷ Ts)
--   there : ∀ {Tₗ Tᵣ Ts} → Tᵣ → many Ts → many ((Tₗ , Tᵣ) ∷ Ts)

-- data some : List (Set × Set) → Set where
--   here  : ∀ {Tₗ Tᵣ Ts} → Tₗ → many Ts → some ((Tₗ , Tᵣ) ∷ Ts)
--   there : ∀ {Tₗ Tᵣ Ts} → Tᵣ → some Ts → some ((Tₗ , Tᵣ) ∷ Ts)

-- -- Unique untypability; gives *every* possible reason that something
-- -- is not typeable.  There is no 'mismatch' constructor.

-- {-# NO_POSITIVITY_CHECK #-}
-- data _⊬₂_∶_ : ∀ {n} → Ctx n → Expr n → Type → Set where

--   lit : ∀ {n} {Γ : Ctx n} {m} {τ} → τ ≁ Nat → Γ ⊬₂ lit m ∶ τ

--   -- For t₁ ⊕ t₂ to be untypeable, at least one of three things must be wrong:
--   ⊕   : ∀ {n} {Γ : Ctx n} {t₁ t₂ τ}
--       → some
--         ( (Γ ⊬₂ t₁ ∶ Nat , Γ ⊢ t₁ ∶ Nat)     -- Either t₁ is well-typed or not
--         ∷ (Γ ⊬₂ t₂ ∶ Nat , Γ ⊢ t₂ ∶ Nat)     -- Either t₂ is well-typed or not
--         ∷ ((τ ≁ Nat) , (τ ≡ Nat))            -- τ is Nat or not
--         ∷ []
--         )
--       → Γ ⊬₂ t₁ ⊕ t₂ ∶ τ

--   var : ∀ {n} {Γ : Ctx n} {i τ}
--       → τ ≁ lookup i Γ
--       → Γ ⊬₂ var i ∶ τ

--   -- ƛ τ₁ t does not have type τ if
--   --   - τ is not an arrow type

--   -- ƛ   : ∀ {n} {Γ : Ctx n} {t} {τ₁ τ₂ τ}
--   --     → some
--   --       ( (τ ≁

max_stars_repo_name: enlambdment/disco

max_issues_repo_name: enlambdment/disco

max_forks_repo_name: enlambdment/disco


text:
module UniDB.Morph.Reg where

open import UniDB.Spec
open import UniDB.Morph.WeakenPrime
open import UniDB.Morph.ShiftsPrime

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

data Reg (T : STX) : MOR where
  baseR : {γ₁ γ₂ : Dom} (ξ : Weaken` γ₁ γ₂) → Reg T γ₁ γ₂
  snocR : {γ₁ γ₂ : Dom} (ξ : Reg T γ₁ γ₂) (t : T γ₂) → Reg T (suc γ₁) γ₂

module _ {T : STX} where

  instance
    iIdmReg : Idm (Reg T)
    idm {{iIdmReg}} γ = baseR baseW

    iWkmReg : Wkm (Reg T)
    wkm {{iWkmReg}} δ = baseR (wkm {Weaken`} δ)

    iBetaReg : Beta T (Reg T)
    beta {{iBetaReg}} t = snocR (idm {_} _) t

  module _ {{vrT : Vr T}} {{wkT : Wk T}} where

    instance
      iWkReg : {γ₁ : Dom} → Wk (Reg T γ₁)
      wk₁ {{iWkReg}} (baseR ξ)    = baseR (wk₁ ξ)
      wk₁ {{iWkReg}} (snocR ξ t) = snocR (wk₁ ξ) (wk₁ t)
      wk {{iWkReg}} zero ξ       = ξ
      wk {{iWkReg}} (suc δ) ξ    = wk₁ (wk δ ξ)
      wk-zero {{iWkReg}} x = refl
      wk-suc {{iWkReg}} δ x = refl

      iUpReg : Up (Reg T)
      _↑₁ {{iUpReg}} ξ = snocR (wk₁ ξ) (vr {T} zero)
      _↑_ {{iUpReg}} ξ 0 = ξ
      _↑_ {{iUpReg}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
      ↑-zero {{iUpReg}} ξ = refl
      ↑-suc {{iUpReg}} ξ δ⁺ = refl

      -- iUpIdmReg : {{wkT : Wk T}} → UpIdm (Reg T)
      -- idm-↑₁ {{iUpIdmReg}} = ?refl

  instance
    iHCompWeakenReg : HComp Weaken` (Reg T) (Reg T)
    _⊡_ {{iHCompWeakenReg}} ξ         (baseR ζ)   = baseR (ξ ⊙ ζ)
    _⊡_ {{iHCompWeakenReg}} baseW     ζ           = ζ
    _⊡_ {{iHCompWeakenReg}} (stepW ξ) (snocR ζ t) = ξ ⊡ ζ

    iHCompIdmLeftWeakenReg : HCompIdmLeft Weaken` (Reg T)
    idm-⊡ {{iHCompIdmLeftWeakenReg}} (baseR ξ)
      rewrite idm-⊙ {Weaken`} ξ = refl
    idm-⊡ {{iHCompIdmLeftWeakenReg}} (snocR ξ₂ t) = refl

  ⊡-⊡-assoc : {γ₁ γ₂ γ₃ γ₄ : Dom}
    (ξ₁ : Weaken` γ₁ γ₂)
    (ξ₂ : Weaken` γ₂ γ₃)
    (ξ₃ : Reg T γ₃ γ₄) →
    _⊡_ {Weaken`} {Reg T} {Reg T} ξ₁ (ξ₂ ⊡ ξ₃) ≡ (ξ₁ ⊙ ξ₂) ⊡ ξ₃
  ⊡-⊡-assoc ξ₁ ξ₂ (baseR ξ₃) = cong baseR (⊙-assoc {Weaken`} ξ₁ ξ₂ ξ₃)
  ⊡-⊡-assoc ξ₁ baseW ξ₃ rewrite idm-⊡ {Weaken`} {Reg T} ξ₃ = refl
  ⊡-⊡-assoc ξ₁ (stepW ξ₂) (snocR ξ₃ t) = ⊡-⊡-assoc ξ₁ ξ₂ ξ₃

module _ {T : STX} {{vrT : Vr T}} where

  instance
    iLkReg : Lk T (Reg T)
    lk {{iLkReg}} (baseR ξ)   i       = lk {T} {Weaken`} ξ i
    lk {{iLkReg}} (snocR ξ t) zero    = t
    lk {{iLkReg}} (snocR ξ t) (suc i) = lk {T} {Reg T} ξ i

    iLkIdmReg : LkIdm T (Reg T)
    lk-idm {{iLkIdmReg}} i = refl

    iLkWkmReg : {{wkT : Wk T}} → LkWkm T (Reg T)
    lk-wkm {{iLkWkmReg}} = lk-wkm {T} {Weaken`}

    iLkUpReg : {{wkT : Wk T}} {{wkVrT : WkVr T}} → LkUp T (Reg T)
    lk-↑₁-zero {{iLkUpReg}} ξ = refl
    lk-↑₁-suc {{iLkUpReg}} (baseR ξ)   i       = sym (wk₁-vr {T} (lk {Ix} {Weaken`} ξ i))
    lk-↑₁-suc {{iLkUpReg}} (snocR ξ t) zero    = refl
    lk-↑₁-suc {{iLkUpReg}} (snocR ξ t) (suc i) = lk-↑₁-suc {T} {Reg T} ξ i

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
------------------------------------------------------------------------
-- Not
------------------------------------------------------------------------

module TotalParserCombinators.Not where

open import Axiom.Extensionality.Propositional
open import Data.Bool
open import Data.Empty
open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Binary.BagAndSetEquality
  using () renaming (_∼[_]_ to _List-∼[_]_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Product
import Data.Product.Function.Dependent.Propositional as Σ
open import Data.Unit
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (module Equivalence)
open import Function.Inverse as Inv using (_↔_)
open import Function.Related
import Function.Related.TypeIsomorphisms as Iso
open import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open import TotalParserCombinators.Congruence as C using (_∼[_]P_; _≅P_)
open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.Parser
import TotalParserCombinators.Pointwise as Pointwise
open import TotalParserCombinators.Semantics using (_∈_·_; parser)

------------------------------------------------------------------------
-- An initial bag operator

-- not-index xs is non-empty iff xs is empty.

not-index : {R : Set} → List R → List ⊤
not-index xs = if null xs then [ tt ] else []

-- not-index preserves equality.

not-index-cong : ∀ {k R} {xs xs′ : List R} →
                 xs List-∼[ ⌊ k ⌋⇔ ] xs′ →
                 not-index xs List-∼[ ⌊ k ⌋⇔ ] not-index xs′
not-index-cong {xs = []   } {xs′ = []   } eq = ↔⇒ Inv.id
not-index-cong {xs = _ ∷ _} {xs′ = _ ∷ _} eq = ↔⇒ Inv.id
not-index-cong {xs = []   } {xs′ = _ ∷ _} eq
  with Equivalence.from (⇒⇔ eq) ⟨$⟩ here P.refl
... | ()
not-index-cong {xs = _ ∷ _} {xs′ = []   } eq
  with Equivalence.to   (⇒⇔ eq) ⟨$⟩ here P.refl
... | ()

-- not-index is correct, assuming that propositional equality is
-- extensional.

not-index-correct :
  Extensionality zero zero →
  ∀ {R} (xs : List R) → tt ∈ not-index xs ↔ ∄ λ x → x ∈ xs
not-index-correct ext [] = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = from∘to
    ; right-inverse-of = to∘from
    }
  }
  where
  to : tt ∈ [ tt ] → ∄ λ x → x ∈ []
  to _ (_ , ())

  from : (∄ λ x → x ∈ []) → tt ∈ [ tt ]
  from _ = here P.refl

  to∘from : (p : ∄ λ x → x ∈ []) → to (from p) ≡ p
  to∘from p = ext helper
    where
    helper : (∈[] : ∃ λ x → x ∈ []) → to (from p) ∈[] ≡ p ∈[]
    helper (_ , ())

  from∘to : (p : tt ∈ [ tt ]) → from (to p) ≡ p
  from∘to (here P.refl) = P.refl
  from∘to (there ())

not-index-correct ext (x ∷ xs) = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = λ ()
    ; right-inverse-of = to∘from
    }
  }
  where
  ys = x ∷ xs

  to : tt ∈ [] → ∄ λ y → y ∈ ys
  to ()

  from : (∄ λ y → y ∈ ys) → tt ∈ []
  from y∉∷ with y∉∷ (-, here P.refl)
  ... | ()

  to∘from : (p : ∄ λ y → y ∈ ys) → to (from p) ≡ p
  to∘from y∉∷ with y∉∷ (-, here P.refl)
  ... | ()

------------------------------------------------------------------------
-- Not

-- ¬_ is defined as a pointwise lifting of not-index. Note that ¬_
-- preserves parser and language equality, but not the
-- sub-/superparser and sub-/superlanguage relations.

private
  module Not {R : Set} =
    Pointwise ⊥ R ⌊_⌋⇔ (const not-index) (const not-index-cong)

infix 60 ¬_ ¬-cong_

-- ¬ p returns a result if p doesn't.

¬_ : ∀ {Tok R xs} → Parser Tok R xs → Parser Tok ⊤ (not-index xs)
¬_ = Not.lift fail

-- D distributes over ¬_.

D-¬ : ∀ {Tok R xs t} (p : Parser Tok R xs) → D t (¬ p) ≅P ¬ D t p
D-¬ = Not.D-lift fail

-- ¬_ preserves equality.

¬-cong_ : ∀ {k Tok R xs xs′}
            {p : Parser Tok R xs} {p′ : Parser Tok R xs′} →
          p ∼[ ⌊ k ⌋⇔ ]P p′ → ¬ p ∼[ ⌊ k ⌋⇔ ]P ¬ p′
¬-cong_ = Not.lift-cong C.fail

-- ¬_ is correct (assuming that propositional equality is
-- extensional).

correct : (∀ {ℓ} → Extensionality ℓ zero) →
          ∀ {Tok R xs s} (p : Parser Tok R xs) →
          tt ∈ ¬ p · s ↔ ∄ λ x → x ∈ p · s
correct ext =
  Not.lift-property
    (λ _ G H → H tt ↔ ∄ G)
    (λ _ G↔G′ H↔H′ →
       Iso.Related-cong
         (H↔H′ tt)
         (Iso.→-cong ext ext (Σ.cong Inv.id λ {x} → G↔G′ x) Inv.id))
    (not-index-correct ext _)
    fail

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Issue1039 where
open import Common.Level

Test : ∀ {a b} → Set a → Set (a ⊔ b) → Set a
Test X Y = X

test : Set (lsuc lzero)
test = Test Set (Set (lsuc lzero))

test₂ : ∀ {l} → Set (lsuc l)
test₂ {l} = Test (Set l) (Set (lsuc l))


text:
module Numeral.Natural.Function.Coprimalize where

open import Data.Tuple
open import Numeral.Natural
open import Numeral.Natural.Function.GreatestCommonDivisor
open import Numeral.Natural.Oper.FlooredDivision

coprimalize : (ℕ ⨯ ℕ) → (ℕ ⨯ ℕ)
coprimalize(x , y) = ((x ⌊/⌋₀ gcd(x)(y)) , (y ⌊/⌋₀ gcd(x)(y)))

{- TODO: Maybe prove something like (b ∣ a) → ((d ∣ (a / b)) ↔ ((d ∣ a) ∧ (d ∤ b))) if it holds?
open import Numeral.Natural.Coprime
open import Relator.Equals

Coprime-coprimalize : ∀{xy} → uncurry Coprime(coprimalize xy)
Coprime.proof Coprime-coprimalize nx ny = {!!} where

n ∣ (x ⌊/⌋₀ gcd(x)(y))
(n ∣ x) ∧ (n ∤ gcd(x)(y))
-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of n-ary products
------------------------------------------------------------------------

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

module Data.Vec.Recursive.Properties where

open import Level using (Level)
open import Data.Nat.Base hiding (_^_)
open import Data.Product
open import Data.Vec.Recursive
open import Data.Vec.Base using (Vec; _∷_)
open import Function.Inverse using (_↔_; inverse)
open import Relation.Binary.PropositionalEquality as P
open ≡-Reasoning

private
  variable
    a : Level
    A : Set a

------------------------------------------------------------------------
-- Basic proofs

cons-head-tail-identity : ∀ n (as : A ^ suc n) → cons n (head n as) (tail n as) ≡ as
cons-head-tail-identity 0       as = P.refl
cons-head-tail-identity (suc n) as = P.refl

head-cons-identity : ∀ n a (as : A ^ n) → head n (cons n a as) ≡ a
head-cons-identity 0       a as = P.refl
head-cons-identity (suc n) a as = P.refl

tail-cons-identity : ∀ n a (as : A ^ n) → tail n (cons n a as) ≡ as
tail-cons-identity 0       a as = P.refl
tail-cons-identity (suc n) a as = P.refl

append-cons-commute : ∀ m n a (xs : A ^ m) ys →
  append (suc m) n (cons m a xs) ys ≡ cons (m + n) a (append m n xs ys)
append-cons-commute 0       n a xs ys = P.refl
append-cons-commute (suc m) n a xs ys = P.refl

append-splitAt-identity : ∀ m n (as : A ^ (m + n)) → uncurry (append m n) (splitAt m n as) ≡ as
append-splitAt-identity 0       n as = P.refl
append-splitAt-identity (suc m) n as = begin
  let x         = head (m + n) as in
  let (xs , ys) = splitAt m n (tail (m + n) as) in
  append (suc m) n (cons m (head (m + n) as) xs) ys
    ≡⟨ append-cons-commute m n x xs ys ⟩
  cons (m + n) x (append m n xs ys)
    ≡⟨ P.cong (cons (m + n) x) (append-splitAt-identity m n (tail (m + n) as)) ⟩
  cons (m + n) x (tail (m + n) as)
    ≡⟨ cons-head-tail-identity (m + n) as ⟩
  as
    ∎

------------------------------------------------------------------------
-- Conversion to and from Vec

fromVec∘toVec : ∀ n (xs : A ^ n) → fromVec (toVec n xs) ≡ xs
fromVec∘toVec 0       _  = P.refl
fromVec∘toVec (suc n) xs = begin
  cons n (head n xs) (fromVec (toVec n (tail n xs)))
    ≡⟨ P.cong (cons n (head n xs)) (fromVec∘toVec n (tail n xs)) ⟩
  cons n (head n xs) (tail n xs)
    ≡⟨ cons-head-tail-identity n xs ⟩
  xs ∎

toVec∘fromVec : ∀ {n} (xs : Vec A n) → toVec n (fromVec xs) ≡ xs
toVec∘fromVec             Vec.[]       = P.refl
toVec∘fromVec {n = suc n} (x Vec.∷ xs) = begin
  head n (cons n x (fromVec xs)) Vec.∷ toVec n (tail n (cons n x (fromVec xs)))
    ≡⟨ P.cong₂ (λ x xs → x Vec.∷ toVec n xs) hd-prf tl-prf ⟩
  x Vec.∷ toVec n (fromVec xs)
    ≡⟨ P.cong (x Vec.∷_) (toVec∘fromVec xs) ⟩
  x Vec.∷ xs
    ∎ where

  hd-prf = head-cons-identity _ x (fromVec xs)
  tl-prf = tail-cons-identity _ x (fromVec xs)

↔Vec : ∀ n → A ^ n ↔ Vec A n
↔Vec n = inverse (toVec n) fromVec (fromVec∘toVec n) toVec∘fromVec


text:
-- This is mostly based on the ``Dependently-typed Functional Programming''
-- lecture from Pierre-Evariste Dagand (17--18, MPRI).
-- ref: https://gitlab.inria.fr/fpottier/mpri-2.4-public/

module lambda.stlc where

open import Relation.Binary.PropositionalEquality
open import Function hiding (id)
open import Data.Product
open import Agda.Builtin.Unit

open import lambda.stack

infixr 50 _⇒_

data type : Set where
  unit : type
  _⇒_ : type → type → type

context : Set
context = stack type

data _⊢_ (Γ : context) : type → Set where
  lam : ∀ {A B} → Γ ▸ A ⊢ B → Γ ⊢ A ⇒ B
  var : ∀ {A} → A ∈ Γ → Γ ⊢ A
  app : ∀ {A B} → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
  tt : Γ ⊢ unit

module norm where

  infix 30 _⊢ⁿ_
  infix 30 _⊢ᵉ_
  infix 40 _⟶_
  infix 45 _⟦⇒⟧_
  infix 50 _⟦×⟧_

  data _⊢ᵉ_ (Γ : context) : type → Set
  data _⊢ⁿ_ (Γ : context) : type → Set

  data _⊢ⁿ_ (Γ : context) where
    lam : ∀ {A B} → Γ ▸ A ⊢ⁿ B → Γ ⊢ⁿ A ⇒ B
    tt : Γ ⊢ⁿ unit
    ground : Γ ⊢ᵉ unit → Γ ⊢ⁿ unit

  data _⊢ᵉ_ (Γ : context) where
    var : ∀ {A} → A ∈ Γ → Γ ⊢ᵉ A
    app : ∀ {A B} → Γ ⊢ᵉ A ⇒ B → Γ ⊢ⁿ A → Γ ⊢ᵉ B

  ⌊_⌋ⁿ : ∀ {Γ A} → Γ ⊢ⁿ A → Γ ⊢ A
  ⌊_⌋ᵉ : ∀ {Γ A} → Γ ⊢ᵉ A → Γ ⊢ A

  ⌊ lam x ⌋ⁿ = lam ⌊ x ⌋ⁿ
  ⌊ tt ⌋ⁿ = tt
  ⌊ ground x ⌋ⁿ = ⌊ x ⌋ᵉ

  ⌊ var x ⌋ᵉ = var x
  ⌊ app x y ⌋ᵉ = app ⌊ x ⌋ᵉ ⌊ y ⌋ⁿ

  record sem : Set₁ where
    field
      _⊢ : context → Set
      ren : ∀ {Γ Δ} → Γ ⊇ Δ → Δ ⊢ → Γ ⊢

  _⟶_ : (A B : sem) → Set
  A ⟶ B = ∀ {Γ} → Γ ⊢A → Γ ⊢B
    where open sem A renaming (_⊢ to _⊢A)
          open sem B renaming (_⊢ to _⊢B)

  renameⁿ : ∀ {Γ Δ T} → Γ ⊇ Δ → Δ ⊢ⁿ T → Γ ⊢ⁿ T
  renameᵉ : ∀ {Γ Δ T} → Γ ⊇ Δ → Δ ⊢ᵉ T → Γ ⊢ᵉ T

  renameⁿ wk (lam b)       = lam (renameⁿ (keep wk) b)
  renameⁿ wk (ground grnd) = ground (renameᵉ wk grnd)
  renameⁿ wk tt            = tt

  renameᵉ wk (var v)       = var (shift wk v)
  renameᵉ wk (app f s)     = app (renameᵉ wk f) (renameⁿ wk s)

  renameⁿ-id : ∀ {Γ T} → (x : Γ ⊢ⁿ T) → renameⁿ id x ≡ x
  renameᵉ-id : ∀ {Γ T} → (x : Γ ⊢ᵉ T) → renameᵉ id x ≡ x

  renameⁿ-id (lam x) = cong lam (renameⁿ-id x)
  renameⁿ-id tt = refl
  renameⁿ-id (ground x) = cong ground (renameᵉ-id x)

  renameᵉ-id (var x) = cong var (shift-id x)
  renameᵉ-id (app x y) = cong₂ app (renameᵉ-id x) (renameⁿ-id y)

  semⁿ : type → sem
  semⁿ T = record {
    _⊢ = λ Γ → Γ ⊢ⁿ T ;
    ren = renameⁿ }

  semᵉ : type → sem
  semᵉ T = record {
    _⊢ = λ Γ → Γ ⊢ᵉ T ;
    ren = renameᵉ }

  ⟦unit⟧ : sem
  ⟦unit⟧ = semⁿ unit

  ⟦tt⟧ : ∀ {P} → P ⟶ ⟦unit⟧
  ⟦tt⟧ ρ = tt

  _⟦⇒⟧_ : sem → sem → sem
  P ⟦⇒⟧ Q = record {
    _⊢ = λ Γ → ∀ {Δ} → Δ ⊇ Γ → Δ ⊢P → Δ ⊢Q ;
    ren = λ wk₁ k wk₂ → k (wk₂ ∘⊇ wk₁) }
    where open sem P renaming (_⊢ to _⊢P)
          open sem Q renaming (_⊢ to _⊢Q)

  _⟦×⟧_ : sem → sem → sem
  P ⟦×⟧ Q = record { _⊢ = λ Γ → (Γ ⊢P) × (Γ ⊢Q)
                   ; ren = λ { wk (x , y) → ( ren-P wk x , ren-Q wk y ) } }
    where open sem P renaming (_⊢ to _⊢P ; ren to ren-P)
          open sem Q renaming (_⊢ to _⊢Q ; ren to ren-Q)

  ⟦lam⟧ : ∀ {P Q R} → P ⟦×⟧ Q ⟶ R → P ⟶ Q ⟦⇒⟧ R
  ⟦lam⟧ {P} η p = λ wk q → η (ren-P wk p , q)
    where open sem P renaming (ren to ren-P)

  ⟦app⟧ : ∀ {P Q R} → P ⟶ Q ⟦⇒⟧ R → P ⟶ Q → P ⟶ R
  ⟦app⟧ η μ = λ px → η px id (μ px)

  ⟦_⟧ : type → sem
  ⟦ unit ⟧  = ⟦unit⟧
  ⟦ S ⇒ T ⟧ = ⟦ S ⟧ ⟦⇒⟧ ⟦ T ⟧

  ⊤̂ : sem
  ⊤̂ = record { _⊢ = λ _ → ⊤
             ; ren = λ _ _ → tt }

  ⟦_⟧c : (Γ : context) → sem
  ⟦ ε ⟧c     = ⊤̂
  ⟦ Γ ▸ T ⟧c = ⟦ Γ ⟧c ⟦×⟧ ⟦ T ⟧

  _⟦⊢⟧_ : context → type → Set
  Γ ⟦⊢⟧ T = ⟦ Γ ⟧c ⟶ ⟦ T ⟧

  lookup : ∀ {Γ T} → T ∈ Γ → Γ ⟦⊢⟧ T
  lookup here (_ , v)      = v
  lookup (there x) (γ , _) = lookup x γ

  eval : ∀ {Γ T} → Γ ⊢ T → Γ ⟦⊢⟧ T
  eval {Γ} {A ⇒ B} (lam x) = ⟦lam⟧ {⟦ Γ ⟧c} {⟦ A ⟧} {⟦ B ⟧} (eval x)
  eval (var x) = lookup x
  eval {Γ} {B} (app {A} x y) = ⟦app⟧ {⟦ Γ ⟧c} {⟦ A ⟧} {⟦ B ⟧} (eval x) (eval y)
  eval {Γ} tt = ⟦tt⟧ {⟦ Γ ⟧c}

  [_]⊢_ : context → type → Set
  [ Γ ]⊢ T = Γ ⊢⟦T⟧
    where open sem ⟦ T ⟧ renaming (_⊢ to _⊢⟦T⟧)

  [_]⊢c_ : context → context → Set
  [ Γ ]⊢c Δ = Γ ⊢⟦Δ⟧c
    where open sem ⟦ Δ ⟧c renaming (_⊢ to _⊢⟦Δ⟧c)

  reify : ∀ {T Γ} → [ Γ ]⊢ T  → Γ ⊢ⁿ T
  reflect : ∀ {Γ} → (T : type) → Γ ⊢ᵉ T → [ Γ ]⊢ T

  reify {unit} v = v
  reify {A ⇒ B} x = lam (reify (x (skip id) (reflect A (var here))))

  reflect unit x = ground x
  reflect (A ⇒ B) x = λ w s → reflect B (app (ren w x) (reify s))
    where open sem (semᵉ (A ⇒ B))

  reify-id : ∀ {Γ T} → Γ ⟦⊢⟧ T → Γ ⊢ⁿ T
  reify-id {Γ} x = reify (x (id-c Γ))
    where
      open sem
      id-c : ∀ Γ → [ Γ ]⊢c Γ
      id-c ε = tt
      id-c (Γ ▸ T) = ren ⟦ Γ ⟧c (skip id) (id-c Γ) , reflect T (var here)

  norm : ∀ {Γ T} → Γ ⊢ T → Γ ⊢ⁿ T
  norm = reify-id ∘ eval


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

module Categories.Bicategory.Bigroupoid where

open import Level
open import Function using (_$_)
open import Data.Product using (Σ; _,_)

open import Categories.Category
open import Categories.Category.Equivalence using (WeakInverse)
open import Categories.Category.Product
open import Categories.Category.Groupoid using (IsGroupoid)
open import Categories.Bicategory
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties
open import Categories.Functor.Bifunctor.Properties
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; NaturalIsomorphism)

import Categories.Morphism as Mor
import Categories.Morphism.Properties as MP
import Categories.Morphism.Reasoning as MR

-- https://link.springer.com/article/10.1023/A:1011270417127
record IsBigroupoid {o ℓ e t} (C : Bicategory o ℓ e t) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
  open Bicategory C public

  field
    hom-isGroupoid : ∀ A B → IsGroupoid (hom A B)
    hom[_,_]⁻¹     : ∀ A B → Functor (hom A B) (hom B A)
    cancel         : ∀ A B → ⊚ ∘F (hom[ A , B ]⁻¹ ※ idF) ≃ const id₁
    cancel′        : ∀ A B → ⊚ ∘F (idF ※ hom[ A , B ]⁻¹) ≃ const id₁

  module hom⁻¹ {A B}   = Functor (hom[ A , B ]⁻¹)
  module cancel {A B}  = NaturalIsomorphism (cancel A B)
  module cancel′ {A B} = NaturalIsomorphism (cancel′ A B)

  infix 13 _⁻¹ _⁻¹′

  _⁻¹ : ∀ {A B} → A ⇒₁ B → B ⇒₁ A
  _⁻¹ = hom⁻¹.F₀

  _⁻¹′ : ∀ {A B} {f g : A ⇒₁ B} → f ⇒₂ g → f ⁻¹ ⇒₂ g ⁻¹
  _⁻¹′ = hom⁻¹.F₁

  open hom.Commutation

  field
    pentagon₁ : ∀ {A B} {f : A ⇒₁ B} →
                  [ (f ∘ₕ f ⁻¹) ∘ₕ f ⇒ f ]⟨
                    associator.from      ⇒⟨ f ∘ₕ f ⁻¹ ∘ₕ f ⟩
                    f ▷ cancel.⇒.η f     ⇒⟨ f ∘ₕ id₁ ⟩
                    unitorʳ.from
                  ≈ cancel′.⇒.η f ◁ f    ⇒⟨ id₁ ∘ₕ f ⟩
                    unitorˡ.from
                  ⟩
    pentagon₂ : ∀ {A B} {f : A ⇒₁ B} →
                  [ (f ⁻¹ ∘ₕ f) ∘ₕ f ⁻¹ ⇒ f ⁻¹ ]⟨
                    associator.from            ⇒⟨ f ⁻¹ ∘ₕ f ∘ₕ f ⁻¹ ⟩
                    f ⁻¹ ▷ cancel′.⇒.η f       ⇒⟨ f ⁻¹ ∘ₕ id₁ ⟩
                    unitorʳ.from
                  ≈ cancel.⇒.η f ◁ f ⁻¹        ⇒⟨ id₁ ∘ₕ f ⁻¹ ⟩
                    unitorˡ.from
                  ⟩

  private
    variable
      A B : Obj
      f g : A ⇒₁ B
      α β : f ⇒₂ g

    open hom.HomReasoning
    module MR′ {A B} where
      open MR (hom A B) public
      open Mor (hom A B) public
      open MP (hom A B) public
    open MR′
    module ℱ = Functor

  cancel-comm : ∀ {α : f ⇒₂ g} → cancel.⇒.η g ∘ᵥ (α ⁻¹′ ⊚₁ α) ≈ cancel.⇒.η f
  cancel-comm {α = α} = cancel.⇒.commute α ○ identity₂ˡ

  cancel⁻¹-comm : ∀ {α : f ⇒₂ g} → (α ⁻¹′ ⊚₁ α) ∘ᵥ cancel.⇐.η f ≈ cancel.⇐.η g
  cancel⁻¹-comm {α = α} = ⟺ (cancel.⇐.commute α) ○ identity₂ʳ

  cancel′-comm : ∀ {α : f ⇒₂ g} → cancel′.⇒.η g ∘ᵥ (α ⊚₁ α ⁻¹′) ≈ cancel′.⇒.η f
  cancel′-comm {α = α} = cancel′.⇒.commute α ○ identity₂ˡ

  cancel′⁻¹-comm : ∀ {α : f ⇒₂ g} → (α ⊚₁ α ⁻¹′) ∘ᵥ cancel′.⇐.η f ≈ cancel′.⇐.η g
  cancel′⁻¹-comm {α = α} = ⟺ (cancel′.⇐.commute α) ○ identity₂ʳ

  hom⁻¹⁻¹≃id : ∀ {A B} → hom[ B , A ]⁻¹ ∘F hom[ A , B ]⁻¹ ≃ idF
  hom⁻¹⁻¹≃id {A} {B} = record
    { F⇒G = ntHelper record
      { η       = λ f → (((unitorˡ.from ∘ᵥ cancel.⇒.η (f ⁻¹) ◁ f) ∘ᵥ associator.to) ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇐.η f) ∘ᵥ unitorʳ.to
      ; commute = λ {f g} α → begin
        ((((unitorˡ.from ∘ᵥ cancel.⇒.η (g ⁻¹) ◁ g) ∘ᵥ associator.to) ∘ᵥ g ⁻¹ ⁻¹ ▷ cancel.⇐.η g) ∘ᵥ unitorʳ.to) ∘ᵥ α ⁻¹′ ⁻¹′
          ≈˘⟨ pushʳ ◁-∘ᵥ-λ⁻¹ ⟩
        (((unitorˡ.from ∘ᵥ cancel.⇒.η (g ⁻¹) ◁ g) ∘ᵥ associator.to) ∘ᵥ g ⁻¹ ⁻¹ ▷ cancel.⇐.η g) ∘ᵥ ((α ⁻¹′ ⁻¹′ ◁ id₁) ∘ᵥ unitorʳ.to)
          ≈⟨ center ◁-▷-exchg ⟩
        ((unitorˡ.from ∘ᵥ cancel.⇒.η (g ⁻¹) ◁ g) ∘ᵥ associator.to) ∘ᵥ (α ⁻¹′ ⁻¹′ ◁ (g ⁻¹ ∘ₕ g) ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇐.η g) ∘ᵥ unitorʳ.to
          ≈⟨ center (⟺ assoc₂ ○ hom.∘-resp-≈ assoc⁻¹-◁-∘ₕ (ℱ.F-resp-≈ ((f ⁻¹ ⁻¹) ⊚-) (⟺ cancel⁻¹-comm))) ⟩
        (unitorˡ.from ∘ᵥ cancel.⇒.η (g ⁻¹) ◁ g) ∘ᵥ ((α ⁻¹′ ⁻¹′ ◁ g ⁻¹ ◁ g ∘ᵥ associator.to) ∘ᵥ f ⁻¹ ⁻¹ ▷ ((α ⁻¹′ ⊚₁ α) ∘ᵥ cancel.⇐.η f)) ∘ᵥ unitorʳ.to
          ≈⟨ refl ⟩∘⟨ (hom.∘-resp-≈ʳ (ℱ.homomorphism ((f ⁻¹ ⁻¹) ⊚-)) ○ center (⊚-assoc.⇐.commute _) ○ center⁻¹ ([ ⊚ ]-merge (⟺ [ ⊚ ]-decompose₁) identity₂ˡ) refl) ⟩∘⟨ refl ⟩
        (unitorˡ.from ∘ᵥ cancel.⇒.η (g ⁻¹) ◁ g) ∘ᵥ (((α ⁻¹′ ⁻¹′ ⊚₁ α ⁻¹′) ⊚₁ α) ∘ᵥ associator.to ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇐.η f) ∘ᵥ unitorʳ.to
          ≈˘⟨ assoc₂ ⟩
        ((unitorˡ.from ∘ᵥ cancel.⇒.η (g ⁻¹) ◁ g) ∘ᵥ (((α ⁻¹′ ⁻¹′ ⊚₁ α ⁻¹′) ⊚₁ α) ∘ᵥ associator.to ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇐.η f)) ∘ᵥ unitorʳ.to
          ≈⟨ center ([ ⊚ ]-merge cancel-comm identity₂ˡ) ⟩∘⟨refl ⟩
        (unitorˡ.from ∘ᵥ cancel.⇒.η (f ⁻¹) ⊚₁ α ∘ᵥ associator.to ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇐.η f) ∘ᵥ unitorʳ.to
          ≈˘⟨ (assoc₂ ○ assoc₂) ⟩∘⟨refl ⟩
        (((unitorˡ.from ∘ᵥ cancel.⇒.η (f ⁻¹) ⊚₁ α) ∘ᵥ associator.to) ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇐.η f) ∘ᵥ unitorʳ.to
          ≈⟨ (hom.∘-resp-≈ʳ [ ⊚ ]-decompose₂) ⟩∘⟨refl ⟩∘⟨refl ⟩∘⟨refl ⟩
        (((unitorˡ.from ∘ᵥ id₁ ▷ α ∘ᵥ cancel.⇒.η (f ⁻¹) ◁ f) ∘ᵥ associator.to) ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇐.η f) ∘ᵥ unitorʳ.to
          ≈⟨ pullˡ ρ-∘ᵥ-▷ ⟩∘⟨refl ⟩∘⟨refl ⟩∘⟨refl ⟩
        ((((α ∘ᵥ unitorˡ.from) ∘ᵥ cancel.⇒.η (f ⁻¹) ◁ f) ∘ᵥ associator.to) ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇐.η f) ∘ᵥ unitorʳ.to
          ≈⟨ (assoc₂ ○ assoc₂ ○ assoc₂ ○ assoc₂) ⟩
        α ∘ᵥ unitorˡ.from ∘ᵥ cancel.⇒.η (f ⁻¹) ◁ f ∘ᵥ associator.to ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇐.η f ∘ᵥ unitorʳ.to
          ≈˘⟨ refl⟩∘⟨ (assoc₂ ○ assoc₂ ○ assoc₂) ⟩
        α ∘ᵥ (((unitorˡ.from ∘ᵥ cancel.⇒.η (f ⁻¹) ◁ f) ∘ᵥ associator.to) ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇐.η f) ∘ᵥ unitorʳ.to
          ∎
      }
    ; F⇐G = ntHelper record
      { η       = λ f → unitorʳ.from ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇒.η f ∘ᵥ associator.from ∘ᵥ cancel.⇐.η (f ⁻¹) ◁ f ∘ᵥ unitorˡ.to
      ; commute = λ {f g} α → begin
        (unitorʳ.from ∘ᵥ g ⁻¹ ⁻¹ ▷ cancel.⇒.η g ∘ᵥ associator.from ∘ᵥ cancel.⇐.η (g ⁻¹) ◁ g ∘ᵥ unitorˡ.to) ∘ᵥ α
          ≈⟨ assoc₂ ○ hom.∘-resp-≈ʳ (assoc₂ ○ hom.∘-resp-≈ʳ (assoc₂ ○ hom.∘-resp-≈ʳ assoc₂)) ⟩
        unitorʳ.from ∘ᵥ g ⁻¹ ⁻¹ ▷ cancel.⇒.η g ∘ᵥ associator.from ∘ᵥ cancel.⇐.η (g ⁻¹) ◁ g ∘ᵥ unitorˡ.to ∘ᵥ α
          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟺ ▷-∘ᵥ-ρ⁻¹ ⟩
        unitorʳ.from ∘ᵥ g ⁻¹ ⁻¹ ▷ cancel.⇒.η g ∘ᵥ associator.from ∘ᵥ cancel.⇐.η (g ⁻¹) ◁ g ∘ᵥ id₁ ▷ α ∘ᵥ unitorˡ.to
          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (⟺ [ ⊚ ]-decompose₁ ○ ⊚.F-resp-≈ (⟺ cancel⁻¹-comm , refl)) ⟩
        unitorʳ.from ∘ᵥ g ⁻¹ ⁻¹ ▷ cancel.⇒.η g ∘ᵥ associator.from ∘ᵥ (α ⁻¹′ ⁻¹′ ⊚₁ α ⁻¹′ ∘ᵥ cancel.⇐.η (f ⁻¹)) ⊚₁ α ∘ᵥ unitorˡ.to
          ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ hom.∘-resp-≈ˡ ([ ⊚ ]-merge refl identity₂ʳ) ⟩
        unitorʳ.from ∘ᵥ g ⁻¹ ⁻¹ ▷ cancel.⇒.η g ∘ᵥ associator.from ∘ᵥ ((α ⁻¹′ ⁻¹′ ⊚₁ α ⁻¹′) ⊚₁ α ∘ᵥ cancel.⇐.η (f ⁻¹) ◁ f) ∘ᵥ unitorˡ.to
          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ center⁻¹ (⊚-assoc.⇒.commute _) refl ⟩
        unitorʳ.from ∘ᵥ g ⁻¹ ⁻¹ ▷ cancel.⇒.η g ∘ᵥ (α ⁻¹′ ⁻¹′ ⊚₁ α ⁻¹′ ⊚₁ α ∘ᵥ associator.from) ∘ᵥ cancel.⇐.η (f ⁻¹) ◁ f ∘ᵥ unitorˡ.to
          ≈⟨ refl⟩∘⟨ (hom.∘-resp-≈ʳ assoc₂ ○ pullˡ ([ ⊚ ]-merge identity₂ˡ cancel-comm)) ⟩
        unitorʳ.from ∘ᵥ (α ⁻¹′ ⁻¹′) ⊚₁ (cancel.⇒.η f) ∘ᵥ associator.from ∘ᵥ cancel.⇐.η (f ⁻¹) ◁ f ∘ᵥ unitorˡ.to
          ≈⟨ refl⟩∘⟨ (hom.∘-resp-≈ˡ [ ⊚ ]-decompose₁ ○ assoc₂) ⟩
        unitorʳ.from ∘ᵥ (α ⁻¹′ ⁻¹′) ◁ id₁ ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇒.η f ∘ᵥ associator.from ∘ᵥ cancel.⇐.η (f ⁻¹) ◁ f ∘ᵥ unitorˡ.to
          ≈⟨ (pullˡ λ-∘ᵥ-◁) ○ assoc₂ ⟩
        α ⁻¹′ ⁻¹′ ∘ᵥ unitorʳ.from ∘ᵥ f ⁻¹ ⁻¹ ▷ cancel.⇒.η f ∘ᵥ associator.from ∘ᵥ cancel.⇐.η (f ⁻¹) ◁ f ∘ᵥ unitorˡ.to
          ∎
      }
    ; iso = λ f → Iso-∘ (Iso-swap (unitʳ.iso _)) $
                  Iso-∘ ([ (f ⁻¹ ⁻¹) ⊚- ]-resp-Iso (Iso-swap (cancel.iso f))) $
                  Iso-∘ (Iso-swap associator.iso) $
                  Iso-∘ ([ -⊚ f ]-resp-Iso (cancel.iso _))
                        (unitˡ.iso _)
    }

  hom⁻¹-weakInverse : ∀ {A B} → WeakInverse hom[ A , B ]⁻¹ hom[ B , A ]⁻¹
  hom⁻¹-weakInverse = record { F∘G≈id = hom⁻¹⁻¹≃id ; G∘F≈id = hom⁻¹⁻¹≃id }

  module hom⁻¹-weakInverse {A B} = WeakInverse (hom⁻¹-weakInverse {A} {B})

  open hom⁻¹-weakInverse using () renaming (F⊣G to hom⁻¹-⊣Equivalence) public

-- A bigroupoid is a bicategory that has a bigroupoid structure

record Bigroupoid (o ℓ e t : Level) : Set (suc (o ⊔ ℓ ⊔ e ⊔ t)) where
  field
    bicategory   : Bicategory o ℓ e t
    isBigroupoid : IsBigroupoid bicategory

  open IsBigroupoid isBigroupoid public


text:
{-# OPTIONS --guardedness #-}

module Cubical.Codata.Stream where

open import Cubical.Codata.Stream.Base public

open import Cubical.Codata.Stream.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
module Issue217 where

record A : Set where
  ⊥ : Set
  ⊥ = ⊥

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Categories.Adjoint.Instance.01-Truncation where

-- The adjunction between (0,1)-truncation and the inclusion functor
-- from Posets to Categories.

open import Data.Product using (_,_)
import Function
open import Relation.Binary using (Poset)
open import Relation.Binary.OrderMorphism using (_⇒-Poset_)

open import Categories.Adjoint using (_⊣_)
open import Categories.Category.Construction.Thin using (Thin)
open import Categories.Category using (Category)
open import Categories.Category.Instance.Cats using (Cats)
open import Categories.Category.Instance.Posets using (Posets)
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Instance.01-Truncation using (Trunc)
open import Categories.NaturalTransformation
  using (NaturalTransformation; ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (refl)

open _⇒-Poset_

-- The inclusion functor from Posets to Categories

Inclusion : ∀ {c ℓ₁ ℓ₂} e → Functor (Posets c ℓ₁ ℓ₂) (Cats c ℓ₂ e)
Inclusion {c} {ℓ₁} e = record
  { F₀           = Thin e
  ; F₁           = λ f → record { F₀ = fun f ; F₁ = monotone f }
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = λ {A B f g} f≗g →
    let open Poset B
    in record
    { F⇒G = record { η = λ _ → reflexive f≗g          }
    ; F⇐G = record { η = λ _ → reflexive (Eq.sym f≗g) }
    }
  }

-- Trunc is left-adjoint to the inclusion functor from Setoids to Groupoids

TruncAdj : ∀ {o ℓ e} → Trunc ⊣ Inclusion {o} {ℓ} e
TruncAdj {o} {ℓ} {e} = record
  { unit   = unit
  ; counit = counit
  ; zig    = λ {C} → id C , id C
  ; zag    = refl
  }
  where
    open Category

    unit : NaturalTransformation idF (Inclusion e ∘F Trunc)
    unit = record
      { η           = λ _ → record { F₀ = Function.id ; F₁ = Function.id }
      ; commute     = λ _ → refl
      ; sym-commute = λ _ → refl
      }

    counit : NaturalTransformation (Trunc ∘F Inclusion e) idF
    counit = ntHelper record
      { η       = λ _ → record { fun = Function.id ; monotone = Function.id }
      ; commute = λ {_ D} _ → Poset.Eq.refl D
      }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories