EQUIVALENCE

Formation

(Fiberwise Equivalence). Fiberwise equivalence or of function represents internal equality of types and in the universe as contractible fibers of over base .

def isContr (A: U) : U
 := Σ (x: A), Π (y: A), Path A x y

def fiber (A B : U) (f: A → B) (y : B): U
 := Σ (x : A), Path B y (f x)

def isEquiv (A B : U) (f : A → B) : U
 := Π (y : B), isContr (fiber A B f y)

def equiv (A B : U) : U
 := Σ (f : A → B), isEquiv A B f

Introduction

(Fiberwise Reflection). There is a fiberwise instance of that is derived as :

def singl (A: U) (a: A): U
 := Σ (x: A), Path A a x

def contr (A : U) (a b : A) (p : Path A a b)
  : Path (singl A a) (eta A a) (b, p)
 := <i> (p @ i, <j> p @ i /\ j)

def isContrSingl (A : U) (a : A)
  : isContr (singl A a)
 := ((a,idp A a),
     (\(z:singl A a),contr A a z.1 z.2))

def idEquiv (A : U)
  : equiv A A
 := (\(a:A) -> a, isContrSingl A)

Elimination

(Fiberwise Induction Principle). For any and it's evidence at there is a function . HoTT 5.8.5

def J-equiv (A B: U)
    (P: Π (A B: U), equiv A B → U)
    (d: P B B (idEquiv B))
  : Π (e: equiv A B), P A B e
 := λ (e: equiv A B),
      subst (single B) (\ (z: single B), P z.1 B z.2)
            (B,idEquiv B) (A,e)
            (contrSinglEquiv A B e) d

Computation

(Fiberwise Computation of Induction Principle).

def compute-Equiv (A : U)
    (C : Π (A B: U), equiv A B → U)
    (d: C A A (idEquiv A))
  : Path (C A A (idEquiv A)) d
         (ind-Equiv A A C d (idEquiv A))

UNIVALENCE

The notion of univalence represents transport between fibrational equivalence as contractability of fibers and homotopical multi-dimentional heterogeneous path equality (HoTT 2.10):

The type is called type. Univalence is packed as isomorphism where intro is obtained by type and elim is obtained by transport from constant map.

Formation

(Univalence Formation).

def univ-formation (A B : U)
 := equiv A B → PathP (<_> U) A B

Introduction

(Univalence Intro). Glueing onto is an operation when using and onto itself when using the identity equivalence. The term ua(e) is a path from to as the type reduces when the boundary conditions are satisfied when this reduces to and when it reduces to .

def univ-intro (A B : U)
  : univ-formation A B
 := λ (e : equiv A B),
    <i> Glue B (∂ i)
     [ (i = 0) → (A, e),
       (i = 1) → (B, idEquiv B) ]

Elimination

(Univalence Elimination).

def univ-elim (A B : U)
    (p : PathP (<_> U) A B)
  : equiv A B
 := transp (<i> equiv A (p @ i))
           0 (idEquiv A)

Computation

(Univalence Computation).

Uniqueness

(Univalence Uniqueness).

def univ-computation (A B : U)
    (p : PathP (<_> U) A B)
  : PathP (<_> PathP (<_> U) A B)
          (univ-intro A B (univ-elim A B p)) p
 := <j i> Glue B (j ∨ ∂ i)
       [ (i = 0) → (A, univ-elim A B p),
         (i = 1) → (B, idEquiv B),
         (j = 1) → (p @ i, univ-elim (p @ i)
                           B (<k> p @ (i ∨ k))) ]

MINIVALENCE

The notion of Minivalence as forth-back map between fibrational equivalence and section/retract-based isomorphism is mentioned in Cubical Agda sources.

Formation

(Minivalence Formation).

def mini-Form (A B : U) : U
 := iso A B -> equiv A B

Introduction

(Minivalence Introduction).

def mini-Intro (A B : U)
  : mini-Form A B
 := \ (x : iso A B),
      univ-elim A B
        (isoPath A B x.f x.g x.s x.t)

Elimination

(Minivalence Elimination).

def mini-Elim (A B : U)
  : equiv A B -> iso A B
 := \ (x : equiv A B),
      ( x.f,
        inv-equiv A B x,
        ret-equiv A B x,
        sec-equiv A B x,
        star
      )