iso

groupoid · Oct 30, 2023 · ef679a2 · ef679a2
1 parent d32bc74
commit ef679a2
Show file tree

Hide file tree

Showing 17 changed files with 588 additions and 567 deletions.
diff --git a/foundations/univalent/iso/index.html b/foundations/univalent/iso/index.html
diff --git a/foundations/univalent/iso/index.pug b/foundations/univalent/iso/index.pug
@@ -21,7 +21,22 @@ block content
                 time Published: 26 NOV 2017
             +tex.
                 Just like $\mathrm{Equiv}$ notion of $\mathrm{Iso}$ represents equality
-                of types $A$ and $B$ within given universe $U$.
+                of types $A$ and $B$ within given universe $U$. However instead of Fibration it
+                uses Section and Retract for its definition and unlike equivalence
+                isomorphism predicate is not a proposition:
+            +tex(true).
+                $$
+                    \prod_{f : A \rightarrow B}\mathrm{isProp}\ (\mathrm{isEquiv}_f),
+                $$
+            +tex(true).
+                $$
+                    \prod_{f : \Pi(x:S^1), x\equiv x} \neg \mathrm{isProp}\ (\mathrm{isIso}_f).
+                $$
+            +tex.
+                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.
             h2 Formation
             +tex.
                 $\mathbf{Definition}$ (Isomorphism Formation).

diff --git a/foundations/univalent/path/index.html b/foundations/univalent/path/index.html
diff --git a/intro/index.html b/intro/index.html
diff --git a/mathematics/algebra/algebra/index.html b/mathematics/algebra/algebra/index.html
diff --git a/mathematics/algebra/homology/index.html b/mathematics/algebra/homology/index.html
diff --git a/mathematics/analysis/set/index.html b/mathematics/analysis/set/index.html
diff --git a/mathematics/categories/category/index.html b/mathematics/categories/category/index.html
diff --git a/mathematics/categories/presheaf/index.html b/mathematics/categories/presheaf/index.html
diff --git a/mathematics/categories/topos/index.html b/mathematics/categories/topos/index.html
diff --git a/mathematics/geometry/bundle/index.html b/mathematics/geometry/bundle/index.html
diff --git a/mathematics/geometry/derham/index.html b/mathematics/geometry/derham/index.html
diff --git a/mathematics/homotopy/cw/index.html b/mathematics/homotopy/cw/index.html
diff --git a/mathematics/homotopy/hopf/index.html b/mathematics/homotopy/hopf/index.html
diff --git a/mathematics/homotopy/pullback/index.html b/mathematics/homotopy/pullback/index.html
diff --git a/mathematics/homotopy/pushout/index.html b/mathematics/homotopy/pushout/index.html
diff --git a/spec/index.html b/spec/index.html