Chuangjie Xu 2014 (ported to TypeTopology in 2026)

This file defines a category-with-families structure on C-spaces. A
type over a context is given by a family together with a notion of
admissible dependent probes satisfying the expected closure axioms. A
term is a section whose composites with probes are admissible. From
these data we define substitution, context comprehension, and verify
the basic CwF equalities needed in the concrete model.

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt using (Fun-Ext; dfunext)

module C-Spaces.UsingFunExt.CwF (fe : Fun-Ext) where

open import UF.Base
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

open import C-Spaces.CwFs.Base
open import C-Spaces.Preliminaries.Sequence
open import C-Spaces.Coverage
open import C-Spaces.UsingFunExt.Space
open import C-Spaces.UsingFunExt.CartesianClosedness (dfunext fe)

\end{code}

Contexts are C-spaces, and substitutions are continuous maps.

\begin{code}

Con : 𝓀₁ Μ‡
Con = Space

Sub : Con β†’ Con β†’ 𝓀₀ Μ‡
Sub = Map

\end{code}

A dependent version of the probe axioms.

For a family `A` over a space `Ξ“`, the predicate `Q` specifies which
dependent probes are admissible. The four clauses say that admissible
dependent probes are closed under constants, precomposition by
uniformly continuous maps, gluing from finite approximations, and
change of witness for the underlying probe.

The last clause would be unnecessary if the probe predicate itself were
proposition-valued.

\begin{code}

dependent-probe-axioms : (Ξ“ : Space) (A : U Ξ“ β†’ 𝓀₀ Μ‡ )
                       β†’ ((p : β‚‚β„• β†’ U Ξ“) β†’ p ∈ Probe Ξ“ β†’ ((Ξ± : β‚‚β„•) β†’ A (p Ξ±)) β†’ 𝓀₀ Μ‡ )
                       β†’ 𝓀₀ Μ‡
dependent-probe-axioms (Ξ“ , P , cβ‚€ , c₁ , cβ‚‚) A Q
 =  ((Ξ³ : Ξ“) (a : A Ξ³) β†’ (Ξ» Ξ± β†’ a) ∈ Q (Ξ» Ξ± β†’ Ξ³) (cβ‚€ Ξ³))
  Γ— ((t : β‚‚β„• β†’ β‚‚β„•) (tC : t ∈ C) (p : β‚‚β„• β†’ Ξ“) (pP : p ∈ P) β†’
     (q : (Ξ± : β‚‚β„•) β†’ A (p Ξ±)) β†’ q ∈ Q p pP β†’ q ∘ t ∈ Q (p ∘ t) (c₁ t tC p pP))
  Γ— ((p : β‚‚β„• β†’ Ξ“)
     (q : (Ξ± : β‚‚β„•) β†’ A (p Ξ±))
     (d : Ξ£ \(n : β„•) β†’ (s : β‚‚Fin n) β†’ Ξ£ \(psP : p ∘ cons s ∈ P) β†’ q ∘ cons s ∈ Q (p ∘ cons s) psP) β†’
     q ∈ Q p (cβ‚‚ p (pr₁ d , Ξ» s β†’ pr₁ (prβ‚‚ d s))))
  Γ— ((p : β‚‚β„• β†’ Ξ“) (pP pP' : p ∈ P) (q : (Ξ± : β‚‚β„•) β†’ A (p Ξ±)) β†’ Q p pP q β†’ Q p pP' q)

dependent-probe-axioms-is-prop
 : (Ξ“ : Space) (A : U Ξ“ β†’ 𝓀₀ Μ‡ )
 β†’ (Q : (p : β‚‚β„• β†’ U Ξ“) β†’ p ∈ Probe Ξ“ β†’ ((Ξ± : β‚‚β„•) β†’ A (p Ξ±)) β†’ 𝓀₀ Μ‡ )
 β†’ (βˆ€ p pΞ“ q β†’ is-prop (q ∈ Q p pΞ“))
 β†’ is-prop (dependent-probe-axioms Ξ“ A Q)
dependent-probe-axioms-is-prop (Ξ“ , P , cβ‚€ , c₁ , cβ‚‚) A Q pQ
 = Γ—-is-prop cβ‚€-prop (Γ—-is-prop c₁-prop (Γ—-is-prop cβ‚‚-prop c₃-prop))
 where
  cβ‚€-prop
   : is-prop ((Ξ³ : Ξ“) (a : A Ξ³) β†’ (Ξ» Ξ± β†’ a) ∈ Q (Ξ» Ξ± β†’ Ξ³) (cβ‚€ Ξ³))
  cβ‚€-prop
   = Ξ β‚‚-is-prop fe (Ξ» Ξ³ a β†’ pQ (Ξ» Ξ± β†’ Ξ³) (cβ‚€ Ξ³) (Ξ» Ξ± β†’ a))
  c₁-prop
   : is-prop ((t : β‚‚β„• β†’ β‚‚β„•) (tC : t ∈ C) (p : β‚‚β„• β†’ Ξ“) (pP : p ∈ P) β†’
              (q : (Ξ± : β‚‚β„•) β†’ A (p Ξ±)) β†’ q ∈ Q p pP β†’ q ∘ t ∈ Q (p ∘ t) (c₁ t tC p pP))
  c₁-prop
   = Π₆-is-prop fe (Ξ» t tC p pP q qQ β†’ pQ (p ∘ t) (c₁ t tC p pP) (q ∘ t))
  cβ‚‚-prop
   : is-prop ((p : β‚‚β„• β†’ Ξ“)
              (q : (Ξ± : β‚‚β„•) β†’ A (p Ξ±))
              (d : Ξ£ \(n : β„•) β†’ (s : β‚‚Fin n) β†’ Ξ£ \(psP : p ∘ cons s ∈ P) β†’ q ∘ cons s ∈ Q (p ∘ cons s) psP) β†’
              q ∈ Q p (cβ‚‚ p (pr₁ d , Ξ» s β†’ pr₁ (prβ‚‚ d s))))
  cβ‚‚-prop
   = Π₃-is-prop fe (Ξ» p q d β†’ pQ p (cβ‚‚ p (pr₁ d , Ξ» s β†’ pr₁ (prβ‚‚ d s))) q)
  c₃-prop
   : is-prop ((p : β‚‚β„• β†’ Ξ“) (pP pP' : p ∈ P) (q : (Ξ± : β‚‚β„•) β†’ A (p Ξ±)) β†’ Q p pP q β†’ Q p pP' q)
  c₃-prop
   = Ξ β‚…-is-prop fe (Ξ» p pP pP' q qQ β†’ pQ p pP' q)

\end{code}

Types over a context are families equipped with proposition-valued
dependent probes satisfying the axioms above. Terms are sections whose
composites with probes are admissible.

\begin{code}

Ty : Con β†’ 𝓀₁ Μ‡
Ty Ξ“ = Ξ£ \(A : U Ξ“ β†’ 𝓀₀ Μ‡ ) β†’
         Ξ£ \(Q : (p : β‚‚β„• β†’ U Ξ“) β†’ p ∈ Probe Ξ“ β†’ ((Ξ± : β‚‚β„•) β†’ A (p Ξ±)) β†’ 𝓀₀ Μ‡ )
           β†’ (βˆ€ p pΞ“ q β†’ is-prop (q ∈ Q p pΞ“)) Γ—
             dependent-probe-axioms Ξ“ A Q

tyProbe : (Ξ“ : Con) (A : Ty Ξ“)
        β†’ (p : β‚‚β„• β†’ U Ξ“) β†’ p ∈ Probe Ξ“ β†’ ((Ξ± : β‚‚β„•) β†’ U A (p Ξ±)) β†’ 𝓀₀ Μ‡
tyProbe _ (_ , Q , _) = Q

tyProbe-is-prop : (Ξ“ : Con) (A : Ty Ξ“)
                β†’ βˆ€ p pΞ“ q β†’ is-prop (q ∈ tyProbe Ξ“ A p pΞ“)
tyProbe-is-prop _ (_ , _ , pQ , _) = pQ

Tm : (Ξ“ : Con) β†’ Ty Ξ“ β†’ 𝓀₀ Μ‡
Tm (Ξ“ , P , _) (A , Q , _)
 = Ξ£ \(u : (Ξ³ : Ξ“) β†’ A Ξ³) β†’ (p : β‚‚β„• β†’ Ξ“) (pP : p ∈ P) β†’ u ∘ p ∈ Q p pP

\end{code}

Substitution is defined by reindexing both the underlying family and
its dependent probe predicate along a substitution.

\begin{code}

βŸͺ_,_⟫_[_]ΚΈ : (Ξ“ Ξ” : Con) β†’ Ty Ξ“ β†’ Sub Ξ” Ξ“ β†’ Ty Ξ”
βŸͺ Ξ“ , Ξ” ⟫ (A , Q , pQ , tcβ‚€ , tc₁ , tcβ‚‚ , tc₃) [ Οƒ , cΟƒ ]ΚΈ
 = AΟƒ , Q' , pQ' , cβ‚€ , c₁ , cβ‚‚ , c₃
 where
  AΟƒ : U Ξ” β†’ 𝓀₀ Μ‡
  Aσ δ = A (σ δ)
  Q' : (p : β‚‚β„• β†’ U Ξ”) β†’ p ∈ Probe Ξ” β†’ ((Ξ± : β‚‚β„•) β†’ AΟƒ (p Ξ±)) β†’ 𝓀₀ Μ‡
  Q' p pΞ” q = q ∈ Q (Οƒ ∘ p) (cΟƒ p pΞ”)
  pQ' : βˆ€ p pΞ” q β†’ is-prop (q ∈ Q' p pΞ”)
  pQ' p pΞ” q = pQ (Οƒ ∘ p) (cΟƒ p pΞ”) q
  cβ‚€ : (Ξ΄ : U Ξ”) (a : AΟƒ Ξ΄) β†’ (Ξ» Ξ± β†’ a) ∈ Q' (Ξ» Ξ± β†’ Ξ΄) (condβ‚€ Ξ” Ξ΄)
  cβ‚€ Ξ΄ a = goal
   where
    fact : (Ξ» Ξ± β†’ a) ∈ Q (Ξ» Ξ± β†’ Οƒ Ξ΄) (condβ‚€ Ξ“ (Οƒ Ξ΄))
    fact = tcβ‚€ (Οƒ Ξ΄) a
    goal : (Ξ» Ξ± β†’ a) ∈ Q (Ξ» Ξ± β†’ Οƒ Ξ΄) (cΟƒ (Ξ» Ξ± β†’ Ξ΄) (condβ‚€ Ξ” Ξ΄))
    goal = tc₃ (Ξ» Ξ± β†’ Οƒ Ξ΄) _ _ (Ξ» Ξ± β†’ a) fact
  c₁ : (t : β‚‚β„• β†’ β‚‚β„•) (tC : t ∈ C) (p : β‚‚β„• β†’ U Ξ”) (pΞ” : p ∈ Probe Ξ”) β†’
       (q : (Ξ± : β‚‚β„•) β†’ AΟƒ (p Ξ±)) β†’ q ∈ Q' p pΞ” β†’ q ∘ t ∈ Q' (p ∘ t) (cond₁ Ξ” t tC p pΞ”)
  c₁ t tC p pΞ” q qQ' = goal
   where
    fact : q ∘ t ∈ Q (Οƒ ∘ p ∘ t) (cond₁ Ξ“ t tC (Οƒ ∘ p) (cΟƒ p pΞ”))
    fact = tc₁ t tC (Οƒ ∘ p) (cΟƒ p pΞ”) q qQ'
    goal : q ∘ t ∈ Q (Οƒ ∘ p ∘ t) (cΟƒ (p ∘ t) (cond₁ Ξ” t tC p pΞ”))
    goal = tc₃ (Οƒ ∘ p ∘ t) _ _ (q ∘ t) fact
  c₂ : (p : ₂ℕ → U Δ) (q : (α : ₂ℕ) → Aσ (p α)) →
       (d : Ξ£ \(n : β„•) β†’ (s : β‚‚Fin n) β†’ Ξ£ \(psΞ” : p ∘ cons s ∈ Probe Ξ”)
          β†’ q ∘ cons s ∈ Q' (p ∘ cons s) psΞ”) β†’
       q ∈ Q' p (condβ‚‚ Ξ” p (pr₁ d , Ξ» s β†’ pr₁ (prβ‚‚ d s)))
  cβ‚‚ p q (n , ΞΎ) = goal
   where
    ΞΎ' : (s : β‚‚Fin n)
       β†’ Ξ£ \(ΟƒpsΞ“ : Οƒ ∘ p ∘ cons s ∈ Probe Ξ“) β†’ q ∘ cons s ∈ Q (Οƒ ∘ p ∘ cons s) ΟƒpsΞ“
    ΞΎ' s = cΟƒ (p ∘ cons s) (pr₁ (ΞΎ s)) , prβ‚‚ (ΞΎ s)
    fact : q ∈ Q (Οƒ ∘ p) (condβ‚‚ Ξ“ (Οƒ ∘ p) (n , Ξ» s β†’ pr₁ (ΞΎ' s)))
    fact = tcβ‚‚ (Οƒ ∘ p) q (n , ΞΎ')
    goal : q ∈ Q (Οƒ ∘ p) (cΟƒ p (condβ‚‚ Ξ” p (n , Ξ» s β†’ pr₁ (ΞΎ s))))
    goal = tc₃ (Οƒ ∘ p) _ _ q fact
  c₃ : (p : β‚‚β„• β†’ U Ξ”) (pΞ” pΞ”' : p ∈ Probe Ξ”) (q : (Ξ± : β‚‚β„•) β†’ AΟƒ (p Ξ±)) β†’
       Q' p pΞ” q β†’ Q' p pΞ”' q
  c₃ p _ _ = tc₃ (Οƒ ∘ p) _ _

βŸͺ_,_,_⟫_[_]ᡐ : (Ξ“ Ξ” : Con) (A : Ty Ξ“)
             β†’ Tm Ξ“ A β†’ (Οƒ : Sub Ξ” Ξ“) β†’ Tm Ξ” (βŸͺ Ξ“ , Ξ” ⟫ A [ Οƒ ]ΚΈ)
βŸͺ Ξ“ , Ξ” , (A , Q , _) ⟫ (u , cu) [ Οƒ , cΟƒ ]ᡐ = uΟƒ , cuΟƒ
 where
  uσ : (δ : U Δ) → A (σ δ)
  uσ δ = u (σ δ)
  cuΟƒ : (p : β‚‚β„• β†’ U Ξ”) (pΞ” : p ∈ Probe Ξ”) β†’ uΟƒ ∘ p ∈ Q (Οƒ ∘ p) (cΟƒ p pΞ”)
  cuΟƒ p pΞ” = cu (Οƒ ∘ p) (cΟƒ p pΞ”)

\end{code}

Context comprehension is given by the sigma-space of a family, equipped
with the evident probe structure.

\begin{code}

_β‚Š_ : (Ξ“ : Con) β†’ Ty Ξ“ β†’ Con
Ξ“ β‚Š (A , Q , pQ , tcβ‚€ , tc₁ , tcβ‚‚ , tc₃) = (Ξ£ A , R , cβ‚€ , c₁ , cβ‚‚)
 where
  R : (β‚‚β„• β†’ Ξ£ A) β†’ 𝓀₀ Μ‡
  R r = Ξ£ \(rΞ“ : pr₁ ∘ r ∈ Probe Ξ“) β†’ prβ‚‚ ∘ r ∈ Q (pr₁ ∘ r) rΞ“
  cβ‚€ : (w : Ξ£ A) β†’ (Ξ» Ξ± β†’ w) ∈ R
  cβ‚€ (Ξ³ , a) = condβ‚€ Ξ“ Ξ³ , tcβ‚€ Ξ³ a
  c₁ : (t : β‚‚β„• β†’ β‚‚β„•) (tC : t ∈ C) (r : β‚‚β„• β†’ Ξ£ A) (rR : r ∈ R) β†’ r ∘ t ∈ R
  c₁ t tC r (rΞ“ , rQ) = cond₁ Ξ“ t tC (pr₁ ∘ r) rΞ“ ,
                        tc₁ t tC (pr₁ ∘ r) rΞ“ (prβ‚‚ ∘ r) rQ
  cβ‚‚ : (r : β‚‚β„• β†’ Ξ£ A)
     β†’ (Ξ£ \(n : β„•) β†’ βˆ€(s : β‚‚Fin n) β†’ r ∘ cons s ∈ R) β†’ r ∈ R
  cβ‚‚ r (n , ΞΎ) = condβ‚‚ Ξ“ (pr₁ ∘ r) (n , Ξ» s β†’ pr₁ (ΞΎ s)) ,
                 tcβ‚‚ (pr₁ ∘ r) (prβ‚‚ ∘ r) (n , ΞΎ)

βŸͺ_,_⟫p : (Ξ“ : Con) (A : Ty Ξ“) β†’ Sub (Ξ“ β‚Š A) Ξ“
βŸͺ Ξ“ , A ⟫p = pr₁ , (Ξ» p pΞ“A β†’ pr₁ pΞ“A)

βŸͺ_⟫_[p]ΚΈ : (Ξ“ : Con) β†’ (A : Ty Ξ“) β†’ Ty (Ξ“ β‚Š A)
βŸͺ Ξ“ ⟫ A [p]ΚΈ = βŸͺ Ξ“ , Ξ“ β‚Š A ⟫ A [ βŸͺ Ξ“ , A ⟫p ]ΚΈ

βŸͺ_,_⟫q : (Ξ“ : Con) (A : Ty Ξ“) β†’ Tm (Ξ“ β‚Š A) (βŸͺ Ξ“ ⟫ A [p]ΚΈ)
βŸͺ Ξ“ , A ⟫q = prβ‚‚ , (Ξ» p pΞ“A β†’ prβ‚‚ pΞ“A)

βŸͺ_,_,_⟫⟨_,_⟩ : (Ξ“ Ξ” : Con) (A : Ty Ξ“)
             β†’ (Οƒ : Sub Ξ” Ξ“) β†’ Tm Ξ” (βŸͺ Ξ“ , Ξ” ⟫ A [ Οƒ ]ΚΈ)
             β†’ Sub Ξ” (Ξ“ β‚Š A)
βŸͺ Ξ“ , Ξ” , A ⟫⟨ (Οƒ , cΟƒ) , (u , cu) ⟩ = (Οƒu , cΟƒu)
 where
  Οƒu : U Ξ” β†’ Ξ£ (U A)
  Οƒu Ξ΄ = (Οƒ Ξ΄ , u Ξ΄)
  cΟƒu : βˆ€(p : β‚‚β„• β†’ U Ξ”) (pΞ” : p ∈ Probe Ξ”) β†’ Οƒu ∘ p ∈ Probe (Ξ“ β‚Š A)
  cσu p pΔ = (cσ p pΔ , cu p pΔ)

\end{code}

We can now assemble these operations into a CwF structure on spaces.

\begin{code}

SpaceCwFStructure : CwFStructure
SpaceCwFStructure = record {
    Con = Space
  ; Sub = Map
  ; idSub = Ξ» {Ξ“} β†’ idMap Ξ“
  ; _β—‹_ = Ξ» {Ξ“ Ξ” Θ} f g β†’ βŸͺ Ξ“ , Ξ” , Θ ⟫ f β—‹ g
  ; Ξ΅ = πŸ™Space
  ; Ξ΅Sub = Ξ» {Ξ“} β†’ continuous-unit Ξ“
  ; Ty = Ty
  ; _[_] = Ξ» {Ξ“ Ξ”} A Οƒ β†’ βŸͺ Ξ“ , Ξ” ⟫ A [ Οƒ ]ΚΈ
  ; Tm = Tm
  ; _⁅_⁆ = Ξ» {Ξ“ Ξ” A} t Οƒ β†’ βŸͺ Ξ“ , Ξ” , A ⟫ t [ Οƒ ]ᡐ
  ; _β‚Š_ = _β‚Š_
  ; ⟨_,_⟩ = Ξ» {Ξ“ Ξ” A} Οƒ u β†’ βŸͺ Ξ“ , Ξ” , A ⟫⟨ Οƒ , u ⟩
  ; p = Ξ» {Ξ“ A} β†’ βŸͺ Ξ“ , A ⟫p
  ; q = Ξ» {Ξ“ A} β†’ βŸͺ Ξ“ , A ⟫q
  }

\end{code}

We next verify the basic equalities satisfied by this structure.

For the term equalities below we work with raw equalities, without the
explicit transports that appear in `CwFLaws`. This is enough for the
present concrete development because the family `Tm Ξ“ A` only depends
definitionally on the family part and the probe predicate part of
`A : Ty Ξ“`; it ignores the proof components. For example,
`βŸͺ Ξ“ , Ξ“ , A ⟫ t [ idMap Ξ“ ]ᡐ ＝ t` type checks because reindexing along
`idMap` leaves those data judgmentally unchanged, even though the full
equality `βŸͺ Ξ“ , Ξ“ ⟫ A [ idMap Ξ“ ]ΚΈ ＝ A` still needs proof irrelevance for
the proof fields.

Accordingly, this file does not yet package the results below into an
element of `CwFLaws SpaceCwFStructure`. The record `CwFLaws` phrases
some laws, such as `tm[id]`, `tm[β—‹]`, `q,-Ξ²`, and `,β—‹-distrib`, with
transports along the corresponding type equalities. To build that
record one would still need bridge lemmas showing that these transports
act trivially on the concrete term family used here.

\begin{code}

-- Left unit law for substitutions.
-- id ∘ Οƒ ＝ Οƒ
idl : {Ξ“ Ξ” : Con} {Οƒ : Sub Ξ“ Ξ”}
    β†’ βŸͺ Ξ“ , Ξ” , Ξ” ⟫ idMap Ξ” β—‹ Οƒ ＝ Οƒ
idl = refl

-- Right unit law for substitutions.
-- Οƒ ∘ id = Οƒ
idr : {Ξ“ Ξ” : Con} {Οƒ : Sub Ξ“ Ξ”}
    β†’ βŸͺ Ξ“ , Ξ“ , Ξ” ⟫ Οƒ β—‹ idMap Ξ“ ＝ Οƒ
idr = refl

-- Associativity of substitution composition.
-- (Οƒ ∘ Ο„) ∘ ρ = Οƒ ∘ (Ο„ ∘ ρ)
β—‹-assoc : {Ξ“ Ξ” Θ Ξ : Con} {Οƒ : Sub Θ Ξ} {Ο„ : Sub Ξ” Θ} {ρ : Sub Ξ“ Ξ”}
        β†’ βŸͺ Ξ“ , Ξ” , Ξ ⟫ (βŸͺ Ξ” , Θ , Ξ ⟫ Οƒ β—‹ Ο„) β—‹ ρ ＝
          βŸͺ Ξ“ , Θ , Ξ ⟫ Οƒ β—‹ (βŸͺ Ξ“ , Ξ” , Θ ⟫ Ο„ β—‹ ρ)
β—‹-assoc = refl

-- There is a unique substitution into the terminal context.
Ξ΅Sub-unique : {Ξ“ : Con} {Οƒ : Sub Ξ“ πŸ™Space}
            β†’ Οƒ ＝ continuous-unit Ξ“
Ξ΅Sub-unique = refl

-- Type substitution by the identity map is extensionality equal to the original type.
-- A [ id ] = A
ty[id] : (Ξ“ : Con) (A : Ty Ξ“)
       β†’ βŸͺ Ξ“ , Ξ“ ⟫ A [ idMap Ξ“ ]ΚΈ ＝ A
ty[id] Ξ“ A =
  to-Σ-＝
    (refl ,
     to-Σ-＝
       (refl ,
        to-Γ—-＝ refl
          (dependent-probe-axioms-is-prop Ξ“ _ _ (tyProbe-is-prop Ξ“ A) _ _)))

-- Type substitution is compatible with composition.
-- A [ Οƒ ∘ Ο„ ] = A [ Οƒ ] [ Ο„ ]
ty[β—‹] : (Ξ“ Ξ” Θ : Con) (A : Ty Ξ“) (Οƒ : Sub Ξ” Ξ“) (Ο„ : Sub Θ Ξ”)
      β†’ βŸͺ Ξ“ , Θ ⟫ A [ βŸͺ Θ , Ξ” , Ξ“ ⟫ Οƒ β—‹ Ο„ ]ΚΈ ＝
        βŸͺ Ξ” , Θ ⟫ βŸͺ Ξ“ , Ξ” ⟫ A [ Οƒ ]ΚΈ [ Ο„ ]ΚΈ
ty[β—‹] Ξ“ Ξ” Θ A Οƒ Ο„ =
  to-Σ-＝
    (refl ,
     to-Σ-＝
       (refl ,
        to-Γ—-＝ refl
          (dependent-probe-axioms-is-prop Θ _ _ (tyProbe-is-prop Θ Aστ) _ _)))
 where
  Aστ : Ty Θ
  Aστ = βŸͺ Ξ“ , Θ ⟫ A [ βŸͺ Θ , Ξ” , Ξ“ ⟫ Οƒ β—‹ Ο„ ]ΚΈ

-- Term substitution by the identity map is judgmentally trivial in this concrete model.
-- t [ id ] = t
tm[id] : (Ξ“ : Con) (A : Ty Ξ“) (t : Tm Ξ“ A)
       β†’ βŸͺ Ξ“ , Ξ“ , A ⟫ t [ idMap Ξ“ ]ᡐ ＝ t
tm[id] Ξ“ A t = refl

-- Term substitution is compatible with composition.
-- t [ Οƒ ∘ Ο„ ] = t [ Οƒ ] [ Ο„ ]
tm[β—‹] : {Ξ“ Ξ” Θ : Con} {A : Ty Ξ“} {t : Tm Ξ“ A} {Οƒ : Sub Ξ” Ξ“} {Ο„ : Sub Θ Ξ”}
      β†’ βŸͺ Ξ“ , Θ , A ⟫ t [ βŸͺ Θ , Ξ” , Ξ“ ⟫ Οƒ β—‹ Ο„ ]ᡐ ＝
        βŸͺ Ξ” , Θ , βŸͺ Ξ“ , Ξ” ⟫ A [ Οƒ ]ΚΈ ⟫ βŸͺ Ξ“ , Ξ” , A ⟫ t [ Οƒ ]ᡐ [ Ο„ ]ᡐ
tm[β—‹] = refl

-- The first projection of a comprehension pair is the original substitution.
-- p ∘ ⟨ Οƒ , t ⟩ ＝ Οƒ
p,-Ξ² : {Ξ“ Ξ” : Con} {A : Ty Ξ“} {Οƒ : Sub Ξ” Ξ“} {t : Tm Ξ” (βŸͺ Ξ“ , Ξ” ⟫ A [ Οƒ ]ΚΈ)}
     β†’ βŸͺ Ξ” , Ξ“ β‚Š A , Ξ“ ⟫ βŸͺ Ξ“ , A ⟫p β—‹ βŸͺ Ξ“ , Ξ” , A ⟫⟨ Οƒ , t ⟩ ＝ Οƒ
p,-Ξ² = refl

-- The second projection of a comprehension pair recovers the given term.
-- q [ ⟨ Οƒ , t ⟩ ] = t
q,-Ξ² : {Ξ“ Ξ” : Con} {A : Ty Ξ“} {Οƒ : Sub Ξ” Ξ“} {t : Tm Ξ” (βŸͺ Ξ“ , Ξ” ⟫ A [ Οƒ ]ΚΈ)}
     β†’ βŸͺ Ξ“ β‚Š A , Ξ” , βŸͺ Ξ“ ⟫ A [p]ΚΈ ⟫ βŸͺ Ξ“ , A ⟫q [ βŸͺ Ξ“ , Ξ” , A ⟫⟨ Οƒ , t ⟩ ]ᡐ ＝ t
q,-Ξ² = refl

-- Pairing the projections yields the identity substitution on the comprehension context.
-- ⟨ p , q ⟩ ＝ id
p,q-Ξ· : {Ξ“ Ξ” : Con} {A : Ty Ξ“} {Οƒ : Sub Ξ” Ξ“} {t : Tm Ξ” (βŸͺ Ξ“ , Ξ” ⟫ A [ Οƒ ]ΚΈ)}
      β†’ βŸͺ Ξ“ , Ξ“ β‚Š A , A ⟫⟨ βŸͺ Ξ“ , A ⟫p , βŸͺ Ξ“ , A ⟫q ⟩ ＝ idMap (Ξ“ β‚Š A)
p,q-Ξ· = refl

-- Pairing is stable under postcomposition.
-- ⟨ Οƒ , t ⟩ ∘ Ο„ = ⟨ Οƒ ∘ Ο„ , t [ Ο„ ] ⟩
,β—‹-distrib : {Ξ“ Ξ” Θ : Con} {A : Ty Ξ“}
           β†’ {Οƒ : Sub Ξ” Ξ“} {t : Tm Ξ” (βŸͺ Ξ“ , Ξ” ⟫ A [ Οƒ ]ΚΈ)} {Ο„ : Sub Θ Ξ”}
           β†’ βŸͺ Θ , Ξ” , Ξ“ β‚Š A ⟫ βŸͺ Ξ“ , Ξ” , A ⟫⟨ Οƒ , t ⟩ β—‹ Ο„ ＝
             βŸͺ Ξ“ , Θ , A ⟫⟨ βŸͺ Θ , Ξ” , Ξ“ ⟫ Οƒ β—‹ Ο„ , βŸͺ Ξ” , Θ , βŸͺ Ξ“ , Ξ” ⟫ A [ Οƒ ]ΚΈ ⟫ t [ Ο„ ]ᡐ ⟩
,β—‹-distrib = refl

\end{code}