Tope disjuction elimination along identity paths¶

\(\mathsf{rec}_{\lor}^{\ψ,\φ}(a_\ψ, a*\φ)\) (written recOR(ψ, φ, a_psi, a_phi) in the code) is well-typed when \(a*\ψ\) and \(a*\φ\) are _definitionally equal* on \(\ψ \land \φ\). Sometimes this is too strong since many terms are not definitionally equal, but only equal up to a path. Luckily, assuming relative function extensionality, we can define a weaker version of \(rec*{\lor}\) (recOR), which we call recId, that can work in presence of a witness of type \(\prod*{t : I \mid \ψ \land \φ} a*\ψ = a*\φ\).

Prerequisites¶

We begin by introducing common HoTT definitions:

#lang rzk-1
-- A is contractible there exists x : A such that for any y : A we have x = y.
#define iscontr (A : U) : U
  := Σ (a : A), (x : A) → a =_{A} x

-- A is a proposition if for any x, y : A we have x = y
#define isaprop (A : U) : U
  := (x : A) → (y : A) → x =_{A} y

-- A is a set if for any x, y : A the type x =_{A} y is a proposition
#define isaset (A : U) : U
  := (x : A) → (y : A) → isaprop (x =_{A} y)

-- Non-dependent product of A and B
#define prod (A : U) (B : U) : U
  := Σ (x : A), B

-- A function f : A → B is an equivalence
-- if there exists g : B → A
-- such that for all x : A we have g (f x) = x
-- and for all y : B we have f (g y) = y
#define isweq (A : U) (B : U) (f : A → B) : U
  := Σ (g : B → A), prod ((x : A) → g (f x) =_{A} x) ((y : B) → f (g y) =_{B} y)

-- Equivalence of types A and B
#define weq (A : U) (B : U) : U
  := Σ (f : A → B), isweq A B f

-- Transport along a path
#define transport
    (A : U)
    (C : A → U)
    (x y : A)
    (p : x =_{A} y)
    : C x → C y
  := \ cx → idJ(A, x, (\z q → C z), cx, y, p)

Relative function extensionality¶

We can now define relative function extensionality. There are several formulations, we provide two, following Riehl and Shulman:

-- [RS17, Axiom 4.6] Relative function extensionality.
#define relfunext : U
  := (I : CUBE)
  → (ψ : I → TOPE)
  → (φ : ψ → TOPE)
  → (A : ψ → U)
  → ((t : ψ) → iscontr (A t))
  → (a : (t : φ) → A t)
  → (t : ψ) → A t [ φ t ↦ a t]

-- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality.
#define relfunext2 : U
  := (I : CUBE)
  → (ψ : I → TOPE)
  → (φ : ψ → TOPE)
  → (A : ψ → U)
  → (a : (t : φ) → A t)
  → (f : (t : ψ) → A t [ φ t ↦ a t ])
  → (g : (t : ψ) → A t [ φ t ↦ a t ])
  → weq (f = g)
         ((t : ψ) → (f t =_{A t} g t) [ φ t ↦ refl ])

Construction of `recId`¶

The idea is straightforward. We ask for a proof that a = b for all points in ψ ∧ φ. Then, by relative function extensionality (relfunext2), we can show that restrictions of a and b to ψ ∧ φ are equal. If we reformulate a as extension of its restriction, then we can transport such reformulation along the path connecting two restrictions and apply recOR.

First, we define how to restrict an extension type to a subshape:

#section construction-of-recId

#variable r : relfunext2
#variable I : CUBE
#variables ψ φ : I → TOPE
#variable A : (t : I | ψ t ∨ φ t) → U

-- Restrict extension type to a subshape.
#define restrict_phi
    (a : (t : φ) → A t)
  : (t : I | ψ t ∧ φ t) → A t
  := \ t → a t

-- Restrict extension type to a subshape.
#define restrict_psi
    (a : (t : ψ) → A t)
  : (t : I | ψ t ∧ φ t) → A t
  := \ t → a t

Then, how to reformulate an a (or b) as an extension of its restriction:

-- Reformulate extension type as an extension of a restriction.
#define ext-of-restrict_psi
    (a : (t : ψ) → A t)
  : (t : ψ) → A t [ ψ t ∧ φ t ↦ restrict_psi a t ]
  := a  -- type is coerced automatically here

-- Reformulate extension type as an extension of a restriction.
#define ext-of-restrict_phi
    (a : (t : φ) → A t)
  : (t : φ) → A t [ ψ t ∧ φ t ↦ restrict_phi a t ]
  := a  -- type is coerced automatically here

Now, assuming relative function extensionality, we construct a path between restrictions:

-- Transform extension of an identity into an identity of restrictions.
#define restricts-path
    (a_psi : (t : ψ) → A t)
    (a_phi : (t : φ) → A t)
    (e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t)
  : restrict_psi a_psi = restrict_phi a_phi
  := (first (second (r I
      (\t → ψ t ∧ φ t)
      (\t → BOT)
      (\t → A t)
      (\t → recBOT)
      (\t → a_psi t)
      (\t → a_phi t)))) e

Finally, we bring everything together into recId:

-- A weaker version of recOR, demanding only a path between a and b:
-- recOR(ψ, φ, a, b) demands that for ψ ∧ φ we have a == b (definitionally)
-- (recId ψ φ a b e) demands that e is the proof that a = b (intensionally) for ψ ∧ φ
#define recId uses (r) -- we declare that recId is using r on purpose
    (a_psi : (t : ψ) → A t)
    (a_phi : (t : φ) → A t)
    (e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t)
  : (t : I | ψ t ∨ φ t) → A t
  := \t → recOR(
        ψ t ↦ transport
          ((s : I | ψ s ∧ φ s) → A s)
          (\ra → (s : ψ) → A s [ ψ s ∧ φ s ↦ ra s ])
          (restrict_psi a_psi)
          (restrict_phi a_phi)
          (restricts-path a_psi a_phi e)
          (ext-of-restrict_psi a_psi)
          t,
        φ t ↦ ext-of-restrict_phi a_phi t
      )

#end construction-of-recId

Gluing extension types¶

An application of of recId is gluing together extension types, whenever we can show that they are equal on the intersection of shapes:

-- If two extension types are equal along two subshapes,
-- then they are also equal along their union.
#define id-along-border
    (r : relfunext2)
    (I : CUBE)
    (ψ : I → TOPE)
    (φ : I → TOPE)
    (A : (t : I | ψ t ∨ φ t) → U)
    (a b : (t : I | ψ t ∨ φ t) → A t)
    (e_psi : (t : ψ) → a t = b t)
    (e_phi : (t : φ) → a t = b t)
    (border-is-a-set : (t : I | ψ t ∧ φ t) → isaset (A t))
  : (t : I | ψ t ∨ φ t) → a t = b t
  := recId r I ψ φ
        (\t → a t = b t)
        e_psi e_phi
        (\t → border-is-a-set t (a t) (b t) (e_psi t) (e_phi t))

Tope disjuction elimination along identity paths¶

Prerequisites¶

Relative function extensionality¶

Construction of recId¶

Gluing extension types¶

Construction of `recId`¶