iso

groupoid · Oct 30, 2023 · 3ab10a2 · 3ab10a2
1 parent 70a9f8e
commit 3ab10a2
Show file tree

Hide file tree

Showing 17 changed files with 584 additions and 568 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
@@ -46,14 +46,30 @@ block content
                 $$
             +tex(true).
                 $$
-                   \sum_{f:A\rightarrow B}
-                   \sum_{g:B\rightarrow A}
+                   \sum_{f:A\rightarrow B} \mathrm{isiso}_f
+                $$
+            +tex.
+                $\mathbf{Definition\ 9.1.1}$ (Isomorphism Path Predicate).
+            +tex(true).
+                $$
+                    \mathrm{isiso}_f : U =_{def} \sum_{g:B\rightarrow A}
                 $$
             +tex(true).
                 $$
                           \prod_{x:A}f\hspace{-0.1em}\cdot\hspace{-0.1em}g(x)\hspace{-0.3em}\equiv\hspace{-0.1em}x
                    \times \prod_{y:B}g\hspace{-0.1em}\cdot\hspace{-0.2em}f(y)\hspace{-0.1em}\equiv\hspace{-0.1em}y.
                 $$
+            +tex.
+                $\mathbf{Definition\ 9.1.2}$ (Isomorphism Homotopy Predicate).
+            +tex(true).
+                $$
+                    \mathrm{isqinv}_f : U =_{def} \sum_{g:B\rightarrow A}
+                $$
+            +tex(true).
+                $$
+                          \prod_{x:A}f\hspace{-0.1em}\cdot\hspace{-0.1em}g\hspace{-0.1em}\sim\hspace{-0.1em}\mathrm{id}_A
+                   \times \prod_{y:B}g\hspace{-0.0em}\cdot\hspace{-0.2em}f\hspace{-0.1em}\sim\hspace{-0.1em}\mathrm{id}_B.
+                $$
             +code.
                 def iso (A B: U) : U :=
                   Σ (f : A -> B) (g : B -> A)

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