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
  constructor mkHom
  infix 8 ∣_∣
  field
    ∣_∣ : βˆ₯ β„° βˆ₯ C β†’ βˆ₯ β„° βˆ₯ D
    cng :
      (c c' : βˆ₯ β„° βˆ₯ C)
      (_ : C , c β‰ˆαΆœ C , c')
      β†’ ---------------------
      D , ∣_∣ c β‰ˆαΆœ D , ∣_∣ 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
----------------------------------------------------------------------

{- Since we wish to ensure that, up to definitional equality, families
are sections of universes, we begin with the definition of sections
and then define families in terms of them. The use of a record type
rather than a Ξ£-type helps with inferring universe levels. -}

record Sect
  (n : β„•)
  (C : ∣ π’ž ∣)
  (X : βˆ₯ β„° βˆ₯ C β†’ U n)
  -- The next argument is not used, but including it enables the
  -- element re-indexing function *ᢜ to only depend implicitly upon
  -- its family argument
  (q : βˆ€ c c' β†’ C , c β‰ˆαΆœ C , c' β†’ 𝒰 n βˆ‹ X c ~ X c')
  : -----------------------------------------------
  Set
  where
  constructor mkSect
  infix 8 βˆ₯_βˆ₯
  field
    βˆ₯_βˆ₯ : (c : Elᢜ C) β†’ El n (X c)
    hcng :
      (c c' : Elᢜ C)
      (_ : C , c β‰ˆαΆœ C , c')
      β†’ --------------------------------
      ℰ𝓁 n βˆ‹ X c , βˆ₯_βˆ₯ c β‰ˆ X c' , βˆ₯_βˆ₯ c'

open Sect public

-- Families
Fam : β„• β†’ ∣ π’ž ∣ β†’ Set
Fam n C =
  -- we rely on the fact that El (1+ n) Univ ≑ U 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
----------------------------------------------------------------------
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)

----------------------------------------------------------------------
-- 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 ] (mkSect 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 , mkSect 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
----------------------------------------------------------------------
ℰ𝓆 :
  {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)

----------------------------------------------------------------------
-- Empty type
----------------------------------------------------------------------
ℰ𝓂𝓅 :
 {C : ∣ π’ž ∣}
 β†’ -------
 Fam 0 C

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

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

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

-- ntrlℯ𝓂𝓅 :
--   {D C : ∣ π’ž ∣}
--   (n : β„•)
--   (S : Fam n C)
--   (e : Elem 0 C ℰ𝓂𝓅)
--   (f : Hom D C)
--   β†’ --------------------------------------
--   ℰ𝓁ℯ𝓂 n βˆ‹ (D , f * S) , f *₁ (ℯ𝓂𝓅 n S e) β‰ˆ
--   (D , f * S) , ℯ𝓂𝓅 n (f * S) (f *₁ e)

-- ntrlℯ𝓂𝓅 _ _ e f c _ _ = Øelim (βˆ₯ e βˆ₯ (∣ f ∣ c))

----------------------------------------------------------------------
-- Natural number type
----------------------------------------------------------------------
𝒩𝒢𝓉 :
 {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))

----------------------------------------------------------------------
-- Displayed morphisms , families and elements
----------------------------------------------------------------------
-- β„±π“Šπ“ƒ : Setd

-- β„±π“Šπ“ƒ = (π’ž βŠ— π’ž) ⋉ ℋℴ𝓂

-- Σℱ𝒢𝓂 : β„• β†’ Setd

-- Σℱ𝒢𝓂 l = π’ž ⋉ ℱ𝒢𝓂 l

-- Σℱ𝒢𝓂ℰ𝓁ℯ𝓂 : β„• β†’ Setd[ π’ž ]

-- Σℱ𝒢𝓂ℰ𝓁ℯ𝓂 l = Ξ£ (ℱ𝒢𝓂 l) (ℰ𝓁ℯ𝓂 l)

-- Σℰ𝓁ℯ𝓂 : β„• β†’ Setd

-- Σℰ𝓁ℯ𝓂 l = π’ž ⋉ Σℱ𝒢𝓂ℰ𝓁ℯ𝓂 l