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