headers

lib/foundations/mltt/bool.anders

@@ -1,38 +1,21 @@
 module bool where
-
 import lib/foundations/mltt/either
 import lib/foundations/mltt/proto
 
+--- data 𝟐 : U := 0₂ | 1₂
 def rec₂ (A : U) (a b : A) : 𝟐 → A := ind₂ (λ (_ : 𝟐), A) a b
-
-def 𝟐-β₁ (C : 𝟐 → U) (f : Π (x : 𝟐), C 0₂) (g : Π (y : 𝟐), C 1₂) 
-  : PathP (<_>C 0₂) (f 0₂) (ind₂ (λ (x : 𝟐), C x) (f 0₂) (g 1₂) 0₂)
- := <_> f 0₂
-
-def 𝟐-β₂ (C : 𝟐 → U) (f : Π (x : 𝟐), C 0₂) (g : Π (y : 𝟐), C 1₂) 
-  : PathP (<_>C 1₂) (g 1₂) (ind₂ (λ (x : 𝟐), C x) (f 0₂) (g 1₂) 1₂)
- := <_> g 1₂
-
-def 𝟐-η (c : 𝟐) : + (PathP (<_> 𝟐) c 0₂) (PathP (<_> 𝟐) c 1₂)
- := ind₂ (λ (c : 𝟐), + (PathP (<_> 𝟐) c 0₂) (PathP (<_> 𝟐) c 1₂))
-         (0₂, <_> 0₂) (1₂, <_> 1₂) c
-
--- data 𝟐 : U := 0₂ | 1₂
-
 def not : 𝟐 → 𝟐 := rec₂ 𝟐 1₂ 0₂
 def and : 𝟐 → 𝟐 → 𝟐 := rec₂ (𝟐 → 𝟐) (const 𝟐 𝟐 0₂) (id 𝟐)
 def or  : 𝟐 → 𝟐 → 𝟐 := rec₂ (𝟐 → 𝟐) (id 𝟐) (const 𝟐 𝟐 1₂)
 def xor : 𝟐 → 𝟐 → 𝟐 := rec₂ (𝟐 → 𝟐) (id 𝟐) not
 
--- Bitlib
-
+--- Bitlib
 def HA (a b : 𝟐) : 𝟐 × 𝟐 := (xor a b, and a b)
 def or² (a : 𝟐) (w : 𝟐 × 𝟐) : 𝟐 × 𝟐 := (w.1, or a w.2)
 def FA (a b cᵢₙ : 𝟐) : 𝟐 × 𝟐 := or² (HA a b).2 (HA (HA a b).1 cᵢₙ)
 def add-2bit (a b : 𝟐 × 𝟐) : 𝟐 × 𝟐 := ((FA a.1 b.1 (HA a.2 b.2).2).1, (HA a.2 b.2).1)
 
--- Church
-
+--- Church
 def bool′ := Π (α : U), α → α → α
 def true′  : bool′ := λ (α : U) (t f : α), t
 def false′ : bool′ := λ (α : U) (t f : α), f

lib/foundations/mltt/fin.anders

@@ -1,5 +1,7 @@
 {- Finite Set Type: https://anders.groupoid.space/foundations/mltt/fin/
-   - Vec.
+   - Fin.
+
+   HoTT 1.9 Exercise
 
    Copyright (c) Groupoid Infinity, 2014-2023. -}
 
@@ -52,8 +54,10 @@ def 2₆ : 𝟔 := inl 𝟑 𝟑 2₃
 def 3₆ : 𝟔 := inr 𝟑 𝟑 0₃
 def 4₆ : 𝟔 := inr 𝟑 𝟑 1₃
 def 5₆ : 𝟔 := inr 𝟑 𝟑 2₃
-def ind₆ (C : 𝟔 → U) (c₀ : C 0₆) (c₁ : C 1₆) (c₂ : C 2₆) (c₃ : C 3₆) (c₄ : C 4₆) (c₅ : C 5₆) : Π (x : 𝟔), C x
- := +-ind 𝟑 𝟑 C (ind₃ (λ (x : 𝟑), C (0₂, x)) c₀ c₁ c₂) (ind₃ (λ (x : 𝟑), C (1₂, x)) c₃ c₄ c₅)
+def ind₆ (C : 𝟔 → U) (c₀ : C 0₆) (c₁ : C 1₆) (c₂ : C 2₆)
+         (c₃ : C 3₆) (c₄ : C 4₆) (c₅ : C 5₆) : Π (x : 𝟔), C x
+ := +-ind 𝟑 𝟑 C (ind₃ (λ (x : 𝟑), C (0₂, x)) c₀ c₁ c₂)
+                (ind₃ (λ (x : 𝟑), C (1₂, x)) c₃ c₄ c₅)
 
 def 𝟕 : U := + 𝟑 𝟒
 def 0₇ : 𝟕 := inl 𝟑 𝟒 0₃

lib/foundations/mltt/inductive.anders

@@ -2,7 +2,11 @@
    - 0, 1, 2, W types;
 
    HoTT 1.8 The type of booleans
+   HoTT 2.8 Unit type
+   HoTT 5.1 Induction to inductive types
    HoTT 5.3 W-Types
+   HoTT 5.4 Inductive types are initial algebras
+   HoTT 5.5 Homotopy-in
 
    Copyright (c) Groupoid Infinity, 2014-2023. -}
 
@@ -34,12 +38,15 @@ def 1-η (z: 𝟏) : Path 𝟏 ★ z := idp 𝟏 ★ -- 𝟏-irrelevance enabled
 
 def 2-ind (C: 𝟐 → U) (x: C 0₂) (y: C 1₂) : П (z: 𝟐), C z := ind₂ C x y
 def 2-rec (C: U) (x y: C) : П (z: bool), C := ind₂ (\(_:𝟐), C) x y
+
 def 2-β₁ (C : 𝟐 → U) (f : Π (x : 𝟐), C 0₂) (g : Π (y : 𝟐), C 1₂)
   : PathP (<_>C 0₂) (f 0₂) (ind₂ (λ (x : 𝟐), C x) (f 0₂) (g 1₂) 0₂)
  := <_> f 0₂
+
 def 2-β₂ (C : 𝟐 → U) (f : Π (x : 𝟐), C 0₂) (g : Π (y : 𝟐), C 1₂)
   : PathP (<_>C 1₂) (g 1₂) (ind₂ (λ (x : 𝟐), C x) (f 0₂) (g 1₂) 1₂)
  := <_> g 1₂
+
 def 2-η (c : 𝟐) : + (PathP (<_> 𝟐) c 0₂) (PathP (<_> 𝟐) c 1₂)
  := ind₂ (λ (c : 𝟐), + (PathP (<_> 𝟐) c 0₂) (PathP (<_> 𝟐) c 1₂))
          (0₂, <_> 0₂) (1₂, <_> 1₂) c

lib/foundations/mltt/mltt.anders

@@ -1,34 +1,40 @@
-{- MLTT Reality Check: https://groupoid.space/articles/mltt/mltt.pdf
-   - Pi, Sigma, Path.
+{- MLTT Reality Module Check: https://groupoid.space/articles/mltt/mltt.pdf
+   — Pi;
+   — Sigma;
+   — Path.
 
-   Copyright (c) Groupoid Infinity, 2014-2022. -}
+   Copyright (c) Groupoid Infinity, 2014-2023. -}
 
 module mltt where
 import lib/foundations/mltt/pi
 import lib/foundations/mltt/sigma
 import lib/foundations/univalent/path
 
 def MLTT (A : U) : U₁ ≔ Σ
-  (Π-form  : Π (B : A → U), U)
-  (Π-ctor₁ : Π (B : A → U), Pi A B → Pi A B)
-  (Π-elim₁ : Π (B : A → U), Pi A B → Pi A B)
-  (Π-comp₁ : Π (B : A → U) (a : A) (f : Pi A B), Path (B a) (Π-elim₁ B (Π-ctor₁ B f) a) (f a))
-  (Π-comp₂ : Π (B : A → U) (a : A) (f : Pi A B), Path (Pi A B) f (λ (x : A), f x))
-  (Σ-form  : Π (B : A → U), U)
-  (Σ-ctor₁ : Π (B : A → U) (a : A) (b : B a) , Sigma A B)
-  (Σ-elim₁ : Π (B : A → U) (p : Sigma A B), A)
-  (Σ-elim₂ : Π (B : A → U) (p : Sigma A B), B (pr₁ A B p))
-  (Σ-comp₁ : Π (B : A → U) (a : A) (b: B a), Path A a (Σ-elim₁ B (Σ-ctor₁ B a b)))
-  (Σ-comp₂ : Π (B : A → U) (a : A) (b: B a), Path (B a) b (Σ-elim₂ B (a, b)))
-  (Σ-comp₃ : Π (B : A → U) (p : Sigma A B), Path (Sigma A B) p (pr₁ A B p, pr₂ A B p))
-  (=-form  : Π (a : A), A → U)
-  (=-ctor₁ : Π (a : A), Path A a a)
-  (=-elim₁ : Π (a : A) (C: D A) (d: C a a (=-ctor₁ a)) (y: A) (p: Path A a y), C a y p)
-  (=-comp₁ : Π (a : A) (C: D A) (d: C a a (=-ctor₁ a)), Path (C a a (=-ctor₁ a)) d (=-elim₁ a C d a (=-ctor₁ a))), 𝟏
+    (Π-form  : Π (B : A → U), U)
+    (Π-ctor₁ : Π (B : A → U), Pi A B → Pi A B)
+    (Π-elim₁ : Π (B : A → U), Pi A B → Pi A B)
+    (Π-comp₁ : Π (B : A → U) (a : A) (f : Pi A B), Path (B a) (Π-elim₁ B (Π-ctor₁ B f) a) (f a))
+    (Π-comp₂ : Π (B : A → U) (a : A) (f : Pi A B), Path (Pi A B) f (λ (x : A), f x))
+    (Σ-form  : Π (B : A → U), U)
+    (Σ-ctor₁ : Π (B : A → U) (a : A) (b : B a) , Sigma A B)
+    (Σ-elim₁ : Π (B : A → U) (p : Sigma A B), A)
+    (Σ-elim₂ : Π (B : A → U) (p : Sigma A B), B (pr₁ A B p))
+    (Σ-comp₁ : Π (B : A → U) (a : A) (b: B a), Path A a (Σ-elim₁ B (Σ-ctor₁ B a b)))
+    (Σ-comp₂ : Π (B : A → U) (a : A) (b: B a), Path (B a) b (Σ-elim₂ B (a, b)))
+    (Σ-comp₃ : Π (B : A → U) (p : Sigma A B), Path (Sigma A B) p (pr₁ A B p, pr₂ A B p))
+    (=-form  : Π (a : A), A → U)
+    (=-ctor₁ : Π (a : A), Path A a a)
+    (=-elim₁ : Π (a : A) (C: D A) (d: C a a (=-ctor₁ a)) (y: A) (p: Path A a y), C a y p)
+    (=-comp₁ : Π (a : A) (C: D A) (d: C a a (=-ctor₁ a)), Path (C a a (=-ctor₁ a)) d (=-elim₁ a C d a (=-ctor₁ a))), 𝟏
 
--- Theorem. β-rule for pretypes is derivable with generalized transport
+--- Self-aware MLTT:
+--- Theorem. Id β-rule is derivable from generalized transport
 
-theorem internalizing (A : U) : MLTT A ≔
-  (Pi A, lambda A, apply A, Π-β A, Π-η A,
-   Sigma A, pair A, pr₁ A, pr₂ A, Σ-β₁ A, Σ-β₂ A, Σ-η A,
-   Path A, idp A, J A, J-β A, ★)
+def internalizing (A : U)
+  : MLTT A
+ := ( Pi A, lambda A, apply A, Π-β A, Π-η A,
+      Sigma A, pair A, pr₁ A, pr₂ A, Σ-β₁ A, Σ-β₂ A, Σ-η A,
+      Path A, idp A, J A, J-β A,
+      ★
+    )

lib/foundations/mltt/nat.anders

@@ -1,6 +1,7 @@
 {- Natural Numbers: https://anders.groupoid.space/foundations/mltt/nat/
    - Nat.
 
+   HoTT 2.13 Natural Numbers
    HoTT 5.3 W-Types
    HoTT 5.5 Homotopy-inductive types
 

lib/foundations/mltt/sigma.anders

@@ -2,7 +2,8 @@
    - Sigma.
    - Total, Axiom of Choice.
 
-   HoTT 1.5 Product types
+   HoTT 2.6 Cartesian Product
+   HoTT 2.7 Sigma Types
 
    Copyright (c) Groupoid Infinity, 2014-2023. -}
 

lib/foundations/mltt/vec.anders

@@ -1,6 +1,8 @@
 {- Vector Type: https://anders.groupoid.space/foundations/mltt/vec/
    - Vec.
 
+   HoTT 5.7 Generalization of inductive types
+
    Copyright (c) Groupoid Infinity, 2014-2023. -}
 
 module vec where

lib/foundations/modal/infinitesimal.anders

@@ -1,9 +1,9 @@
-{- The modality of shape infinitesimal: https://anders.groupoid.space/foundations/modal/infinitesimal/
-   - \Im modality type.
+{- Im: https://anders.groupoid.space/foundations/modal/infinitesimal/
+   — Im modality of shape infinitesimal.
 
    HoTT 7.7 Modalities
 
-   Copyright (c) Groupoid Infinity, 2014-2022. -}
+   Copyright (c) Groupoid Infinity, 2014-2023. -}
 
 module infinitesimal where
 import lib/foundations/univalent/path

lib/foundations/univalent/equiv.anders

@@ -2,11 +2,14 @@
    — Fibers;
    — Contractability of Fibers and Singletons;
    — Equivalence;
-   — Surjective, Injective, Embedding, Hae;
+   — Surjective, Injective, Embedding
+   - Half-adjoint equivalence;
    — Univalence;
    — Theorems, Gluing.
 
+   HoTT 2.10 Universes and univalence axiom
    HoTT 4.2.4 Fiber
+   HoTT 4.4 Contractible Fibers
    HoTT 4.6 Surjections and Embedding
    HoTT 5.8.5 Equivalence Induction
 

lib/foundations/univalent/extensionality.anders

@@ -1,9 +1,10 @@
-{- FunExt Type: https://anders.groupoid.space/foundations/univalent/funext
+{- FunExt: https://anders.groupoid.space/foundations/univalent/funext
    — Homotopy;
    — Identity System;
    — Function Extensionality;
    — FunExt as Isomorphism.
 
+   HoTT 2.4 Homotopies and equivalence
    HoTT 2.9 Pi-types and the function extensionality axiom
 
    Copyright (c) Groupoid Infinity, 2014-2023. -}

lib/foundations/univalent/iso.anders

@@ -5,7 +5,7 @@
 
    HoTT 2.4 Homotopies and equivalences
 
-   Copyright (c) Groupoid Infinity, 2014-2022. -}
+   Copyright (c) Groupoid Infinity, 2014-2023. -}
 
 module iso where
 import lib/foundations/univalent/path

lib/foundations/univalent/path.anders

@@ -1,4 +1,4 @@
-{- Path Type: https://anders.groupoid.space/foundations/univalent/path
+{- Path: https://anders.groupoid.space/foundations/univalent/path
    - Path Equality;
    - Computational properties;
    - Interval and De Morgan laws;
@@ -11,6 +11,7 @@
    HoTT 1.12.1 Path induction
    HoTT 2.1 Types are higher groupoids
    HoTT 2.11 Identity type
+   HoTT 2.2 Functions are functors
    HoTT 3.11 Contractibility
    HoTT 5.8 Identity types and identity systems
    HoTT 6.2 Induction principles and dependent paths.

lib/foundations/univalent/prop.anders

@@ -1,3 +1,11 @@
+{- Proposition: https://anders.groupoid.space/foundations/univalent/prop
+   - Prop type.
+
+   HoTT 3.3 Mere Proposition
+   HoTT 3.4 Classical vs. intuitionistic logic
+
+   Copyright (c) Groupoid Infinity, 2014-2023. -}
+
 module prop where
 import lib/foundations/univalent/path
 import lib/foundations/mltt/sigma