module Semantics.CwF where

open import Prelude
open import Setoid

{- A setoid enriched category-with-families whose objects are semantic
contexts (elements of the universe π’ž). -}

----------------------------------------------------------------------
-- Morphisms
----------------------------------------------------------------------
record Hom (C D : ∣ π’ž ∣) : Set where
  {-  We could define morphisms between context codes by
    Hom : ∣ π’ž ∣ β†’ ∣ π’ž ∣ β†’ Set
    Hom C D = ∣ β„° β€² C ⟢ β„° β€² D ∣
  but to aid instance resolution it is better to use this record type,
  which isomorphic to that. -}
  constructor mkHom
  infix 8 ∣_∣
  field
    ∣_∣ : βˆ₯ β„° βˆ₯ C β†’ βˆ₯ β„° βˆ₯ D
    cng :
      (c c' : βˆ₯ β„° βˆ₯ C)
      (_ : β„° β€² C βˆ‹ c ~ c')
      β†’ --------------------
      β„° β€² D βˆ‹ ∣ c ∣ ~ ∣ c' ∣

open Hom public

ℋℴ𝓂 : Setd[ π’ž βŠ— π’ž ]

βˆ₯ ℋℴ𝓂 βˆ₯ (C , D) = Hom C D
ℋℴ𝓂 βˆ‹ (C , D) , f β‰ˆ (C' , D') , f' =
  (c : βˆ₯ β„° βˆ₯ C)
  (c' : βˆ₯ β„° βˆ₯ C')
  (_ : β„° βˆ‹ C , c β‰ˆ C' , c')
  β†’ ------------------------------
  β„° βˆ‹ D , ∣ f ∣ c β‰ˆ D' , ∣ f' ∣ c'
hrfl ℋℴ𝓂 (C , D) f _ _ e = cng f _ _ e
hsym ℋℴ𝓂 (e , e') f c c' e'' =
  hsymᢜ e' (f c' c (hsymᢜ (symᢜ e) e''))
htrs ℋℴ𝓂 (e₁ , e₁') (eβ‚‚ , eβ‚‚') f₁ fβ‚‚ c c' e =
  htrsᢜ e₁' eβ‚‚'
    (f₁ c (coeᢜ e₁ c) (cohᢜ e₁ c))
    (fβ‚‚ (coeᢜ e₁ c) c'
      ((htrsᢜ (symᢜ e₁) (trsᢜ e₁ eβ‚‚) (hsymᢜ e₁ (cohᢜ e₁ c)) e)))
∣ coe ℋℴ𝓂 (e₁ , eβ‚‚) f ∣ c = coeᢜ eβ‚‚ (∣ f ∣ (coeᢜ (symᢜ e₁) c))
cng (coe ℋℴ𝓂 (e₁ , eβ‚‚) f) c c' e =  htrsᢜ (symᢜ eβ‚‚) eβ‚‚
  (hsymᢜ eβ‚‚ (cohᢜ eβ‚‚ (∣ f ∣(coeᢜ (symᢜ e₁) c))))
  (htrsᢜ (rflᢜ _) eβ‚‚
    (cng f _ _ (htrsᢜ e₁ (symᢜ e₁)
      (hsymᢜ (symᢜ e₁) (cohᢜ (symᢜ e₁) c))
      (htrsᢜ (rflᢜ _) (symᢜ e₁) e (cohᢜ (symᢜ e₁) c'))))
    (cohᢜ eβ‚‚ (∣ f ∣(coeᢜ (symᢜ e₁) c'))))
coh ℋℴ𝓂 (e₁ , eβ‚‚) f c c' e = htrsᢜ (rflᢜ _) eβ‚‚
  (cng f _ _ (htrsᢜ e₁ (symᢜ e₁) e (cohᢜ (symᢜ e₁) c')))
  (cohᢜ eβ‚‚ (∣ f ∣(coeᢜ (symᢜ e₁) c')))

-- Identity morphism
instance
  HomIdentity : βˆ€{C} β†’ Identity (Hom C C)
  ∣ id ⦃ HomIdentity ⦄ ∣ x = x
  cng (id ⦃ HomIdentity ⦄) _ _ = id

-- Composition of morphisms
instance
  HomComp : βˆ€{C D E} β†’
    Composition (Hom D E) (Hom C D) (Hom C E)
  ∣ _∘_ ⦃ HomComp ⦄ g f ∣ x = ∣ g ∣ (∣ f ∣ x)
  cng (_∘_ ⦃ HomComp ⦄ g f) _ _ = cng g _ _ ∘ cng f _ _

compCng :
  {C C' D D' E E' : ∣ π’ž ∣}
  {f : Hom C D}
  {f' : Hom C' D'}
  {g : Hom D E}
  {g' : Hom D' E'}
  (_ : ℋℴ𝓂 βˆ‹ (C , D) , f β‰ˆ (C' , D') , f')
  (_ : ℋℴ𝓂 βˆ‹ (D , E) , g β‰ˆ (D' , E') , g')
  β†’ ---------------------------------------------
  ℋℴ𝓂 βˆ‹ (C , E) , (g ∘ f) β‰ˆ (C' , E') , (g' ∘ f')

compCng {f = f}{f'} u v c c' w = v (∣ f ∣ c) (∣ f' ∣ c') (u c c' w)

-- Terminal morphism
unit : (C : ∣ π’ž ∣) β†’ Hom C Unit

∣ unit C ∣ _ = tt
cng (unit C) _ _ _ = tt

----------------------------------------------------------------------
-- Families and their elements
----------------------------------------------------------------------

{- We wish to ensure that, up to definitional equality, families are
sections of universes, so we begin with a definition of "universe
section" 𝒰sect, from which both families and their elements can be
defined. One could take

  𝒰sect : (l : β„•)(C : ∣ π’ž ∣) β†’ ∣ β„° β€² C ⟢ 𝒰 l ∣ β†’ Set

to be

  𝒰sect l C F = Setd[ β„° β€² C  ⊩ F * ℰ𝓁 l ]

but using the following equivalent record type seems to make life
easier. -}

record 𝒰sect
  (n : β„•)
  (C : ∣ π’ž ∣)
  (X : βˆ₯ β„° βˆ₯ C β†’ ∣ 𝒰 n ∣)
  (q : βˆ€ c c' β†’ (β„° β€² C βˆ‹ c ~ c') β†’ (𝒰 n βˆ‹ X c ~ X c'))
  : --------------------------------------------------
  Set
  where
  constructor mk𝒰sect
  infix 8 βˆ₯_βˆ₯
  field
    βˆ₯_βˆ₯ : (c : βˆ₯ β„° βˆ₯ C) β†’ βˆ₯ ℰ𝓁 n βˆ₯ (X c)
    hcng :
      (c c' : Setd[_].βˆ₯_βˆ₯ β„° C)
      (_ : β„° β€² C βˆ‹ c ~ c')
      β†’ --------------------------------
      ℰ𝓁 n βˆ‹ X c , βˆ₯_βˆ₯ c β‰ˆ X c' , βˆ₯_βˆ₯ c'

open 𝒰sect public

-- Families
Fam : β„• β†’ ∣ π’ž ∣ β†’ Set
Fam n C =
  -- Because El (1+ n) Univ ≑ U l, the following definition makes
  -- Fam n C equal to the type | β„° β€² C ⟢ 𝒰 l | of setoid mprphisms
  -- from β„° β€² C to 𝒰 l
  𝒰sect (1+ n) C (Ξ» _ β†’ Univ) (Ξ» _ _ _ β†’ rfl (𝒰 (1+ n)) Univ)

ℱ𝒢𝓂 : β„• β†’ Setd[ π’ž ]
βˆ₯ ℱ𝒢𝓂 n βˆ₯ = Fam n
ℱ𝒢𝓂 n βˆ‹ C , T β‰ˆ C' , T' =
  βˆ€ c c' β†’ (β„° βˆ‹ C , c β‰ˆ C' , c') β†’ 𝒰 n βˆ‹ βˆ₯ T βˆ₯ c ~ βˆ₯ T' βˆ₯ c'
hrfl (ℱ𝒢𝓂 n) C T = hcng T
hsym (ℱ𝒢𝓂 n) e f c c' e' =
  sym (𝒰 n) (f c' c (hsymᢜ (symᢜ e) e'))
htrs (ℱ𝒢𝓂 n) e₁ eβ‚‚ f₁ fβ‚‚ c c'' e = trs (𝒰 n)
  (f₁ c (coeᢜ e₁ c) (cohᢜ e₁ c))
  (fβ‚‚ (coeᢜ e₁ c) c'' (htrsᢜ (symᢜ e₁) (trsᢜ e₁ eβ‚‚)
    (hsymᢜ e₁ (cohᢜ e₁ c)) e))
βˆ₯ coe (ℱ𝒢𝓂 n) e T βˆ₯ c = βˆ₯ T βˆ₯ (coeᢜ (symᢜ e) c)
hcng (coe (ℱ𝒢𝓂 n) e T) c c' e' =
  hcng T _ _ (htrsᢜ e (symᢜ e)
    (hsymᢜ (symᢜ e) (cohᢜ (symᢜ e) c))
    (htrsᢜ (rflᢜ _) (symᢜ e) e' (cohᢜ (symᢜ e) c')))
coh (ℱ𝒢𝓂 n) e T c c' e' =
  hcng T _ _ (htrsᢜ e (symᢜ e) e' (cohᢜ (symᢜ e) c'))

-- Elements of families
Elem : (n : β„•)(C : ∣ π’ž ∣) β†’ Fam n C β†’ Set
Elem n C T = 𝒰sect n C βˆ₯ T βˆ₯ (hcng T)

ℰ𝓁ℯ𝓂 : (n : β„•) β†’ Setd[ π’ž ⋉ ℱ𝒢𝓂 n ]
βˆ₯ ℰ𝓁ℯ𝓂 n βˆ₯ (C , T) = Elem n C T
ℰ𝓁ℯ𝓂 n βˆ‹ (C , T) , t β‰ˆ (C' , T') , t' =
  (c : βˆ₯ β„° βˆ₯ C)
  (c' : βˆ₯ β„° βˆ₯ C')
  (_ : β„° βˆ‹ C , c β‰ˆ C' , c')
  β†’ ----------------------------------------------
  ℰ𝓁 n βˆ‹ βˆ₯ T βˆ₯ c , βˆ₯ t βˆ₯ c β‰ˆ βˆ₯ T' βˆ₯ c' , βˆ₯ t' βˆ₯ c'
hrfl (ℰ𝓁ℯ𝓂 n) _ T _ _ e = hcng T _ _ e
hsym (ℰ𝓁ℯ𝓂 n) (e , f) g c c' e' = hsym (ℰ𝓁 n)
  (f c' c (hsymᢜ (symᢜ e) e'))
  (g c' c (hsymᢜ (symᢜ e) e'))
htrs (ℰ𝓁ℯ𝓂 n) (e₁ , f₁) (eβ‚‚ , fβ‚‚) g₁ gβ‚‚ c c'' e =
  let
    c'  = coeᢜ e₁ c
    e'  = cohᢜ e₁ c
    e₁' = symᢜ e₁
  in htrs (ℰ𝓁 n)
    (f₁ c c' e')
    (fβ‚‚ c' c'' (htrsᢜ e₁' (trsᢜ e₁ eβ‚‚) (hsymᢜ e₁ e') e))
    (g₁ c c' e')
    (gβ‚‚ c' c'' (htrsᢜ e₁' (trsᢜ e₁ eβ‚‚) (hsymᢜ e₁ e') e))
βˆ₯ coe (ℰ𝓁ℯ𝓂 n) (e , f) t βˆ₯ c' =
  let
    c  = coeᢜ (symᢜ e) c'
    e' = cohᢜ (symᢜ e) c'
  in
  coe (ℰ𝓁 n) (f c c' (hsymᢜ (symᢜ e) e')) (βˆ₯ t βˆ₯ c)
hcng (coe (ℰ𝓁ℯ𝓂 n) {x' = _ , T'} (e , f) t) c₁ cβ‚‚ e' =
  let
    c₁'  = coeᢜ (symᢜ e) c₁
    e₁'  = cohᢜ (symᢜ e) c₁
    cβ‚‚'  = coeᢜ (symᢜ e) cβ‚‚
    eβ‚‚'  = cohᢜ (symᢜ e) cβ‚‚
    e₁'' = f c₁' c₁ (hsymᢜ (symᢜ e) e₁')
    eβ‚‚'' = f cβ‚‚' cβ‚‚ (hsymᢜ (symᢜ e) eβ‚‚')
  in  htrs (ℰ𝓁 n)
    (sym (𝒰 n) e₁'')
    (f c₁' cβ‚‚ (htrsᢜ e (rflᢜ _) (hsymᢜ (symᢜ e) e₁') e'))
    (hsym (ℰ𝓁 n) e₁'' (coh (ℰ𝓁 n) e₁'' (βˆ₯ t βˆ₯ c₁')))
    (htrs (ℰ𝓁 n)
    (trs (𝒰 n) e₁'' (trs (𝒰 n) (hcng T' _ _ e') (sym (𝒰 n) eβ‚‚'')))
      eβ‚‚''
      (hcng t _ _ (htrsᢜ e (symᢜ e) (hsymᢜ (symᢜ e) e₁')
        (htrsᢜ (rflᢜ _) (symᢜ e) e' eβ‚‚')))
      (coh (ℰ𝓁 n) eβ‚‚'' (βˆ₯ t βˆ₯ cβ‚‚')))
coh (ℰ𝓁ℯ𝓂 n) {_ , T'} (e , f) t c c' e' =
  let
    c₁  = coeᢜ (symᢜ e) c'
    e₁' = cohᢜ (symᢜ e) c'
  in htrs (ℰ𝓁 n)
    (hcng T' _ _ (htrsᢜ e (symᢜ e) e' e₁'))
    (f c₁ c' (hsymᢜ (symᢜ e) e₁'))
    (hcng t _ _ (htrsᢜ e (symᢜ e) e' e₁'))
    (coh (ℰ𝓁 n) (f c₁ c' (hsymᢜ (symᢜ e) e₁')) (βˆ₯ t βˆ₯ c₁))

----------------------------------------------------------------------
-- Re-indexing
----------------------------------------------------------------------
module ReIndexFam where
  infixr 6 _*ᢜ_
  _*ᢜ_ :
    {n : β„•}
    {C D : ∣ π’ž ∣}
    (f : Hom D C)
    (T : Fam n C)
    β†’ -----------
    Fam n D

  βˆ₯ f *ᢜ T βˆ₯ d = βˆ₯ T βˆ₯ (∣ f ∣ d)
  hcng (f *ᢜ T) d d' e = hcng T (∣ f ∣ d) (∣ f ∣ d') (cng f d d' e)

  -- Notation
  instance
    Apply*ᢜ : βˆ€{n C D} β†’ Apply (Hom D C) (Fam n C) (Fam n D)
    _*_ ⦃ Apply*ᢜ ⦄ = _*ᢜ_

  infixr 6 _*₁_
  _*₁_ :
    {n : β„•}
    {C D : ∣ π’ž ∣}
    {T : Fam n C}
    (f : Hom D C)
    (t : Elem n C T)
    β†’ -------------
    Elem n D (f * T)

  βˆ₯ f *₁ t βˆ₯ d = βˆ₯ t βˆ₯ (∣ f ∣ d)
  hcng (f *₁ t) _ _ e = hcng t _ _ (cng f _ _ e)

  cng* :
    {n : β„•}
    {C C' D D' : ∣ π’ž ∣}
    {T : Fam n C}
    {T' : Fam n C'}
    (f : Hom D C)
    (f' : Hom D' C')
    (_ : ℋℴ𝓂 βˆ‹ (D , C) , f β‰ˆ (D' , C') , f')
    (_ : ℱ𝒢𝓂 n βˆ‹ C , T β‰ˆ C' , T')
    β†’ --------------------------------------
    ℱ𝒢𝓂 n βˆ‹ D , f * T β‰ˆ D' , f' * T'

  cng* f f' e e' c c' u = e' (∣ f ∣ c) (∣ f' ∣ c') (e c c' u)

  cng*₁ :
    {n : β„•}
    {C C' D D' : ∣ π’ž ∣}
    {T : Fam n C}
    {T' : Fam n C'}
    {t : Elem n C T}
    {t' : Elem n C' T'}
    (f : Hom D C)
    (f' : Hom D' C')
    (_ : ℋℴ𝓂 βˆ‹ (D , C) , f β‰ˆ (D' , C') , f')
    (_ : ℰ𝓁ℯ𝓂 n βˆ‹ (C , T) , t β‰ˆ (C' , T') , t')
    β†’ -------------------------------------------------------
    ℰ𝓁ℯ𝓂 n βˆ‹ (D , f * T) , f *₁ t  β‰ˆ (D' , f' * T') , f' *₁ t'

  cng*₁ f f' e e' c c' u = e' (∣ f ∣ c) (∣ f' ∣ c') (e c c' u)

open ReIndexFam public

----------------------------------------------------------------------
-- Codes for universes of types
----------------------------------------------------------------------
π“Šπ“ƒπ’Ύπ“‹ :
  (n : β„•)
  {C : ∣ π’ž ∣}
  β†’ ----------
  Fam (1+ n) C

βˆ₯ π“Šπ“ƒπ’Ύπ“‹ _ βˆ₯ _  = Univ
hcng (π“Šπ“ƒπ’Ύπ“‹ n) _ _ _ = rfl (𝒰 (1+ n)) Univ

-- Families are elements of universes up to definitional equality:
fam-as-elt :
  {n : β„•}
  {C : ∣ π’ž ∣}
  β†’ ------------------------------
  Fam n C ≑ Elem (1+ n) C (π“Šπ“ƒπ’Ύπ“‹ n)

fam-as-elt = refl

----------------------------------------------------------------------
-- Semantic context comprehension
----------------------------------------------------------------------
infixl 8 _⋉[_]_
_⋉[_]_ :
  (C : ∣ π’ž ∣)
  (n : β„•)
  (X : Fam n C)
  β†’ -----------
  ∣ π’ž ∣

C ⋉[ n ] (mk𝒰sect X q) = Sigma C n X q

𝓅 :
  {n : β„•}
  {C : ∣ π’ž ∣}
  (T : Fam n C)
  β†’ ----------------
  Hom (C ⋉[ n ] T) C

∣ 𝓅 _ ∣ (c , _) = c
cng (𝓅 _) _ _ (e , _) = e

𝓆 :
  {n : β„•}
  {C : ∣ π’ž ∣}
  (T : Fam n C)
  β†’ ---------------------------
  Elem n (C ⋉[ n ] T) (𝓅 T * T)

βˆ₯ 𝓆 _ βˆ₯ (c , t) = t
hcng (𝓆 _) _ _ (_ , e , e')
  with refl ← ! ⦃ !≑ ⦄ e refl = e'

π’Έβ„΄π“ƒπ“ˆ :
  {n : β„•}
  {C D : ∣ π’ž ∣}
  {T : Fam n C}
  (f : Hom D C)
  (t : Elem n D (f * T))
  β†’ -------------------
  Hom D (C ⋉[ n ] T)

∣ π’Έβ„΄π“ƒπ“ˆ f t ∣ d = (∣ f ∣ d , βˆ₯ t βˆ₯ d)
cng (π’Έβ„΄π“ƒπ“ˆ f t) _ _ e =
  (cng f _ _ e , refl , hcng t _ _ e)

infixl 8 βŸͺ_⟫
βŸͺ_⟫ :
  {n : β„•}
  {C : ∣ π’ž ∣}
  {T : Fam n C}
  (t : Elem n C T)
  β†’ ----------------
  Hom C (C ⋉[ n ] T)

βŸͺ t ⟫ = π’Έβ„΄π“ƒπ“ˆ id t

infixl 8 _⋉′[_]_
_⋉′[_]_ :
  {C D : ∣ π’ž ∣}
  (f : Hom D C)
  (n : β„•)
  (T : Fam n C)
  β†’ ---------------------------------
  Hom (D ⋉[ n ] (f * T)) (C ⋉[ n ] T)

f ⋉′[ n ] T = π’Έβ„΄π“ƒπ“ˆ (f ∘ 𝓅 (f * T)) (𝓆 (f * T))

cong⋉[] :
  {C C' : ∣ π’ž ∣}
  (n : β„•)
  {T : Fam n C}
  {T' : Fam n C'}
  (_ : π’ž βˆ‹ C ~ C')
  (_ : ℱ𝒢𝓂 n βˆ‹ C , T β‰ˆ C' , T')
  β†’ -----------------------------
  π’ž βˆ‹ C ⋉[ n ] T ~ C' ⋉[ n ] T'

cong⋉[] n e e' = (e , refl , Ξ» c c' u β†’ e' c c' u)

img⋉[] :
  {C : ∣ π’ž ∣}
  {n : β„•}
  {T : Fam n C}
  (C'' : ∣ π’ž ∣)
  (_ : π’ž βˆ‹ C ⋉[ n ] T ~ C'')
  β†’ ------------------------------
  βˆ‘[ C' ∈ ∣ π’ž ∣ ] βˆ‘[ T' ∈ Fam n C' ]
  (C ~ᢜ C')
  ∧
  (ℱ𝒢𝓂 n βˆ‹ C , T β‰ˆ C' , T')

img⋉[] (Sigma C n X q) (e , refl , e') = (C , mk𝒰sect X q , e , e')

imgUnit :
  (C : ∣ π’ž ∣)
  (_ : π’ž βˆ‹ Unit ~ C)
  β†’ -----------------
  Unit ≑ C

imgUnit Unit tt = refl

----------------------------------------------------------------------
-- Pi types
----------------------------------------------------------------------
𝒫𝒾 :
  {C : ∣ π’ž ∣}
  (m n : β„•)
  (S : Fam m C)
  (_ : Fam n (C ⋉[ m ] S))
  β†’ -----------------------
  Fam (max m n) C

βˆ₯ 𝒫𝒾 m n S T βˆ₯ c = PI.ty (pi m n)
  (βˆ₯ S βˆ₯ c)
  (Ξ» c' β†’ βˆ₯ T βˆ₯ (c , c'))
  (Ξ» _ _ e β†’ hcng T _ _ (hrflᢜ _ c , refl , e))
hcng (𝒫𝒾 m n S T) x x' e = PI.tyCong (pi m n) _ _ _ _ _ _
  (hcng S _ _ e)
  (Ξ» _ _ e' β†’ hcng T _ _ (e , refl , e'))

cong𝒫𝒾 :
  {C C' : ∣ π’ž ∣}
  (m n : β„•)
  {S : Fam m C}
  {S' : Fam m C'}
  {T : Fam n (C ⋉[ m ] S)}
  {T' : Fam n (C' ⋉[ m ] S')}
  (_ : ℱ𝒢𝓂 m βˆ‹ C , S β‰ˆ C' , S')
  (_ : ℱ𝒢𝓂 n βˆ‹ C ⋉[ m ] S , T β‰ˆ C' ⋉[ m ] S' , T')
  β†’ ------------------------------------------------
  ℱ𝒢𝓂 (max m n) βˆ‹ C , 𝒫𝒾 m n S T β‰ˆ C' , 𝒫𝒾 m n S' T'

cong𝒫𝒾 m n e e' c c' u = PI.tyCong (pi m n) _ _ _ _ _ _
  (e c c' u)
  (Ξ» y y' v β†’ e' (c , y) (c' , y') (u , refl , v))

-- The 𝒫𝒾 operation is natural up to setoid equivalence
ntrl𝒫𝒾 :
  {D C : ∣ π’ž ∣}
  (m n : β„•)
  (S : Fam m C)
  (T : Fam n (C ⋉[ m ] S))
  (f : Hom D C)
  β†’ ------------------------------------
  ℱ𝒢𝓂 (max m n) β€² D βˆ‹ f * (𝒫𝒾 m n S T) ~
    𝒫𝒾 m n (f * S) ((f ⋉′[ m ] S) * T)

ntrl𝒫𝒾 m n S T f _ _ e = PI.tyCong (pi m n) _ _ _ _ _ _
  (hcng S _ _ (cng f _ _ e))
  Ξ» y y' e' β†’
    hcng T _ _ (cng f _ _ e , refl , e')

𝓁𝒢𝓂 :
  {C : ∣ π’ž ∣}
  (m n : β„•)
  (S : Fam m C)
  {T : Fam n (C ⋉[ m ] S)}
  (t : Elem n (C ⋉[ m ] S) T)
  β†’ --------------------------
  Elem (max m n) C (𝒫𝒾 m n S T)

βˆ₯ 𝓁𝒢𝓂 m n _ t βˆ₯ c = PI.lam (pi m n) _ _ _
  (Ξ» c' β†’ βˆ₯ t βˆ₯ (c , c'))
  (Ξ» _ _ e β†’ hcng t _ _ (hrflᢜ _ c , refl , e))
hcng (𝓁𝒢𝓂 m n _ t) c c' e =
  PI.lamCong (pi m n) _ _ _ _ _ _ _ _ _ _
  Ξ» _ _ e' β†’ hcng t _ _ (e , refl , e')

cong𝓁𝒢𝓂 :
  {C C' : ∣ π’ž ∣}
  (m n : β„•)
  {S : Fam m C}
  {S' : Fam m C'}
  {T : Fam n (C ⋉[ m ] S)}
  {T' : Fam n (C' ⋉[ m ] S')}
  {t : Elem n (C ⋉[ m ] S) T}
  {t' : Elem n (C' ⋉[ m ] S') T'}
  (_ : ℰ𝓁ℯ𝓂 n βˆ‹ (C ⋉[ m ] S , T) , t β‰ˆ (C' ⋉[ m ] S' , T') , t')
  β†’ -----------------------------------------------------------
  ℰ𝓁ℯ𝓂 (max m n) βˆ‹
    (C , 𝒫𝒾 m n S T) , 𝓁𝒢𝓂 m n S t β‰ˆ
    (C' , 𝒫𝒾 m n S' T') , 𝓁𝒢𝓂 m n S' t'

cong𝓁𝒢𝓂 m n e c c' u =
  PI.lamCong (pi m n) _ _ _ _ _ _ _ _ _ _
  Ξ» y y' v β†’ e (c , y) (c' , y') (u , refl , v)

ntrl𝓁𝒢𝓂 :
  {D C : ∣ π’ž ∣}
  (m n : β„•)
  {S : Fam m C}
  {T : Fam n (C ⋉[ m ] S)}
  (t : Elem n (C ⋉[ m ] S) T)
  (f : Hom D C)
  β†’ --------------------------------------
  ℰ𝓁ℯ𝓂 (max m n) βˆ‹
  (D , f * (𝒫𝒾 m n S T)) ,
  f *₁ 𝓁𝒢𝓂 m n S t
  β‰ˆ
  (D , 𝒫𝒾 m n (f * S) (f ⋉′[ m ] S * T)) ,
  𝓁𝒢𝓂 m n (f * S) (f ⋉′[ m ] S *₁ t)

ntrl𝓁𝒢𝓂 m n t f c c' e =
  PI.lamCong (pi m n) _ _ _ _ _ _ _ _ _ _
  Ξ» y y' e' β†’ hcng t _ _ (cng f _ _ e , refl , e')

𝒢𝓅𝓅 :
  {C : ∣ π’ž ∣}
  (m n : β„•)
  (S : Fam m C)
  (T : Fam n (C ⋉[ m ] S))
  (_ : Elem (max m n) C (𝒫𝒾 m n S T))
  (s : Elem m C S)
  β†’ --------------------------------
  Elem n C (βŸͺ s ⟫ * T)

βˆ₯ 𝒢𝓅𝓅 m n _ _ t s βˆ₯ c =
  PI.app (pi m n) _ _ _ (βˆ₯ t βˆ₯ c) (βˆ₯ s βˆ₯ c)
hcng (𝒢𝓅𝓅 m n _ _ t s) x x' e =
  PI.appCong (pi m n) _ _ _ _ _ _ _ _ _ _
  (hcng t x x' e)
  (hcng s x x' e)

ntrl𝒢𝓅𝓅 :
  {D C : ∣ π’ž ∣}
  (m n : β„•)
  (S : Fam m C)
  (T : Fam n (C ⋉[ m ] S))
  (t : Elem (max m n) C (𝒫𝒾 m n S T))
  (s : Elem m C S)
  (f : Hom D C)
  β†’ ----------------------------------------
  ℰ𝓁ℯ𝓂 n βˆ‹
  (D , f * βŸͺ s ⟫ * T) , f *₁ 𝒢𝓅𝓅 m n S T t s
  β‰ˆ
  (D , βŸͺ f *₁ s ⟫ * (f ⋉′[ m ] S) * T) ,
  𝒢𝓅𝓅 m n (f * S) (f ⋉′[ m ] S * T)
    (coe (ℰ𝓁ℯ𝓂 (max m n))
      (rflᢜ D , ntrl𝒫𝒾 m n S T f) (f *₁ t))
    (f *₁ s)

ntrl𝒢𝓅𝓅 m n S T t s f c c' e =
  PI.appCong (pi m n) _ _ _ _ _ _ _ _ _ _
  (coh (ℰ𝓁ℯ𝓂 (max m n))
    {x' = _ , 𝒫𝒾 m n (f * S) (f ⋉′[ m ] S * T)}
    (rflᢜ _ , ntrl𝒫𝒾 m n S T f)
    (f *₁ t) c c' e)
  (hcng s (∣ f ∣ c) (∣ f ∣ c') (cng f c c' e))

𝒫𝒾𝒷ℯ𝓉𝒢 :
  {C : ∣ π’ž ∣}
  (m n : β„•)
  (S : Fam m C)
  (T : Fam n (C ⋉[ m ] S))
  (t : Elem n (C ⋉[ m ] S) T)
  (s :  Elem m C S)
  β†’ --------------------------------------
  ℰ𝓁ℯ𝓂 n β€² (C , βŸͺ s ⟫ * T) βˆ‹
  𝒢𝓅𝓅 m n S T (𝓁𝒢𝓂 m n S t) s ~ βŸͺ s ⟫ *₁ t

𝒫𝒾𝒷ℯ𝓉𝒢{C} m n S T t s c _ e =  htrs (ℰ𝓁 n)
  (rfl (𝒰 n) (βˆ₯ βŸͺ s ⟫ * T βˆ₯ c))
  (hcng T _ _ (cng βŸͺ s ⟫ _ _ e))
  (PI.beta (pi m n)
    (βˆ₯ S βˆ₯ c)
    (Ξ» x β†’ βˆ₯ T βˆ₯ (c , x))
    (Ξ» _ _ e' β†’ hcng T _ _ (hrflᢜ C c , refl , e'))
    (Ξ» x β†’ βˆ₯ t βˆ₯ (c , x))
    (Ξ» _ _ e' β†’ hcng t _ _ (hrflᢜ C c , refl , e'))
    (βˆ₯ s βˆ₯ c))
  (hcng t _ _ (cng βŸͺ s ⟫ _ _ e))

module 𝒫𝒾ℰ𝓉𝒢
-- The fact that ntrl𝒫𝒾 is not a definitional equality complicates the
-- proof that the semantics is sound for eta conversion.
  (C : ∣ π’ž ∣)
  (m n : β„•)
  (S : Fam m C)
  (T : Fam n (C ⋉[ m ] S))
  (t : Elem (max m n) C (𝒫𝒾 m n S T))
  where
  S' : Fam m (C ⋉[ m ] S)
  S' = 𝓅 S * S

  T' : Fam n (C ⋉[ m ] S ⋉[ m ] S')
  T' = (𝓅 S ⋉′[ m ] S) * T

  e : ℱ𝒢𝓂 n β€² (C ⋉[ m ] S) βˆ‹ βŸͺ 𝓆 S ⟫ * T' ~ T
  e = hcng T

  t' : Elem (max m n) (C ⋉[ m ] S) (𝒫𝒾 m n S' T')
  t' = coe (ℰ𝓁ℯ𝓂 (max m n))
    ((rflᢜ (C ⋉[ m ] S) , ntrl𝒫𝒾 m n S T (𝓅 S)))
    (𝓅 S *₁ t)

  e' : ℰ𝓁ℯ𝓂 (max m n) βˆ‹
    (C ⋉[ m ] S , 𝒫𝒾 m n S' T') , t' β‰ˆ
    (C ⋉[ m ] S , 𝓅 S *  𝒫𝒾 m n S T) , 𝓅 S *₁ t
  e' = coh⁻¹ (ℰ𝓁ℯ𝓂 (max m n))
    {C ⋉[ m ] S , 𝓅 S *  𝒫𝒾 m n S T}
    {C ⋉[ m ] S , 𝒫𝒾 m n S' T'}
    ((rflᢜ (C ⋉[ m ] S) , ntrl𝒫𝒾 m n S T (𝓅 S)))
    (𝓅 S *₁ t)

  abstract
    etaPf : ℰ𝓁ℯ𝓂 (max m n) βˆ‹
      (C , 𝒫𝒾 m n S (βŸͺ 𝓆 S ⟫ * T')) , 𝓁𝒢𝓂 m n S (𝒢𝓅𝓅 m n S' T' t' (𝓆 S))
      β‰ˆ (C , 𝒫𝒾 m n S T) , t
    etaPf c c' e = htrs (ℰ𝓁 (max m n))
      (PI.tyCong (pi m n) _ _ _ _ _ _ (rfl (𝒰 m) (βˆ₯ S βˆ₯ c))
        (Ξ» x x' u β†’ hcng T (c , x) (c , x')
          (hrflᢜ C c , refl , u)))
      (hcng (𝒫𝒾 m n S T) c c' e)
      q
      (hcng t c c' e)
      where
      q : ℰ𝓁 (max m n) βˆ‹
        (PI.ty (pi m n)
          (βˆ₯ S βˆ₯ c)
          (Ξ» x β†’ βˆ₯ T βˆ₯ (c , x))
          (Ξ» x x' u β†’
          hcng (βŸͺ 𝓆 S ⟫ * T') (c , x) (c , x')
          (hrflᢜ C c , refl , u)
          ))
        ,
        PI.lam (pi m n) _ _ _
        (Ξ» c' β†’ PI.app (pi m n) _ _ _ (βˆ₯ t' βˆ₯ (c , c')) c')
        (Ξ» x x' u β†’ PI.appCong (pi m n) _ _ _ _ _ _ _ _ _ _
          (hcng t' (c , x) (c , x') (hrflᢜ _ c , refl , u))
          (hcng (𝓆 S) (c , x) (c , x') (hrflᢜ _ c , refl , u)))
        β‰ˆ
        (PI.ty (pi m n) (βˆ₯ S βˆ₯ c) (Ξ» x β†’ βˆ₯ T βˆ₯ (c , x))
        (Ξ» x x' u β†’ hcng T (c , x) (c , x')
          (hrflᢜ C c , refl , u)))
        ,
        βˆ₯ t βˆ₯ c
      q = htrs (ℰ𝓁 (max m n))
        (PI.tyCong (pi m n) _ _ _ _ _ _ (rfl (𝒰 m) (βˆ₯ S βˆ₯ c))
          (Ξ» x x' u β†’ hcng T (c , x) (c , x')
            (hrflᢜ _ c , refl , u)))
        (rfl (𝒰 (max m n)) (βˆ₯ 𝒫𝒾 m n S T βˆ₯ c))
        (PI.lamCong (pi m n) _ _ _ _ _ _ _ _ _ _
          Ξ» x x' u β†’ PI.appCong (pi m n) _ _ _ _ _ _ _ _ _ _
            (e' (c , x) (c , x)
          (hrflᢜ C c , refl , hrfl (ℰ𝓁 m) (βˆ₯ S βˆ₯ c) x)) u)
        (PI.eta (pi m n) _ _ _ (βˆ₯ t βˆ₯ c))

----------------------------------------------------------------------
-- Equality types
----------------------------------------------------------------------
module EqualityType where
  ℰ𝓆 :
    {C : ∣ π’ž ∣}
    (n : β„•)
    (T : Fam n C)
    (t t' : Elem n C T)
    β†’ ----------------
    Fam n C

  βˆ₯ ℰ𝓆 n T t t' βˆ₯ c =
    EQ.ty (eq n) (βˆ₯ T βˆ₯ c) (βˆ₯ t βˆ₯ c) (βˆ₯ t' βˆ₯ c)
  hcng (ℰ𝓆 n T t t') _ _ e = EQ.tyCong (eq n)
    (hcng T _ _ e)
    (hcng t _ _ e)
    (hcng t' _ _ e)

  ntrlℰ𝓆 :
    {D C : ∣ π’ž ∣}
    (n : β„•)
    (T : Fam n C)
    (t t' : Elem n C T)
    (f : Hom D C)
    β†’ -------------------------------------------------------------
    ℱ𝒢𝓂 n β€² D βˆ‹ f * (ℰ𝓆 n T t t') ~ ℰ𝓆 n (f * T) (f *₁ t) (f *₁ t')

  ntrlℰ𝓆 n T t t' f _ _ e = EQ.tyCong (eq n)
    (hcng T _ _ (cng f _ _ e))
    (hcng t _ _ (cng f _ _ e))
    (hcng t' _ _ (cng f _ _ e))

  𝓇𝒻𝓁 :
    {C : ∣ π’ž ∣}
    (n : β„•)
    (T : Fam n C)
    (t : Elem n C T)
    β†’ ------------------
    Elem n C (ℰ𝓆 n T t t)

  βˆ₯ 𝓇𝒻𝓁 n _ t βˆ₯ c = EQ.rfl (eq n) (βˆ₯ t βˆ₯ c)
  hcng (𝓇𝒻𝓁 n T t) _ _ e =
    EQ.rflCong (eq n) (hcng T _ _ e) (hcng t _ _ e)

  ntrl𝓇𝒻𝓁 :
    {D C : ∣ π’ž ∣}
    (n : β„•)
    (T : Fam n C)
    (t : Elem n C T)
    (f : Hom D C)
    β†’ -----------------------------------------------------------
    ℰ𝓁ℯ𝓂 n βˆ‹
    (D , f * (ℰ𝓆 n T t t)) , f *₁ (𝓇𝒻𝓁 n T t)
    β‰ˆ
    (D , ℰ𝓆 n (f * T) (f *₁ t) (f *₁ t)) , 𝓇𝒻𝓁 n (f * T) (f *₁ t)

  ntrl𝓇𝒻𝓁 n T t f c c' e = EQ.rflCong (eq n)
    (hcng T (∣ f ∣ c) (∣ f ∣ c') (cng f c c' e))
    (hcng t (∣ f ∣ c) (∣ f ∣ c') (cng f c c' e))

  𝓇ℯ𝒻𝓁ℯ𝒸𝓉 :
    {C : ∣ π’ž ∣}
    (n : β„•)
    (T : Fam n C)
    (t t' : Elem n C T)
    (_ : Elem n C (ℰ𝓆 n T t t'))
    β†’ -------------------------
    ℰ𝓁ℯ𝓂 n β€² (C , T) βˆ‹ t ~ t'

  𝓇ℯ𝒻𝓁ℯ𝒸𝓉 n T t t' e c c' u = htrs (ℰ𝓁 n)
    (rfl (𝒰 n) (βˆ₯ T βˆ₯ c))
    (hcng T c c' u)
    (EQ.reflect (eq n) (βˆ₯ e βˆ₯ c))
    (hcng t' c c' u)

  π“Šπ’Ύπ“… :
    {C : ∣ π’ž ∣}
    (n : β„•)
    (T : Fam n C)
    (t t' : Elem n C T)
    (e e' : Elem n C (ℰ𝓆 n T t t'))
    β†’ --------------------------------
    ℰ𝓁ℯ𝓂 n β€² (C , ℰ𝓆 n T t t') βˆ‹ e ~ e'

  π“Šπ’Ύπ“…{C} n T t t' e e' c c' u = htrs (ℰ𝓁 n)
         (rfl (𝒰 n) (βˆ₯ ℰ𝓆 n T t t' βˆ₯ c))
         (hcng (ℰ𝓆 n T t t') c c' u)
         (EQ.uip (eq n) (βˆ₯ e βˆ₯ c) (βˆ₯ e' βˆ₯ c))
         (hcng e' c c' u)

open EqualityType public
----------------------------------------------------------------------
-- Empty type
----------------------------------------------------------------------
module EmptyType where
  ℰ𝓂𝓅 :
    {C : ∣ π’ž ∣}
    β†’ -------
    Fam 0 C

  βˆ₯ ℰ𝓂𝓅 βˆ₯ _ = Emp
  hcng ℰ𝓂𝓅 _ _ _ = tt

  ℯ𝓂𝓅 :
    {C : ∣ π’ž ∣}
    (n : β„•)
    (T : Fam n C)
    (t : Elem 0 C ℰ𝓂𝓅)
    β†’ ---------------
    Elem n C T

  βˆ₯ ℯ𝓂𝓅 _ _ t βˆ₯ c = Øelim (βˆ₯ t βˆ₯ c)
  hcng (ℯ𝓂𝓅 _ _ t) c _ _ = Øelim (βˆ₯ t βˆ₯ c)

open EmptyType public

----------------------------------------------------------------------
-- Natural number type
----------------------------------------------------------------------
module NaturalNumberType where
  𝒩𝒢𝓉 :
    {C : ∣ π’ž ∣}
    β†’ -------
    Fam 0 C

  βˆ₯ 𝒩𝒢𝓉 βˆ₯ _ = Nat
  hcng 𝒩𝒢𝓉 _ _ _ = tt

  𝓏ℯ𝓇ℴ :
    {C : ∣ π’ž ∣}
    β†’ ---------
    Elem 0 C 𝒩𝒢𝓉

  βˆ₯ 𝓏ℯ𝓇ℴ βˆ₯ _ = 0
  hcng 𝓏ℯ𝓇ℴ _ _ _ = refl

  π“ˆπ“Šπ’Έπ’Έ :
    {C : ∣ π’ž ∣}
    (t : Elem 0 C 𝒩𝒢𝓉)
    β†’ ---------------
    Elem 0 C 𝒩𝒢𝓉

  βˆ₯ π“ˆπ“Šπ’Έπ’Έ t βˆ₯ c = 1+ (βˆ₯ t βˆ₯ c)
  hcng (π“ˆπ“Šπ’Έπ’Έ t) _ _ e = cong 1+ (hcng t _ _ e)

  ntrlπ“ˆπ“Šπ’Έπ’Έ :
    {D C : ∣ π’ž ∣}
    (t : Elem 0 C 𝒩𝒢𝓉)
    (f : Hom D C)
    β†’ --------------------------------
    ℰ𝓁ℯ𝓂 0 βˆ‹ (D ,  𝒩𝒢𝓉) , f *₁ π“ˆπ“Šπ’Έπ’Έ t β‰ˆ
    (D ,  𝒩𝒢𝓉) , π“ˆπ“Šπ’Έπ’Έ (f *₁ t)

  ntrlπ“ˆπ“Šπ’Έπ’Έ t f c c' e =
    cong 1+ (hcng t (∣ f ∣ c) (∣ f ∣ c') (cng f c c' e))

  𝓃𝓇ℯ𝒸 :
    {C : ∣ π’ž ∣}
    (n : β„•)
    (S : Fam n (C ⋉[ 0 ] 𝒩𝒢𝓉))
    (sβ‚€ : Elem n C (βŸͺ 𝓏ℯ𝓇ℴ ⟫ * S))
    (sβ‚Š : Elem n (C ⋉[ 0 ] 𝒩𝒢𝓉 ⋉[ n ] S)
      (𝓅 S * π’Έβ„΄π“ƒπ“ˆ (𝓅 𝒩𝒢𝓉) (π“ˆπ“Šπ’Έπ’Έ (𝓆 𝒩𝒢𝓉)) * S))
    (s : Elem 0 C 𝒩𝒢𝓉)
    β†’ ----------------------------------------
    Elem n C (βŸͺ s ⟫ * S)

  βˆ₯ 𝓃𝓇ℯ𝒸 n S sβ‚€ sβ‚Š s βˆ₯ c = nrec n
    (Ξ» m β†’ βˆ₯ S βˆ₯ (c , m))
    (βˆ₯ sβ‚€ βˆ₯ c)
    (Ξ» m y β†’ βˆ₯ sβ‚Š βˆ₯ ((c , m) , y))
    (Ξ» n _ _ e β†’ hcng sβ‚Š _ _
      ((hrflᢜ _ c , refl , refl) , refl , e))
    (βˆ₯ s βˆ₯ c)
  hcng (𝓃𝓇ℯ𝒸 n S sβ‚€ sβ‚Š s) c c' e = nrecCong{n}
    {Ξ» m β†’ βˆ₯ S βˆ₯ (c , m)}
    {Ξ» m β†’ βˆ₯ S βˆ₯ (c' , m)}
    {βˆ₯ sβ‚€ βˆ₯ c}
    {βˆ₯ sβ‚€ βˆ₯ c'}
    {Ξ» m y β†’ βˆ₯ sβ‚Š βˆ₯ ((c , m) , y)}
    {Ξ» m y β†’ βˆ₯ sβ‚Š βˆ₯ ((c' , m) , y)}
    {Ξ» n _ _ e β†’ hcng sβ‚Š _ _
      ((hrflᢜ _ c , refl , refl) , refl , e)}
    {Ξ» n _ _ e β†’ hcng sβ‚Š _ _
      ((hrflᢜ _ c' , refl , refl) , refl , e)}
    (βˆ₯ s βˆ₯ c)
    (βˆ₯ s βˆ₯ c')
    (Ξ» _ β†’ hcng S _ _ (e , refl , refl))
    (hcng sβ‚€ _ _ e)
    (Ξ» _ _ _ e' β†’ hcng sβ‚Š _ _
      ((e , refl , refl) , refl , e'))
    (hcng s _ _ e)

  ntrl𝓃𝓇ℯ𝒸 :
    {D C : ∣ π’ž ∣}
    (n : β„•)
    (S : Fam n (C ⋉[ 0 ] 𝒩𝒢𝓉))
    (sβ‚€ : Elem n C (βŸͺ 𝓏ℯ𝓇ℴ ⟫ * S))
    (sβ‚Š : Elem n (C ⋉[ 0 ] 𝒩𝒢𝓉 ⋉[ n ] S)
      (𝓅 S * (π’Έβ„΄π“ƒπ“ˆ (𝓅 𝒩𝒢𝓉) (π“ˆπ“Šπ’Έπ’Έ (𝓆 𝒩𝒢𝓉))) * S))
    (s : Elem 0 C 𝒩𝒢𝓉)
    (f : Hom D C)
    β†’ -------------------------------------------
    ℰ𝓁ℯ𝓂 n βˆ‹
    (D , f * βŸͺ s ⟫ * S) , f *₁ (𝓃𝓇ℯ𝒸 n S sβ‚€ sβ‚Š s)
    β‰ˆ
    (D , βŸͺ f *₁ s ⟫ * (f ⋉′[ 0 ] 𝒩𝒢𝓉) * S) ,
    𝓃𝓇ℯ𝒸 n
      (f ⋉′[ 0 ] 𝒩𝒢𝓉 * S)
      (f *₁ sβ‚€)
      (f ⋉′[ 0 ] 𝒩𝒢𝓉 ⋉′[ n ] S *₁ sβ‚Š)
      (f *₁ s)

  ntrl𝓃𝓇ℯ𝒸 n S sβ‚€ sβ‚Š s f c c' e = nrecCong{n}
    {Ξ» m β†’ βˆ₯ S βˆ₯ (∣ f ∣ c , m)}
    {Ξ» m β†’ βˆ₯ S βˆ₯ (∣ f ∣ c' , m)}
    {βˆ₯ sβ‚€ βˆ₯ (∣ f ∣ c)}
    {βˆ₯ sβ‚€ βˆ₯ (∣ f ∣ c')}
    {Ξ» m x' β†’ βˆ₯ sβ‚Š βˆ₯ ((∣ f ∣ c , m) , x')}
    {Ξ» m x' β†’ βˆ₯ sβ‚Š βˆ₯ ((∣ f ∣ c' , m) , x')}
    {Ξ» _ _ _ e' β†’ hcng sβ‚Š _ _
      ((hrflᢜ _ (∣ f ∣ c) , refl , refl) , refl , e')}
    {Ξ» _ _ _ e' β†’ hcng sβ‚Š _ _
      ((hrflᢜ _ (∣ f ∣ c') , refl , refl) , refl , e')}
    (βˆ₯ s βˆ₯ (∣ f ∣ c))
    (βˆ₯ s βˆ₯ (∣ f ∣ c'))
    (Ξ» _ β†’ hcng S _ _ (cng f c c' e , refl , refl))
    (hcng sβ‚€ (∣ f ∣ c) (∣ f ∣ c') (cng f c c' e))
    (Ξ» _ _ _ e' β†’ hcng sβ‚Š _ _
      ((cng f c c' e , refl , refl) , refl , e'))
    (hcng s (∣ f ∣ c) (∣ f ∣ c') (cng f c c' e))

open NaturalNumberType public