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 isoPath (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, ★ )