ISO

ISOMORPHISM

Just like notion of represents equality of types and within given universe . However instead of Fibration it uses Section and Retract for its definition and unlike equivalence isomorphism predicate is not a proposition:

This difference was one of the main drivers for developing cubical interpretation of equivalence/univalence as isomorphism/unimorphism is unsatisfactory candidate for basic notion of multidimensional inequality due to loss of propositional preservation.

Formation

(Isomorphism Formation).

(Isomorphism Path Predicate).

(Isomorphism Homotopy Predicate).

def iso (A B: U) : U := Σ (f : A -> B) (g : B -> A) (s : section A B f g) (t : retract A B f g), 𝟏

Introduction

(Isomorphism Introduction).

def iso-intro (A: U) : iso A A := ( id A, id A, (\(x:A), <_>x), (\(x:A), <_>x), star )

Elimination

(Isomorphism Induction Principle). For any and it's evidence at there is a function:

def ind-Iso (A B: U) (C: Π (A B: U), iso A B → U) (d: C A A (iso-Intro A)) : Π (e: iso A B), P A B e := λ (e: iso A B), subst (iso-single B) (\ (z: iso-single B), P z.1 B z.2) (B,iso-intro B) (A,e) (iso-contrSinglEquiv A B e) r

UNIMORPHISM

Similar to Fibrational Equivalence the notion of Retract/Section based Isomorphism could be introduced as forth-back transport between isomorphism and path equality. This notion is somehow cannonical to all cubical systems and is called Unimorphism or here.

Formation

(Unimorphism Formation).

Introduction

(Unimorphism Introduction).

def iso→Path (A B : U) (f : A -> B) (g : B -> A) (s : Π (y : B), Path B (f (g y)) y) (t : Π (x : A), Path A (g (f x)) x) : PathP (<_> U) A B := <i> Glue B (∂ i) [ (i = 0) -> (A,f, isoToEquiv A B f g s t), (i = 1) -> (B,id B, idIsEquiv B)]

Elimination

(Unimorphism Elimination).

def uni-Elim (A B : U) : PathP (<_> U) A B -> iso A B := λ (p : PathP (<_> U) A B), ( coerce A B p, coerce B A (<i> p @ -i), trans⁻¹-trans A B p, λ (a : A), <k> trans-trans⁻¹ A B p a @ -k, ★ )