wip

Author: 5HT

foundations/modal/modality/index.html

@@ -28,6 +28,6 @@
     <span class="h__symbol">(</span>propIsModal <span class="h__symbol">:</span> Π <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>a b <span class="h__symbol">:</span> isModal A<span class="h__symbol">)</span>,
                      <span class="h__keyword">PathP</span> <span class="h__symbol">(</span><_>isModal A<span class="h__symbol">)</span> a b<span class="h__symbol">)</span>
     <span class="h__symbol">(=</span>-Modal <span class="h__symbol">:</span> Π <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>x y <span class="h__symbol">:</span> modality A<span class="h__symbol">)</span>,
-                 isModal <span class="h__symbol">(</span><span class="h__keyword">PathP</span> <span class="h__symbol">(</span><_>modality A<span class="h__symbol">)</span> x y<span class="h__symbol">))</span>, 𝟏</code><br><h1>LITERATURE</h1><p>[1]. E.Rijke, M.Shulman, B.Spitters. <a href="https://arxiv.org/pdf/1706.07526.pdf">
-Modalities in Homotopy Type Theory</a>.<br>
+                 isModal <span class="h__symbol">(</span><span class="h__keyword">PathP</span> <span class="h__symbol">(</span><_>modality A<span class="h__symbol">)</span> x y<span class="h__symbol">))</span>, 𝟏</code><br><h1>LITERATURE</h1><p style="font-size:14px;">[1]. E.Rijke, M.Shulman, B.Spitters. <a href="https://arxiv.org/pdf/1706.07526.pdf">Modalities in Homotopy Type Theory</a>.<br>
+[2]. Daniel R. Licata, Michael Shulman, Mitchell Riley. (2017). <a href="https://dlicata.wescreates.wesleyan.edu/pubs/lsr17multi/lsr17multi-ex.pdf">A Fibrational Framework for Substructural and Modal Logics</a><br>
 </p></section></div></article><footer class="footer"><a href="https://5ht.co/license/"><img class="footer__logo" src="https://longchenpa.guru/seal.png" width="50"></a><span class="footer__copy">2021&mdash;2025 &copy; <a rel="me" href="https://mathstodon.xyz/@5ht">Namdak Tönpa</a></span></footer>

foundations/modal/modality/index.pug

@@ -56,8 +56,8 @@ block content
                 br.
 
                 h1 LITERATURE
-                p.
-                    [1]. E.Rijke, M.Shulman, B.Spitters. <a href="https://arxiv.org/pdf/1706.07526.pdf">
-                    Modalities in Homotopy Type Theory</a>.<br>
+                p(style="font-size:14px;").
+                    [1]. E.Rijke, M.Shulman, B.Spitters. <a href="https://arxiv.org/pdf/1706.07526.pdf">Modalities in Homotopy Type Theory</a>.<br>
+                    [2]. Daniel R. Licata, Michael Shulman, Mitchell Riley. (2017). <a href="https://dlicata.wescreates.wesleyan.edu/pubs/lsr17multi/lsr17multi-ex.pdf">A Fibrational Framework for Substructural and Modal Logics</a><br>
 
 include ../../../footer.pug

lib/mathematics/analysis/topology.anders

@@ -24,12 +24,6 @@ def isSetPi₁' (A: U₁) (B: A → U) (h: Π (x: A), isSet (B x)) : isSet₁ (
 def Prop := U → 𝟐
 def ℙ (X: U₁) := X → Prop
 
-def isSet-ℙ (X: U₁)
-  : isSet₁ (ℙ X)
- := isSetPi₁ X (λ (x: X), Prop) (λ (x: X), isSetPi₁' U (λ (_: U), 𝟐) (λ (_: U), boolset))
-
-axiom specify (X: U₁) : (X → Prop) → ℙ X
-
 def ∅ (X: U₁) : ℙ X := \ (_: X) (_: U), false
 def total (X: U₁) : ℙ X := \ (_: X) (_: U), true
 def ∈ (X: U₁) (el: X) (set: ℙ X) : U₁ := Path₁ (U → 𝟐) (set el) (\(_: U), true)
@@ -38,3 +32,9 @@ def ⊆ (X: U₁) (A B: ℙ X) := Π (x: X), (∈ X x A) × (∈ X x B)
 def ∁ (X: U₁) : ℙ X → ℙ X       := λ (h  : ℙ X),           λ (x: X) (Y: U), not (h x Y)
 def ∪ (X: U₁) : ℙ X → ℙ X → ℙ X := λ (h1 : ℙ X) (h2: ℙ X), λ (x: X) (Y: U), or (h1 x Y) (h2 x Y)
 def ∩ (X: U₁) : ℙ X → ℙ X → ℙ X := λ (h1 : ℙ X) (h2: ℙ X), λ (x: X) (Y: U), and (h1 x Y) (h2 x Y)
+
+def isSet-ℙ (X: U₁)
+  : isSet₁ (ℙ X)
+ := isSetPi₁ X (λ (x: X), Prop) (λ (x: X), isSetPi₁' U (λ (_: U), 𝟐) (λ (_: U), boolset))
+
+axiom specify (X: U₁) : (X → Prop) → ℙ X

lib/mathematics/categories/symmetric.anders

@@ -16,8 +16,7 @@ def isMonoidal (C: precategory): U
       (tensor₁: C.C.ob)
       (left₁: Π (x: C.C.ob),  Path (C.C.ob) x (tensor.ob (tensor₁,x)))
       (right₁: Π (x: C.C.ob), Path (C.C.ob) x (tensor.ob (x,tensor₁)))
-      (associator: Π (x y z: C.C.ob),
-         Path (C.C.ob) (tensor.ob ((tensor.ob (x,y)),z)) (tensor.ob (x,(tensor.ob (y,z)))))
+      (associator: Π (x y z: C.C.ob), Path (C.C.ob) (tensor.ob ((tensor.ob (x,y)),z)) (tensor.ob (x,(tensor.ob (y,z)))))
       (triangle: Π (x y: C.C.ob), 𝟏)
       (pentagon: Π (x y z w: C.C.ob), 𝟏), 𝟏
 

lib/mathematics/homotopy/S1.anders

@@ -10,7 +10,7 @@ def loop : Path S¹ base base := resp 𝟏 𝟏 (id 𝟏) (id 𝟏) ★
 -- [Sokhatsky] 2022
 
 def Loop₀ : U := PathP (<_>𝟐) false false
-def Rec : 𝟐 -> U := λ (x : 𝟐), 2-rec U 𝟎 Loop₀ x
+def Rec : 𝟐 -> U := 2-rec U 𝟎 Loop₀
 def WS¹ : U := W (x : 𝟐), Rec x
 def Wbase : WS¹ := sup 𝟐 Rec false (ind₀ WS¹)
 def Wloop (n : WS¹) : WS¹ := sup 𝟐 Rec true (λ (x : Loop₀), n)