def iso→Path (A B : U)
+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)
diff --git a/foundations/univalent/iso/index.pug b/foundations/univalent/iso/index.pug
index d4db3e9d..287bd318 100644
--- a/foundations/univalent/iso/index.pug
+++ b/foundations/univalent/iso/index.pug
@@ -95,7 +95,7 @@ block content
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 $\mathrm{Uni}$ here.
+ cubical systems and is called Unimorphism or $\mathrm{isoPath}$ here.
h2 Formation
+tex.
$\mathbf{Definition}$ (Unimorphism Formation).
@@ -108,7 +108,7 @@ block content
$\mathbf{Definition}$ (Unimorphism Introduction).
+tex(true).
$$
- \mathrm{uni} : \prod_{A,B:U}\prod_{x:\mathrm{Iso}} A = B =_{def}
+ \mathrm{isoPath} : \prod_{A,B:U}\prod_{x:\mathrm{Iso}} A = B =_{def}
$$
+tex(true).
$$