GLUE

types defines composition structure for fibrant universes that allows partial elements to be extended to fibrant types. In other words it turns equivalences in the multidensional cubes to path spaces. Unlike ABCHFL, CCHM needn't another universe for that purpose.

Formation

(Glue Formation). The Glue types take a partial family of types A that are equivalent to the base type B. These types are then “glued” onto B and the equivalence data gets packaged up into a new type.

def Glue' (A : U) (φ : I)
    (e : Partial (Σ (T : U), equiv T A) φ) : U
 := Glue A φ e

Introduction

(Glue Introduction).

def glue' (A : U) (φ : I)
    (u : Partial (Σ (T : U), equiv T A × T) φ)
    (a : A [φ ↦ [(φ = 1) → (u 1=>1).2.1.1 (u 1=>1).2.2]])
 := glue φ u (ouc a)

Elimination

(Glue Elimination).

def unglue' (A : U) (φ : I)
    (e : Partial (Σ (T : U), equiv T A) φ)
    (a : Glue A φ e) : A
 := unglue φ e a

Computation

(Glue Computation).

Uniqueness

(Glue Uniqueness).