intro

groupoid · Oct 29, 2023 · e88cf18 · e88cf18
1 parent 1552687
commit e88cf18
Show file tree

Hide file tree

Showing 5 changed files with 96 additions and 82 deletions.
diff --git a/intro/index.html b/intro/index.html
@@ -38,12 +38,20 @@
 просторів шляхів <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.025ex;" xmlns="http://www.w3.org/2000/svg" width="4.81ex" height="1.595ex" role="img" focusable="false" viewBox="0 -694 2126 705" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1414-TEX-N-50" d="M130 622Q123 629 119 631T103 634T60 637H27V683H214Q237 683 276 683T331 684Q419 684 471 671T567 616Q624 563 624 489Q624 421 573 372T451 307Q429 302 328 301H234V181Q234 62 237 58Q245 47 304 46H337V0H326Q305 3 182 3Q47 3 38 0H27V46H60Q102 47 111 49T130 61V622ZM507 488Q507 514 506 528T500 564T483 597T450 620T397 635Q385 637 307 637H286Q237 637 234 628Q231 624 231 483V342H302H339Q390 342 423 349T481 382Q507 411 507 488Z"></path><path id="MJX-1414-TEX-N-61" d="M137 305T115 305T78 320T63 359Q63 394 97 421T218 448Q291 448 336 416T396 340Q401 326 401 309T402 194V124Q402 76 407 58T428 40Q443 40 448 56T453 109V145H493V106Q492 66 490 59Q481 29 455 12T400 -6T353 12T329 54V58L327 55Q325 52 322 49T314 40T302 29T287 17T269 6T247 -2T221 -8T190 -11Q130 -11 82 20T34 107Q34 128 41 147T68 188T116 225T194 253T304 268H318V290Q318 324 312 340Q290 411 215 411Q197 411 181 410T156 406T148 403Q170 388 170 359Q170 334 154 320ZM126 106Q126 75 150 51T209 26Q247 26 276 49T315 109Q317 116 318 175Q318 233 317 233Q309 233 296 232T251 223T193 203T147 166T126 106Z"></path><path id="MJX-1414-TEX-N-74" d="M27 422Q80 426 109 478T141 600V615H181V431H316V385H181V241Q182 116 182 100T189 68Q203 29 238 29Q282 29 292 100Q293 108 293 146V181H333V146V134Q333 57 291 17Q264 -10 221 -10Q187 -10 162 2T124 33T105 68T98 100Q97 107 97 248V385H18V422H27Z"></path><path id="MJX-1414-TEX-N-68" d="M41 46H55Q94 46 102 60V68Q102 77 102 91T102 124T102 167T103 217T103 272T103 329Q103 366 103 407T103 482T102 542T102 586T102 603Q99 622 88 628T43 637H25V660Q25 683 27 683L37 684Q47 685 66 686T103 688Q120 689 140 690T170 693T181 694H184V367Q244 442 328 442Q451 442 463 329Q464 322 464 190V104Q464 66 466 59T477 49Q498 46 526 46H542V0H534L510 1Q487 2 460 2T422 3Q319 3 310 0H302V46H318Q379 46 379 62Q380 64 380 200Q379 335 378 343Q372 371 358 385T334 402T308 404Q263 404 229 370Q202 343 195 315T187 232V168V108Q187 78 188 68T191 55T200 49Q221 46 249 46H265V0H257L234 1Q210 2 183 2T145 3Q42 3 33 0H25V46H41Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="50" xlink:href="#MJX-1414-TEX-N-50"></use><use data-c="61" xlink:href="#MJX-1414-TEX-N-61" transform="translate(681,0)"></use><use data-c="74" xlink:href="#MJX-1414-TEX-N-74" transform="translate(1181,0)"></use><use data-c="68" xlink:href="#MJX-1414-TEX-N-68" transform="translate(1570,0)"></use></g></g></g></g></svg></mjx-container> таким чином, що вони
 утворюють фібраційну рівність яка
 збігається (доводиться в самій теорії) з простором шляхів.
-</p><code>isContr <span class="h__symbol">(</span>A<span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span><span class="h__symbol">:</span> <span class="h__keyword">U</span> <span class="h__symbol">:</span><span class="h__symbol">=</span> Σ <span class="h__symbol">(</span>x<span class="h__symbol">:</span> A<span class="h__symbol">)</span>, Π <span class="h__symbol">(</span>y<span class="h__symbol">:</span> A<span class="h__symbol">)</span>, <span class="h__keyword">Path</span> A x y
-fiber <span class="h__symbol">(</span>A B<span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">(</span>f<span class="h__symbol">:</span> A <span class="h__symbol">→</span> B<span class="h__symbol">)</span> <span class="h__symbol">(</span>y<span class="h__symbol">:</span> B<span class="h__symbol">)</span><span class="h__symbol">:</span> <span class="h__keyword">U</span> <span class="h__symbol">:</span><span class="h__symbol">=</span> Σ <span class="h__symbol">(</span>x<span class="h__symbol">:</span> A<span class="h__symbol">)</span>, <span class="h__keyword">Path</span> B y <span class="h__symbol">(</span>f x<span class="h__symbol">)</span>
-isEquiv <span class="h__symbol">(</span>A B<span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">(</span>f<span class="h__symbol">:</span> A <span class="h__symbol">→</span> B<span class="h__symbol">)</span><span class="h__symbol">:</span> <span class="h__keyword">U</span> <span class="h__symbol">:</span><span class="h__symbol">=</span> Π <span class="h__symbol">(</span>y<span class="h__symbol">:</span> B<span class="h__symbol">)</span>, isContr <span class="h__symbol">(</span>fiber A B f y<span class="h__symbol">)</span>
-equiv<span class="h__symbol">(</span>X Y<span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span><span class="h__symbol">:</span> <span class="h__keyword">U</span> <span class="h__symbol">:</span><span class="h__symbol">=</span> Σ <span class="h__symbol">(</span>f<span class="h__symbol">:</span> X <span class="h__symbol">→</span> Y<span class="h__symbol">)</span>, isEqiv X Y f
-ua <span class="h__symbol">(</span>A B <span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">(</span>p <span class="h__symbol">:</span> <span class="h__keyword">Path</span> <span class="h__keyword">U</span> A B<span class="h__symbol">)</span> <span class="h__symbol">:</span> equiv A B
-   <span class="h__symbol">:</span><span class="h__symbol">=</span> <span class="h__keyword">transp</span> <span class="h__symbol">(</span>&lt;i> equiv A <span class="h__symbol">(</span>p @ i<span class="h__symbol">))</span> 0 <span class="h__symbol">(</span>idEquiv A<span class="h__symbol">)</span></code><br><p>Завдяки відсутності ета-правила у рівності,
+</p><code><span class="h__keyword">def</span> isContr <span class="h__symbol">(</span>A<span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">:</span> <span class="h__keyword">U</span>
+ <span class="h__symbol">:</span><span class="h__symbol">=</span> Σ <span class="h__symbol">(</span>x<span class="h__symbol">:</span> A<span class="h__symbol">)</span>, Π <span class="h__symbol">(</span>y<span class="h__symbol">:</span> A<span class="h__symbol">)</span>, <span class="h__keyword">Path</span> A x y
+
+<span class="h__keyword">def</span> fiber <span class="h__symbol">(</span>A B<span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">(</span>f<span class="h__symbol">:</span> A <span class="h__symbol">→</span> B<span class="h__symbol">)</span> <span class="h__symbol">(</span>y<span class="h__symbol">:</span> B<span class="h__symbol">)</span><span class="h__symbol">:</span> <span class="h__keyword">U</span>
+ <span class="h__symbol">:</span><span class="h__symbol">=</span> Σ <span class="h__symbol">(</span>x<span class="h__symbol">:</span> A<span class="h__symbol">)</span>, <span class="h__keyword">Path</span> B y <span class="h__symbol">(</span>f x<span class="h__symbol">)</span>
+
+<span class="h__keyword">def</span> isEquiv <span class="h__symbol">(</span>A B<span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">(</span>f<span class="h__symbol">:</span> A <span class="h__symbol">→</span> B<span class="h__symbol">)</span><span class="h__symbol">:</span> <span class="h__keyword">U</span>
+ <span class="h__symbol">:</span><span class="h__symbol">=</span> Π <span class="h__symbol">(</span>y<span class="h__symbol">:</span> B<span class="h__symbol">)</span>, isContr <span class="h__symbol">(</span>fiber A B f y<span class="h__symbol">)</span>
+
+<span class="h__keyword">def</span> equiv<span class="h__symbol">(</span>X Y<span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span><span class="h__symbol">:</span> <span class="h__keyword">U</span>
+ <span class="h__symbol">:</span><span class="h__symbol">=</span> Σ <span class="h__symbol">(</span>f<span class="h__symbol">:</span> X <span class="h__symbol">→</span> Y<span class="h__symbol">)</span>, isEqiv X Y f
+
+<span class="h__keyword">def</span> ua <span class="h__symbol">(</span>A B <span class="h__symbol">:</span> <span class="h__keyword">U</span><span class="h__symbol">)</span> <span class="h__symbol">(</span>p <span class="h__symbol">:</span> <span class="h__keyword">Path</span> <span class="h__keyword">U</span> A B<span class="h__symbol">)</span> <span class="h__symbol">:</span> equiv A B
+ <span class="h__symbol">:</span><span class="h__symbol">=</span> <span class="h__keyword">transp</span> <span class="h__symbol">(</span>&lt;i> equiv A <span class="h__symbol">(</span>p @ i<span class="h__symbol">))</span> 0 <span class="h__symbol">(</span>idEquiv A<span class="h__symbol">)</span></code><br><p>Завдяки відсутності ета-правила у рівності,
 не кожні два доведення одного простору шляхів
 дорівнюють між собою, отже
 простір шляхів утворює багатовимірну структуру

diff --git a/intro/index.pug b/intro/index.pug
@@ -69,12 +69,20 @@ block content
                     збігається (доводиться в самій теорії) з простором шляхів.
 
                 +code.
-                    isContr (A: U): U := Σ (x: A), Π (y: A), Path A x y
-                    fiber (A B: U) (f: A → B) (y: B): U := Σ (x: A), Path B y (f x)
-                    isEquiv (A B: U) (f: A → B): U := Π (y: B), isContr (fiber A B f y)
-                    equiv(X Y: U): U := Σ (f: X → Y), isEqiv X Y f
-                    ua (A B : U) (p : Path U A B) : equiv A B
-                       := transp (&lt;i> equiv A (p @ i)) 0 (idEquiv A)
+                    def isContr (A: U) : U
+                     := Σ (x: A), Π (y: A), Path A x y
+
+                    def fiber (A B: U) (f: A → B) (y: B): U
+                     := Σ (x: A), Path B y (f x)
+
+                    def isEquiv (A B: U) (f: A → B): U
+                     := Π (y: B), isContr (fiber A B f y)
+
+                    def equiv(X Y: U): U
+                     := Σ (f: X → Y), isEqiv X Y f
+
+                    def ua (A B : U) (p : Path U A B) : equiv A B
+                     := transp (&lt;i> equiv A (p @ i)) 0 (idEquiv A)
                 br.
                 p.
                     Завдяки відсутності ета-правила у рівності,

diff --git a/lib/foundations/univalent/equiv.anders b/lib/foundations/univalent/equiv.anders
@@ -49,14 +49,12 @@ def univ-computation (A B : U) (p : PathP (<_> U) A B)
  := <j i> Glue B (j ∨ ∂ i) [(i = 0) → (A, univ-elim A B p), (i = 1) → (B, idEquiv B),
                             (j = 1) → (p @ i, univ-elim (p @ i) B (<k> p @ (i ∨ k)))]
 
---- Equiv as Identity System [Escardó] 2014
+--- Equiv as [Right] Identity System [Escardó] 2014
 
 def single (B : U) : U := Σ (A: U), equiv A B
-def EquivIsContr (B: U) : isContr (single B)
- := ?
+def EquivIsContr (B: U) : isContr (single B) := ?
 def isContr→isProp (A: U) (w: isContr A) (a b : A) : Path A a b
- := <i> hcomp A (∂ i) (λ (j : I), [(i = 0) → a, (i = 1) → (w.2 b) @ j])
-                      ((<i4> w.2 a @ -i) @ i)
+ := <i> hcomp A (∂ i) (λ (j : I), [(i = 0) → a, (i = 1) → (w.2 b) @ j]) ((<i4> w.2 a @ -i) @ i)
 def contrSinglEquiv (A B : U) (e : equiv A B)
   : Path (single B) (B,idEquiv B) (A,e)
  := isContr→isProp (single B) (EquivIsContr B) (B,idEquiv B) (A,e)
@@ -88,3 +86,13 @@ def hcomp-Glue' (A : U) (φ : I)
           (λ (i : I), [(ψ = 1) → u i 1=1]) (ouc u₀)
 --- def Glue-computation
 --- def Glue-uniqueness
+
+-- The other notion of equality such as Half Adjoint Equivalence and
+-- Bi-Invertible Equivalences could be introduced and encoded as isomorphism by analogy.
+
+def isHae (A B : U) (f : A -> B): U :=
+  Σ (g : B -> A) (eta_: Path (idᵀ A) (∘ A B A g f) (id A)) (eps_: Path (idᵀ B) (∘ B A B f g) (id B)),
+  Π (x : A), Path B (f ((eta_ @ 0) x)) ((eps_ @ 0) (f x))
+
+def hae (A B : U) : U := Σ (f : A -> B), isHae A B f
+
diff --git a/lib/foundations/univalent/iso.anders b/lib/foundations/univalent/iso.anders
@@ -82,34 +82,27 @@ def iso (A B: U) : U :=
     (t : retract A B f g),
     𝟏
 
-def iso-intro (A: U)
-  : iso A A
- := ( id A,
-      id A,
-      (\(x:A), <_>x),
-      (\(x:A), <_>x),
-      ★
-    )
+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)]
+
+--- Iso as [Right] Identity System [Sokhatsky]
 
+def iso-intro (A: U) : iso A A := ( id A, id A, (\(x:A), <_>x), (\(x:A), <_>x), ★)
 def iso-single (B : U) : U := Σ (A: U), iso A B
 def iso-EquivIsContr (B: U) : isContr (iso-single B) := ?
 def iso-isContr→isProp (A: U) (w: isContr A) (a b : A) : Path A a b
- := <i> hcomp A (∂ i) (λ (j : I), [(i = 0) → a, (i = 1) → (w.2 b) @ j])
-                      ((<i4> w.2 a @ -i) @ i)
+ := <i> hcomp A (∂ i) (λ (j : I), [(i = 0) → a, (i = 1) → (w.2 b) @ j]) ((<i4> w.2 a @ -i) @ i)
 def iso-contrSinglEquiv (A B : U) (e : iso A B)
   : Path (iso-single B) (B,iso-intro B) (A,e)
  := isContr→isProp (iso-single B) (iso-EquivIsContr B) (B,iso-intro B) (A,e)
 def iso-J (A B: U) (P: Π (A B: U), iso A B → U) (r: P B B (iso-intro B))
   : Π (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
-
-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)]
+                          (B,iso-intro B) (A,e) (iso-contrSinglEquiv A B e) r
 
 -- 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
@@ -120,7 +113,13 @@ def iso→Path (A B : U) (f : A -> B) (g : B -> A)
 def uni-Form (A B: U) : U₁ := iso A B -> PathP (<_>U) A B
 def uni-Intro (A B: U) : uni-Form A B := \ (x : iso A B), iso→Path A B x.f x.g x.s x.t
 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, star )
+ := λ (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,
+        ★
+      )
 
 -- The notion of Minivalence as forth-back map between fibrational equivalence
 -- and section/retract-based isomorphism is mentioned in Cubical Agda sources.
@@ -131,12 +130,3 @@ def mini-Form (A B : U) : U := iso A B -> equiv A B
 def mini-Intro (A B : U) : mini-Form A B := \ (x : iso A B), univ-elim A B (iso→Path A B x.f x.g x.s x.t)
 def mini-Elim (A B : U) : equiv A B -> iso A B := \ (x : equiv A B), ( x.f, inv-equiv A B x, ret-equiv A B x, sec-equiv A B x, star)
 
--- The other notion of equality such as Half Adjoint Equivalence and
--- Bi-Invertible Equivalences could be introduced and encoded as isomorphism by analogy.
-
-def isHae (A B : U) (f : A -> B): U :=
-  Σ (g : B -> A) (eta_: Path (idᵀ A) (∘ A B A g f) (id A)) (eps_: Path (idᵀ B) (∘ B A B f g) (id B)),
-  Π (x : A), Path B (f ((eta_ @ 0) x)) ((eps_ @ 0) (f x))
-
-def hae (A B : U) : U := Σ (f : A -> B), isHae A B f
-