# ISOMORPHISM

Just like

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

```
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

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

## Elimination

```
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

## Formation

## 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

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