EQUIV

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 )