3. Simplicial Type Theory

These formalisations correspond in part to Section 3 of the RS17 paper.

This is a literate rzk file:

#lang rzk-1

Simplices and their subshapes

Simplices

The 1-simplex

#def Δ¹
  : 2 → TOPE
  := \ t → TOP

The 2-simplex

#def Δ²
  : ( 2 × 2) → TOPE
  := \ (t , s) → s ≤ t

The 3-simplex

#def Δ³
  : ( 2 × 2 × 2) → TOPE
  := \ ((t1 , t2) , t3) → t3 ≤ t2 ∧ t2 ≤ t1

Boundaries of simplices

The boundary of a 1-simplex

#def ∂Δ¹
  : Δ¹ → TOPE
  := \ t → (t ≡ 0₂ ∨ t ≡ 1₂)

The boundary of a 2-simplex

#def ∂Δ²
  : Δ² → TOPE
  :=
    \ (t , s) → (s ≡ 0₂ ∨ t ≡ 1₂ ∨ s ≡ t)

The 2 dimensional inner horn

#def Λ
  : ( 2 × 2) → TOPE
  := \ (t , s) → (s ≡ 0₂ ∨ t ≡ 1₂)

#def Λ²₁
  : Δ² → TOPE
  := \ (s , t) → Λ (s , t)

The 3 dimensional inner horns

For Δ³ with coordinates ((t₁, t₂), t₃) and t₃ ≤ t₂ ≤ t₁, faces are numbered as in hom3 (RS17): face 3 is t₃ ≡ 0₂, face 2 is t₂ ≡ t₃, face 1 is t₁ ≡ t₂, face 0 is t₁ ≡ 1₂. The inner horn Λ³_k is the union of all faces except face k.

#def Λ³₁
  : Δ³ → TOPE
  := \ ((t1 , t2) , t3) → t3 ≡ 0₂ ∨ t2 ≡ t3 ∨ t1 ≡ 1₂

#def Λ³₂
  : Δ³ → TOPE
  := \ ((t1 , t2) , t3) → t3 ≡ 0₂ ∨ t1 ≡ t2 ∨ t1 ≡ 1₂

Products

The product of topes defines the product of shapes.

#def shape-prod
  ( I J : CUBE)
  ( ψ : I → TOPE)
  ( χ : J → TOPE)
  : ( I × J) → TOPE
  := \ (t , s) → ψ t ∧ χ s

The square as a product

#def Δ¹×Δ¹
  : ( 2 × 2) → TOPE
  := shape-prod 2 2 Δ¹ Δ¹

The total boundary of the square

#def ∂□
  : ( 2 × 2) → TOPE
  := \ (t , s) → ((∂Δ¹ t) ∧ (Δ¹ s)) ∨ ((Δ¹ t) ∧ (∂Δ¹ s))

The vertical boundary of the square

#def ∂Δ¹×Δ¹
  : ( 2 × 2) → TOPE
  := shape-prod 2 2 ∂Δ¹ Δ¹

The horizontal boundary of the square

#def Δ¹×∂Δ¹
  : ( 2 × 2) → TOPE
  := shape-prod 2 2 Δ¹ ∂Δ¹

The prism from a 2-simplex in an arrow type

#def Δ²×Δ¹
  : ( 2 × 2 × 2) → TOPE
  := shape-prod (2 × 2) 2 Δ² Δ¹

#def Δ³×Δ²
  : ( ( 2 × 2 × 2) × (2 × 2)) → TOPE
  := shape-prod (2 × 2 × 2) (2 × 2) Δ³ Δ²

Maps out of \(Δ²\) are a retract of maps out of \(Δ¹×Δ¹\).

RS17, Proposition 3.6

#def Δ²-is-retract-Δ¹×Δ¹
  ( A : U)
  : is-retract-of (Δ² → A) (Δ¹×Δ¹ → A)
  :=
    ( ( \ f → \ (t , s) →
        recOR
          ( t ≤ s ↦ f (t , t)
          , s ≤ t ↦ f (t , s)))
    , ( ( \ f → \ ts → f ts) , \ _ → refl))

Maps out of \(Δ³\) are a retract of maps out of \(Δ²×Δ¹\).

RS17, Proposition 3.7

#def Δ³-is-retract-Δ²×Δ¹-retraction
  ( A : U)
  : ( Δ²×Δ¹ → A) → (Δ³ → A)
  := \ f → \ ((t1 , t2) , t3) → f ((t1 , t3) , t2)

#def Δ³-is-retract-Δ²×Δ¹-section
  ( A : U)
  : ( Δ³ → A) → (Δ²×Δ¹ → A)
  :=
    \ f → \ ((t1 , t2) , t3) →
    recOR
      ( t3 ≤ t2 ↦ f ((t1 , t2) , t2)
      , t2 ≤ t3 ↦
          recOR
            ( t3 ≤ t1 ↦ f ((t1 , t3) , t2)
            , t1 ≤ t3 ↦ f ((t1 , t1) , t2)))

#def Δ³-is-retract-Δ²×Δ¹
  ( A : U)
  : is-retract-of (Δ³ → A) (Δ²×Δ¹ → A)
  :=
    ( Δ³-is-retract-Δ²×Δ¹-section A
    , ( Δ³-is-retract-Δ²×Δ¹-retraction A , \ _ → refl))

Pushout product

Pushout product Φ×ζ ∪_{Φ×χ} ψ×χ of Φ ↪ ψ and χ ↪ ζ, domain of the co-gap map.

#def shape-pushout-prod
  ( I J : CUBE)
  ( ψ : I → TOPE)
  ( Φ : ψ → TOPE)
  ( ζ : J → TOPE)
  ( χ : ζ → TOPE)
  : ( shape-prod I J ψ ζ) → TOPE
  := \ (t , s) → (Φ t ∧ ζ s) ∨ (ψ t ∧ χ s)

Intersections

The intersection of shapes is defined by conjunction on topes.

#def shape-intersection
  ( I : CUBE)
  ( ψ χ : I → TOPE)
  : I → TOPE
  := \ t → ψ t ∧ χ t

Unions

The union of shapes is defined by disjunction on topes.

#def shape-union
  ( I : CUBE)
  ( ψ χ : I → TOPE)
  : I → TOPE
  := \ t → ψ t ∨ χ t

Gluing of shapes in low dimensions

We now define instances of the “gluing” construction from RS17, Definition 3.8, for all pairs of dimensions with \(0 \leq n \leq 2\) and \(0 \leq m \leq 2\). For each \(n,m\), the shapes \(A : 2^{1+n+1} → \mathrm{TOPE}\) and \(B : 2^{1+m+1} → \mathrm{TOPE}\) are glued to a shape in \(2^{1+n+1+m+1}\) by precomposing with the appropriate coordinate maps and then taking a conjunction of the resulting topes, as in the paper.

#def shape-gluing-0-0
  ( A B : (2 × 2) → TOPE)
  : ( 2 × 2 × 2) → TOPE
  := \ ((t- , u) , s+) →
    A (t- , u) ∧ B (u , s+)

#def shape-gluing-1-0
  ( A : (2 × 2 × 2) → TOPE)
  ( B : (2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2) → TOPE
  := \ (((t- , t1) , u) , s+) →
    A ((t- , t1) , u) ∧ B (u , s+)

#def shape-gluing-0-1
  ( A : (2 × 2) → TOPE)
  ( B : (2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2) → TOPE
  := \ (((t- , u) , s1) , s+) →
    A (t- , u) ∧ B ((u , s1) , s+)

#def shape-gluing-2-0
  ( A : (2 × 2 × 2 × 2) → TOPE)
  ( B : (2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2 × 2) → TOPE
  := \ ((((t- , t1) , t2) , u) , s+) →
    A (((t- , t1) , t2) , u) ∧ B (u , s+)

#def shape-gluing-0-2
  ( A : (2 × 2) → TOPE)
  ( B : (2 × 2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2 × 2) → TOPE
  := \ ((((t- , u) , s1) , s2) , s+) →
    A (t- , u) ∧ B (((u , s1) , s2) , s+)

#def shape-gluing-1-1
  ( A B : (2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2 × 2) → TOPE
  := \ ((((t- , t1) , u) , s1) , s+) →
    A ((t- , t1) , u) ∧ B ((u , s1) , s+)

#def shape-gluing-1-2
  ( A : (2 × 2 × 2) → TOPE)
  ( B : (2 × 2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2 × 2 × 2) → TOPE
  := \ (((((t- , t1) , u) , s1) , s2) , s+) →
    A ((t- , t1) , u) ∧ B (((u , s1) , s2) , s+)

#def shape-gluing-2-1
  ( A : (2 × 2 × 2 × 2) → TOPE)
  ( B : (2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2 × 2 × 2) → TOPE
  := \ (((((t- , t1) , t2) , u) , s1) , s+) →
    A (((t- , t1) , t2) , u) ∧ B ((u , s1) , s+)

#def shape-gluing-2-2
  ( A B : (2 × 2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2 × 2 × 2 × 2) → TOPE
  := \ ((((((t- , t1) , t2) , u) , s1) , s2) , s+) →
    A (((t- , t1) , t2) , u) ∧ B (((u , s1) , s2) , s+)

Restrictions of shapes in low dimensions

Following RS17, Definition 3.11, we define the restriction of a shape in 2^{1+n+1} by fixing the “bottom” coordinate to 1₂ and the “top” coordinate to 0₂ and then forgetting these coordinates.

For n = 0 we obtain an unrestricted shape, and for 1 ≤ n ≤ 3 we obtain shapes in 2ⁿ.

#def shape-restriction-0
  ( A : (2 × 2) → TOPE)
  : TOPE
  := A (1₂ , 0₂)

#def shape-restriction-1
  ( A : (2 × 2 × 2) → TOPE)
  : 2 → TOPE
  := \ t1 → A ((1₂ , t1) , 0₂)

#def shape-restriction-2
  ( A : (2 × 2 × 2 × 2) → TOPE)
  : ( 2 × 2) → TOPE
  := \ (t1 , t2) → A (((1₂ , t1) , t2) , 0₂)

#def shape-restriction-3
  ( A : (2 × 2 × 2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2) → TOPE
  := \ ((t1 , t2) , t3) → A ((((1₂ , t1) , t2) , t3) , 0₂)

#def shape-restriction-4
  ( A : (2 × 2 × 2 × 2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2) → TOPE
  := \ (((t1 , t2) , t3) , t4) →
    A (((((1₂ , t1) , t2) , t3) , t4) , 0₂)

#def shape-restriction-5
  ( A : (2 × 2 × 2 × 2 × 2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2 × 2) → TOPE
  := \ ((((t1 , t2) , t3) , t4) , t5) →
    A ((((((1₂ , t1) , t2) , t3) , t4) , t5) , 0₂)

Joins of shapes in low dimensions

Using the gluing and restriction operations above, we now define low-dimensional instances of the join construction from RS17, Definition 3.13, for the cases 0 ≤ n ≤ 2 and 0 ≤ m ≤ 2.

#def shape-join-0-0
  ( A B : (2 × 2) → TOPE)
  : 2 → TOPE
  := shape-restriction-1 (shape-gluing-0-0 A B)

#def shape-join-0-1
  ( A : (2 × 2) → TOPE)
  ( B : (2 × 2 × 2) → TOPE)
  : ( 2 × 2) → TOPE
  := shape-restriction-2 (shape-gluing-0-1 A B)

#def shape-join-0-2
  ( A : (2 × 2) → TOPE)
  ( B : (2 × 2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2) → TOPE
  := shape-restriction-3 (shape-gluing-0-2 A B)

#def shape-join-1-0
  ( A : (2 × 2 × 2) → TOPE)
  ( B : (2 × 2) → TOPE)
  : ( 2 × 2) → TOPE
  := shape-restriction-2 (shape-gluing-1-0 A B)

#def shape-join-1-1
  ( A B : (2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2) → TOPE
  := shape-restriction-3 (shape-gluing-1-1 A B)

#def shape-join-1-2
  ( A : (2 × 2 × 2) → TOPE)
  ( B : (2 × 2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2) → TOPE
  := shape-restriction-4 (shape-gluing-1-2 A B)

#def shape-join-2-0
  ( A : (2 × 2 × 2 × 2) → TOPE)
  ( B : (2 × 2) → TOPE)
  : ( 2 × 2 × 2) → TOPE
  := shape-restriction-3 (shape-gluing-2-0 A B)

#def shape-join-2-1
  ( A : (2 × 2 × 2 × 2) → TOPE)
  ( B : (2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2) → TOPE
  := shape-restriction-4 (shape-gluing-2-1 A B)

#def shape-join-2-2
  ( A B : (2 × 2 × 2 × 2) → TOPE)
  : ( 2 × 2 × 2 × 2 × 2) → TOPE
  := shape-restriction-5 (shape-gluing-2-2 A B)

Pushout joins in low dimensions

Finally, we combine joins and unions to obtain low-dimensional instances of the pushout join construction from RS17, Definition 3.15. Given inclusions of augmented shapes A ⊂ B and C ⊂ D, the pushout join is the subshape (A ⋆ D) ∪ (B ⋆ C) of B ⋆ D. At the level of topes, this is expressed by shape-union of the corresponding joins.

#def shape-pushout-join-0-0
  ( B D : (2 × 2) → TOPE)
  ( A : B → TOPE)
  ( C : D → TOPE)
  : 2 → TOPE
  := shape-union 2
       ( shape-join-0-0 A D)
       ( shape-join-0-0 B C)

#def shape-pushout-join-0-1
  ( B : (2 × 2) → TOPE)
  ( D : (2 × 2 × 2) → TOPE)
  ( A : B → TOPE)
  ( C : D → TOPE)
  : ( 2 × 2) → TOPE
  := shape-union (2 × 2)
       ( shape-join-0-1 A D)
       ( shape-join-0-1 B C)

#def shape-pushout-join-0-2
  ( B : (2 × 2) → TOPE)
  ( D : (2 × 2 × 2 × 2) → TOPE)
  ( A : B → TOPE)
  ( C : D → TOPE)
  : ( 2 × 2 × 2) → TOPE
  := shape-union (2 × 2 × 2)
       ( shape-join-0-2 A D)
       ( shape-join-0-2 B C)

#def shape-pushout-join-1-0
  ( B : (2 × 2 × 2) → TOPE)
  ( D : (2 × 2) → TOPE)
  ( A : B → TOPE)
  ( C : D → TOPE)
  : ( 2 × 2) → TOPE
  := shape-union (2 × 2)
       ( shape-join-1-0 A D)
       ( shape-join-1-0 B C)

#def shape-pushout-join-1-1
  ( B D : (2 × 2 × 2) → TOPE)
  ( A : B → TOPE)
  ( C : D → TOPE)
  : ( 2 × 2 × 2) → TOPE
  := shape-union (2 × 2 × 2)
       ( shape-join-1-1 A D)
       ( shape-join-1-1 B C)

#def shape-pushout-join-1-2
  ( B : (2 × 2 × 2) → TOPE)
  ( D : (2 × 2 × 2 × 2) → TOPE)
  ( A : B → TOPE)
  ( C : D → TOPE)
  : ( 2 × 2 × 2 × 2) → TOPE
  := shape-union (2 × 2 × 2 × 2)
       ( shape-join-1-2 A D)
       ( shape-join-1-2 B C)

#def shape-pushout-join-2-0
  ( B : (2 × 2 × 2 × 2) → TOPE)
  ( D : (2 × 2) → TOPE)
  ( A : B → TOPE)
  ( C : D → TOPE)
  : ( 2 × 2 × 2) → TOPE
  := shape-union (2 × 2 × 2)
       ( shape-join-2-0 A D)
       ( shape-join-2-0 B C)

#def shape-pushout-join-2-1
  ( B : (2 × 2 × 2 × 2) → TOPE)
  ( D : (2 × 2 × 2) → TOPE)
  ( A : B → TOPE)
  ( C : D → TOPE)
  : ( 2 × 2 × 2 × 2) → TOPE
  := shape-union (2 × 2 × 2 × 2)
       ( shape-join-2-1 A D)
       ( shape-join-2-1 B C)

#def shape-pushout-join-2-2
  ( B D : (2 × 2 × 2 × 2) → TOPE)
  ( A : B → TOPE)
  ( C : D → TOPE)
  : ( 2 × 2 × 2 × 2 × 2) → TOPE
  := shape-union (2 × 2 × 2 × 2 × 2)
       ( shape-join-2-2 A D)
       ( shape-join-2-2 B C)

Connection squares

RS17 Proposition 3.5(a)

#define join-square-arrow
  ( A : U)
  ( f : 2 → A)
  : ( 2 × 2) → A
  := \ (t , s) → recOR (t ≤ s ↦ f s , s ≤ t ↦ f t)

RS17 Proposition 3.5(b)

#define meet-square-arrow
  ( A : U)
  ( f : 2 → A)
  : ( 2 × 2) → A
  := \ (t , s) → recOR (t ≤ s ↦ f t , s ≤ t ↦ f s)

Functorial comparisons of shapes

Functorial retracts

For a subshape ϕ ⊂ ψ we have an easy way of stating that it is a retract in a strict and functorial way. Intuitively this happens when there is a map from ψ to ϕ that fixes the subshape ψ. But in the definition below we actually ask for a section of the family of extensions of a function ϕ → A to a function ψ → A and we ask for this section to be natural in the type A.

#def is-functorial-shape-retract
  ( I : CUBE)
  ( ψ : I → TOPE)
  ( ϕ : ψ → TOPE)
  : U
  :=
    ( A' : U) → (A : U) → (α : A' → A)
  → has-section-family-over-map
      ( ϕ → A') (\ f → (t : ψ) → A' [ϕ t ↦ f t])
      ( ϕ → A) (\ f → (t : ψ) → A [ϕ t ↦ f t])
      ( \ f t → α (f t))
      ( \ _ g t → α (g t))

For example, this applies to Δ² ⊂ Δ¹×Δ¹.

#def is-functorial-retract-Δ²-Δ¹×Δ¹
  : is-functorial-shape-retract (2 × 2) (Δ¹×Δ¹) (Δ²)
  :=
    \ A' A α →
      ( ( first (Δ²-is-retract-Δ¹×Δ¹ A') , first (Δ²-is-retract-Δ¹×Δ¹ A))
        , \ a' → refl)

Every functorial shape retract automatically induces a section when restricting to diagrams extending a fixed diagram σ': ϕ → A' (or, respectively, its image ϕ → A under α).

#def relativize-is-functorial-shape-retract
  ( I : CUBE)
  ( ψ : I → TOPE)
  ( χ : ψ → TOPE)
  ( is-fretract-ψ-χ : is-functorial-shape-retract I ψ χ)
  ( ϕ : χ → TOPE)
  ( A' A : U)
  ( α : A' → A)
  ( σ' : ϕ → A')
  : has-section-family-over-map
      ( ( t : χ) → A' [ϕ t ↦ σ' t])
      ( \ τ' → (t : ψ) → A' [χ t ↦ τ' t])
      ( ( t : χ) → A [ϕ t ↦ α (σ' t)])
      ( \ τ → (t : ψ) → A [χ t ↦ τ t])
      ( \ τ' t → α (τ' t))
      ( \ _ υ' t → α (υ' t))
  :=
    ( ( \ τ' → first (first (is-fretract-ψ-χ A' A α)) τ'
      , \ τ → second (first (is-fretract-ψ-χ A' A α)) τ
      )
    , \ τ' → second (is-fretract-ψ-χ A' A α) τ'
    )

Isomorphisms of shape inclusions

Consider two shape inclusions ϕ ⊂ ψ and ζ ⊂ χ. We want to express the fact that there is an isomorphism ψ ≅ χ of shapes which restricts to an isomorphism ϕ ≅ ζ. Since shapes are not types themselves, the best we can currently do is describe this isomorphism on representables.

#def isomorphism-shape-inclusions
  ( I : CUBE)
  ( ψ : I → TOPE)
  ( ϕ : ψ → TOPE)
  ( J : CUBE)
  ( χ : J → TOPE)
  ( ζ : χ → TOPE)
  : U
  :=
    ( Σ ( f : (A : U) → Equiv (ζ → A) (ϕ → A))
      , ( ( A : U)
        → ( σ : ζ → A)
        → ( Equiv
            ( ( t : χ) → A [ζ t ↦ σ t])
            ( ( t : ψ) → A [ϕ t ↦ first (f A) σ t]))))

#def functorial-isomorphism-shape-inclusions
  ( I : CUBE)
  ( ψ : I → TOPE)
  ( ϕ : ψ → TOPE)
  ( J : CUBE)
  ( χ : J → TOPE)
  ( ζ : χ → TOPE)
  : U
  :=
  Σ ( ( f , F) : isomorphism-shape-inclusions I ψ ϕ J χ ζ)
  , ( Σ ( e
      : ( A' : U)
        → ( A : U)
        → ( α : A' → A)
        → ( σ' : ζ → A')
        → ( ( \ (t : I | ϕ t) → α (first (f A') σ' t))
          = ( first (f A) (\ t → α (σ' t)))))
      , ( ( A' : U)
        → ( A : U)
        → ( α : A' → A)
        → ( σ' : ζ → A')
        → ( τ' : (t : χ) → A' [ζ t ↦ σ' t])
        → ( ( transport (ϕ → A) (\ σ → (t : ψ) → A [ϕ t ↦ σ t])
              ( \ (t : I | ϕ t) → α (first (f A') σ' t))
              ( first (f A) (\ t → α (σ' t)))
              ( e A' A α σ')
              ( \ (t : ψ) → α (first (F A' σ') τ' t)))
            = ( first (F A (\ (t : ζ) → α (σ' t))) (\ (t : χ) → α (τ' t))))))

In practice, the isomorphisms are usually given via an explicit formula, which would define a map ψ → ϕ if ψ and ϕ were themselves types. In this case all the coherences are just refl, hence it is easy to produce a term of type functorial-isomorphism-shape-inclusions I ψ ϕ J χ ζ.

For example, consider the two shape inclusions {0} ⊂ Δ¹ (subshapes of 2) and {1} ⊂ right-leg-of-Λ (subshapes of 2 × 2), where

#def left-leg-of-Λ
  : Λ → TOPE
  := \ (t , s) → s ≡ 0₂

#def right-leg-of-Λ
  : Λ → TOPE
  := \ (t , s) → t ≡ 1₂

These two shape inclusions are canonically isomorphic via the formulas

-- not valid rzk code
#def f : Δ¹ → right-leg-of-Λ
  \ s → (1₂ , s)

#def g : right-leg-of-Λ → Δ¹
  \ (t , s) → s

We turn these formulas into a functorial shape inclusion as follows. Unfortunately we have to repeat the same formula multiple times, leading to some ugly boilerplate code.

#def isomorphism-1-Δ¹-1-left-leg-of-Λ
  : isomorphism-shape-inclusions
    ( 2 × 2) (\ ts → left-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)
    2 Δ¹ (\ t → t ≡ 1₂)
  :=
    ( \ A →
      ( \ τ (t , s) → τ t
      , ( ( \ υ s → υ (s , 0₂) , \ _ → refl)
        , ( \ υ s → υ (s , 0₂) , \ _ → refl)))
    , \ A _ →
      ( \ τ (t , s) → τ t
      , ( ( \ υ s → υ (s , 0₂) , \ _ → refl)
        , ( \ υ s → υ (s , 0₂) , \ _ → refl))))

#def isomorphism-0-Δ¹-1-right-leg-of-Λ
  : isomorphism-shape-inclusions
    ( 2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)
    2 Δ¹ (\ t → t ≡ 0₂)
  :=
    ( \ A →
      ( \ τ (t , s) → τ s
      , ( ( \ υ s → υ (1₂ , s) , \ _ → refl)
        , ( \ υ s → υ (1₂ , s) , \ _ → refl)))
    , \ A _ →
      ( \ τ (t , s) → τ s
      , ( ( \ υ s → υ (1₂ , s) , \ _ → refl)
        , ( \ υ s → υ (1₂ , s) , \ _ → refl))))

#def functorial-isomorphism-1-Δ¹-1-left-leg-of-Λ
  : functorial-isomorphism-shape-inclusions
    ( 2 × 2) (\ ts → left-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)
    2 Δ¹ (\ t → t ≡ 1₂)
  :=
    ( isomorphism-1-Δ¹-1-left-leg-of-Λ
    , ( \ _ _ _ _ → refl , \ _ _ _ _ _ → refl))

#def functorial-isomorphism-0-Δ¹-1-right-leg-of-Λ
  : functorial-isomorphism-shape-inclusions
    ( 2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)
    2 Δ¹ (\ t → t ≡ 0₂)
  :=
    ( isomorphism-0-Δ¹-1-right-leg-of-Λ
    , ( \ _ _ _ _ → refl , \ _ _ _ _ _ → refl))

Functorial retracts of shape inclusions

We want to express what it means for a shape inclusion ζ ⊂ χ to be a retract of another shape inclusion ϕ ⊂ ψ.

If these shapes were types, we would require a commutative diagram

ζ ⊂ χ
↓   ↓
ϕ ⊂ ψ
↓   ↓
ζ ⊂ χ

such that the vertical composites are the identity. As before, we cannot say this directly; instead we express this property on representables. Since the upper vertical maps are necessarily monomorphisms, we may we may assume up to isomorphism (which we already dealt with) that ζ ⊂ χ are actual subshapes of ϕ ⊂ ψ.

We observe that we must have ζ = χ ∧ ϕ. Thus we have the following setting:

#section retracts-shape-inclusions

#variable I : CUBE
#variable ψ : I → TOPE
#variables ϕ χ : ψ → TOPE
-- ζ := χ ∧ ϕ

#def retract-shape-inclusion
  : U
  :=
  Σ ( s
      : ( A : U)
    → ( σ : (t : I | χ t ∧ ϕ t) → A)
    → ( t : ϕ)
    → A [ χ t ∧ ϕ t ↦ σ t])
  , ( ( A : U)
    → ( σ : (t : I | χ t ∧ ϕ t) → A)
    → ( τ : (t : χ) → A [χ t ∧ ϕ t ↦ σ t])
    → ( t : ψ)
    → A [χ t ↦ τ t , ϕ t ↦ s A σ t])

#def functorial-retract-shape-inclusion
  : U
  :=
  Σ ( ( s , S) : retract-shape-inclusion)
  , Σ ( h
        : ( A' : U)
      → ( A : U)
      → ( α : A' → A)
      → ( σ' : (t : I | χ t ∧ ϕ t) → A')
      → ( ( \ (t : I | ϕ t) → α (s A' σ' t))
        =_{ (t : ϕ) → A [χ t ∧ ϕ t ↦ α (σ' t)]}
  ( s A (\ t → α (σ' t)))))
    , ( ( A' : U)
      → ( A : U)
      → ( α : A' → A)
      → ( σ' : (t : I | χ t ∧ ϕ t) → A')
      → ( τ' : (t : χ) → A' [χ t ∧ ϕ t ↦ σ' t])
      → ( ( transport
            ( ( t : ϕ) → A [χ t ∧ ϕ t ↦ α (σ' t)])
            ( \ σ → (t : ψ) → A [χ t ↦ α (τ' t) , ϕ t ↦ σ t])
            ( \ t → α (s A' σ' t))
            ( \ t → s A (\ t' → α (σ' t')) t)
            ( h A' A α σ')
            ( \ t → α (S A' σ' τ' t)))
        =_{ (t : ψ) → A [χ t ↦ α (τ' t) , ϕ t ↦ s A (\ t' → α (σ' t')) t]}
  ( S A (\ t → α (σ' t)) (\ t → α (τ' t)))))

#end retracts-shape-inclusions

For example the pair {00} ⊂ Δ² is a retract of {0} × Δ¹ ⊂ Δ¹ × Δ¹.

#def functorial-retract-00-Δ²-0Δ¹-Δ¹×Δ¹
  : functorial-retract-shape-inclusion (2 × 2)
    ( Δ¹×Δ¹) (\ (t , _) → t ≡ 0₂)
    ( \ ts → Δ² ts)
  :=
  ( ( ( \ _ f (t , s) → recOR (t ≤ s ↦ f (t , t) , s ≤ t ↦ f (t , s)))
    , ( \ _ _ f (t , s) → recOR (t ≤ s ↦ f (t , t) , s ≤ t ↦ f (t , s))))
  , ( \ _ _ _ _ → refl , \ _ _ _ _ _ → refl))

For completeness we verify that the intesection Δ² ∧ {0}×Δ¹ is indeed {00}.

#def verify-functorial-retract-0-Δ²-0Δ¹-Δ¹×Δ¹
  ( A : U)
  : ( ( shape-intersection (2 × 2) (\ ts → Δ² ts) (\ (t , _) → t ≡ 0₂) → A)
    = ( ( ( t , s) : 2 × 2 | t ≡ 0₂ ∧ s ≡ 0₂) → A))
  := refl