Trinitarianism, Types as Props

Plan.md

@@ -19,9 +19,9 @@
 - References to Harper lectures and HoTT book
 
 # Content
- <!-- listing topics we have pursued, NO ordering -->
+<!-- listing topics we have pursued, NO ordering -->
 - emacs usage
-  - `data` and `record`
+- agda usage
   - basic commands (all covered in https://agda.readthedocs.io/en/v2.6.0.1/getting-started/quick-guide.html)
   - recommend doom emacs? -> basic doom usage and command differences with nude agda.
   - implicit/explicit arguments
@@ -29,24 +29,29 @@
   - `_+_` and `plus__`
 - type theory basics
   - meta (judgemental/definitional) equality vs internal (propositional) equality
-  - constructing types in universes
+    - function extensionality
+  - type formation
   - universes
   - recursors / pattern matching
-  - side quest: some natural number exercises as early evidence of being able to 'do maths'?
+  - (side Q) some natural number exercises as early evidence of being able to 'do maths'?
   - different notions of equivalence
     a) fibers contractable
     b) quasi-inverse
     c) zig-zag
-  - types are infinity groupoids
-  - positive and negative constructions of Pi/Sigma types
+  - (side Q) types are infinity groupoids
+  - inductive types
+    - (side Q) positive and negative constructions of Pi/Sigma types
+    - `data` and `record`
 - HoTT
   - basics
     a) meta interval, identity type vs path type
+      - mention identity type for compatability with other sources, but just use path type
     b) path type on other types
     c) dependent path type PathP vs path over
     d) univalence
     e) the (non)-issue of J in (Cu)TT
     f) isContr, isProp, isSet
+    g) drawing pictures
   - Structures, univalence and transport
     a) transporting results between isomorphic structures
   - HITs, examples
@@ -58,7 +63,7 @@
     a) homotopy levels being closed under type constructions, in particular Set and ETT inside HoTT
        * in particular sigma types
 
-## Debriefs
+# Debriefs
 - 2021 July 15; Homotopy n-types
   - watched (Harper) lecture 15 on Sets being closed under type formations ->- motivates showing in Agda Sets closed under Sigma.
   - Harper does product case, claiming sigma case follows analogously,

Plan.org

@@ -0,0 +1,73 @@
+# Planning The HoTT Game
+
+## Aims of the HoTT Game
+- To get mathematicians with no experience in proof verification interested in HoTT and able to use Agda for HoTT
+- [?] Work towards showing an interesting result in HoTT
+- Try to balance hiding cubical implementations whilst exploiting their advantages
+
+## Barriers
+- HOLD Installation of emacs
+- TODO Usage of emacs
+- TODO General type theoretic foundations
+- TODO Cubical type theory
+
+## Format
+- [?] Everything done in .agda files
+- Partially written code with spaces for participants to fill in + answer files
+- Levels set out with mini-bosses like in Nat Num Game, but with an overall boss
+- [?] Side quests
+- References to Harper lectures and HoTT book
+
+# Content
+<!-- listing topics we have pursued, NO ordering -->
+- emacs usage
+- agda usage
+  - basic commands (all covered in https://agda.readthedocs.io/en/v2.6.0.1/getting-started/quick-guide.html)
+  - recommend doom emacs? -> basic doom usage and command differences with nude agda.
+  - implicit/explicit arguments
+  - holes and inferred types
+  - `_+_` and `plus__`
+- type theory basics
+  - meta (judgemental/definitional) equality vs internal (propositional) equality
+    - function extensionality
+  - type formation
+    - inductive types
+      - (side Q) positive and negative constructions of Pi/Sigma types
+      - `data` and `record`
+  - universes
+  - recursors / pattern matching
+  - (side Q) some natural number exercises as early evidence of being able to 'do maths'?
+  - different notions of equivalence
+    a) fibers contractable
+    b) quasi-inverse
+    c) zig-zag
+  - (side Q) types are infinity groupoids
+  - extra paths (univalence, fun ext, HITs)
+- HoTT
+  - basics
+    a) meta interval, identity type vs path type
+       - mention identity type for compatability with other sources, but just use path type
+    b) path type on other types
+    c) dependent path type PathP vs path over
+    d) univalence
+    e) the (non)-issue of J in (Cu)TT
+    f) isContr, isProp, isSet
+    g) drawing pictures
+  - Structures, using univalence to transport
+    a) transporting results between isomorphic structures
+  - HITs, examples
+    a) the constructed interval
+    b) booleans and covers
+    c) S^n
+    d) S^1 with 2 cw structures equiv
+  - Homotopy n-types
+    a) homotopy levels being closed under type constructions, in particular Set and ETT inside HoTT
+       * in particular sigma types
+
+# Debriefs
+- 2021 July 15; Homotopy n-types
+  - watched (Harper) lecture 15 on Sets being closed under type formations ->- motivates showing in Agda Sets closed under Sigma.
+  - Harper does product case, claiming sigma case follows analogously,
+  - attempt proof in Cubical Agda but highly non-obvious how to use that fibers are Sets.
+  - difficulty is that PathP not in one fiber, but PathOver is, AND PathOver <-> PathP NON-obvious
+  - Easy to generalize situation to n-types being closed under Sigma (7.1.8 in HoTT book), we showed this assuming PathPIsoPath

Trinitarianism/AsCats.agda

@@ -0,0 +1,15 @@
+module TheHoTTGame.Trinitarianism.AsCats where
+
+{-
+  Here are some things that we could like to have in a category
+  (in which we want to do maths e.g. the category of sets)
+  * Initial objects (empty set)
+  * Terminal objects (singleton)
+  * Sums
+  * Products
+  * Cartesian closed (for two objects A B, maps A → B
+    are also an object in the category)
+  * Natural numbers object (the natural numbers ℕ in Set)
+  * and maybe more
+
+-}

Trinitarianism/AsProps/Quest0.agda

@@ -0,0 +1,216 @@
+module TheHoTTGame.Trinitarianism.AsProps.Quest0 where
+open import TheHoTTGame.Trinitarianism.AsProps.Quest0Preamble
+
+{-
+  Here are some things that we could like to have in a logical framework
+  * Propositions (with the data of proofs)
+  * Objects to reason about with propositions
+
+  To make propositions we want
+  * False ⊥
+  * True ⊤
+  * Or ∨
+  * And ∧
+  * Implication →
+
+  but propositions are useless if they're not talking about anything,
+  so we also want
+  * Predicates
+  * Exists ∃
+  * For all ∀
+  * Equality ≡ (of objects)
+-}
+
+-- Here is how we define 'true'
+data ⊤ : Prop where
+  trivial : ⊤
+
+{- It reads '⊤ is a proposition and there is a proof of it, called "trivial"'. -}
+
+-- Here is how we define 'false'
+data ⊥ : Prop where
+
+{- This says that ⊥ is the proposition where there are no proofs of it. -}
+
+{-
+Given two propositions P and Q, we can form a new proposition 'P implies Q'
+written P → Q
+To introduce a proof of P → Q we assume a proof x of P and give a proof y of Q
+
+Here is an example demonstrating → in action
+-}
+
+TrueToTrue : ⊤ → ⊤
+TrueToTrue = ?
+
+{-
+  * press C-c C-l (this means Ctrl-c Ctrl-l) to load the document,
+    and now you can fill the holes
+  * navigate to the hole { } using C-c C-f (forward) or C-c C-b (backward)
+  * press C-c C-r and agda will try to help you (r for refine)
+  * you should see λ x → { }
+  * navigate to the new hole
+  * C-c C-, to check what agda wants in the hole (C-c C-comma)
+  * the Goal area should look like
+
+  Goal: ⊤
+  ————————————————————————————————————————————————————————————
+  x : ⊤
+
+  * this means you have a proof of ⊤ 'x : ⊤' and you need to give a proof of ⊤
+  * you can now give it a proof of ⊤ and press C-c C-SPC to fill the hole
+
+  There is more than one proof (see solutions) - are they the same?
+-}
+
+{-
+Let's assume we have the following the naturals ℕ
+and try to define the 'predicate on ℕ' given by 'x is 0'
+-}
+isZero : ℕ → Prop
+isZero zero = ?
+isZero (suc n) = ?
+
+{-
+Here's how:
+  * when x is zero, we give the proposition ⊤
+  (try typing it in by writing \top then pressing C-c C-SPC)
+  * when x is suc n (i.e. 'n + 1', suc for successor) we give ⊥ (\bot)
+This is technically using induction - see AsTypes.
+
+In general a 'predicate on ℕ' is just a 'function' P : ℕ → Prop
+-}
+
+{-
+You can check if zero is indeed zero by clicking C-c C-n,
+which brings up a thing on the bottom saying 'Expression',
+and you can type the following
+isZero zero
+isZero (suc zero)
+isZero (suc (suc zero))
+...
+-}
+
+{-
+We can prove that 'there exists a natural number that isZero'
+in set theory we might write
+  ∃ x ∈ ℕ, x = 0
+which in agda noation is
+  Σ ℕ isZero
+
+In general if we have predicate P : ℕ → Prop we would write
+  Σ ℕ P
+for
+  ∃ x ∈ ℕ, P x
+
+To formulate the result Σ ℕ isZero we need to define
+a proof of it
+-}
+ExistsZero : Σ ℕ isZero
+ExistsZero = ?
+
+{-
+To fill the hole, we need to give a natural and a proof that it is zero.
+Agda will give the syntax you need:
+  * navigate to the correct hole then refine using C-c C-r
+  * there are now two holes - but which is which?
+  * navigate to the first holes and type C-c C-,
+    - for the first hole it will ask you to give it a natural 'Goal: ℕ'
+    - for the second hole it will ask you for a proof that
+    whatever you put in the first hole is zero 'Goal: isZero ?0' for example
+  * try to fill both holes, using C-c C-SPC as before
+  * for the second hole you can try also C-c C-r,
+    Agda knows there is an obvious proof!
+-}
+
+{-
+Let's show 'if all natural numbers are zero then we have a contradiction',
+where 'a contradiction' is a proof of ⊥.
+In maths we would write
+  (∀ x ∈ ℕ, x = 0) → ⊥
+and the agda notation for this is
+  ((x : ℕ) → isZero x) → ⊥
+
+In general if we have a predicate P : ℕ → Prop then we write
+  (x : ℕ) → P x
+to mean
+  ∀ x ∈ ℕ, P x
+-}
+
+AllZero→⊥ : ((x : ℕ) → isZero x) → ⊥
+AllZero→⊥ = ?
+
+{-
+Here is how we prove it in maths
+  * assume hypothesis h, a proof of (x : ℕ) → isZero x
+  * apply the hypothesis h to 1, deducing isZero 1, i.e. we get a proof of isZero 1
+  * notice isZero 1 IS ⊥
+
+Here is how you can prove it here
+  * navigate to the hole and check the goal
+  * to assume the hypothesis (x : ℕ) → isZero x,
+    type an h in front like so
+    AllZero→⊥ h = { }
+  * now do
+    * C-c C-l to load the file
+    * navigate to the new hole and check the new goal
+  * type h in the hole, type C-c C-r
+  * this should give h { }
+  * navigate to the new hole and check the Goal
+  * Explanation
+    * (h x) is a proof of isZero x for each x
+    * it's now asking for a natural x such that isZero x is ⊥
+  * Try filling the hole with 0 and 1 and see what Agda says
+-}
+
+{-
+Let's try to show the mathematical statement
+'any natural n is 0 or not'
+but we need a definition of 'or'
+-}
+data OR (P Q : Prop) : Prop where
+  left : P → OR P Q
+  right : Q → OR P Q
+{-
+This reads
+  * Given propositions P and Q we have another proposition P or Q
+  * There are two ways of proving P or Q
+    * given a proof of P, left sends this to a proof of P or Q
+    * given a proof of Q, right sends this to a proof of P or Q
+
+Agda supports nice notation using underscores.
+-}
+
+data _∨_ (P Q : Prop) : Prop where
+  left : P → P ∨ Q
+  right : Q → P ∨ Q
+
+{-
+[Important note]
+Agda is sensitive to spaces so these are bad
+
+data _ ∨ _ (P Q : Prop) : Prop where
+  left : P → P ∨ Q
+  right : Q → P ∨ Q
+
+data _∨_ (P Q : Prop) : Prop where
+  left : P → P∨Q
+  right : Q → P∨Q
+
+it is also sensitive to indentation so these are also bad
+
+data _∨_ (P Q : Prop) : Prop where
+left : P → P ∨ Q
+right : Q → P ∨ Q
+
+-}
+
+{-
+Now we can prove it!
+This technically uses induction - see AsTypes.
+Fill the missing part of the theorem statement.
+You need to first uncomment this by getting rid of the -- in front (C-x C-;)
+-}
+-- DecidableIsZero : (n : ℕ) → {!!}
+-- DecidableIsZero zero = {!!}
+-- DecidableIsZero (suc n) = {!!}

Trinitarianism/AsProps/Quest0Preamble.agda

@@ -0,0 +1,12 @@
+
+module TheHoTTGame.Trinitarianism.AsProps.Quest0Preamble where
+
+open import Cubical.Core.Everything hiding (_∨_) public
+open import Cubical.Data.Nat public
+
+private
+  postulate
+    u : Level
+
+Prop = Type u
+

Trinitarianism/AsProps/Quest0Solutions.agda

@@ -0,0 +1,39 @@
+module TheHoTTGame.Trinitarianism.AsProps.Quest0Solutions where
+open import TheHoTTGame.Trinitarianism.AsProps.Quest0Preamble
+
+data ⊤ : Prop where
+  trivial : ⊤
+
+data ⊥ : Prop where
+
+TrueToTrue : ⊤ → ⊤
+TrueToTrue = λ x → x
+
+TrueToTrue' : ⊤ → ⊤
+TrueToTrue' x = x
+
+TrueToTrue'' : ⊤ → ⊤
+TrueToTrue'' trivial = trivial
+
+TrueToTrue''' : ⊤ → ⊤
+TrueToTrue''' x = trivial
+
+isZero : ℕ → Prop
+isZero zero = ⊤
+isZero (suc n) = ⊥
+
+ExistsZero : Σ ℕ isZero
+ExistsZero = zero , trivial
+
+AllZero→⊥ : ((x : ℕ) → isZero x) → ⊥
+AllZero→⊥ h = h 1
+
+data _∨_ (P Q : Prop) : Prop where
+  left : P → P ∨ Q
+  right : Q → P ∨ Q
+
+DecidableIsZero : (n : ℕ) → (isZero n) ∨ (isZero n → ⊥)
+DecidableIsZero zero = left trivial
+DecidableIsZero (suc n) = right (λ x → x)
+
+

Trinitarianism/AsProps/Trash/Qust0.agda

@@ -0,0 +1,31 @@
+{- This says that ⊥ is the proposition where there are no proofs of it. -}
+
+{-
+Given two propositions P and Q, we can form a new proposition 'P implies Q'
+written P → Q
+To introduce a proof of P → Q we assume a proof x of P and give a proof y of Q
+
+Here is an example demonstrating → in action
+-}
+-- TrueToTrue : ⊤ → ⊤
+-- TrueToTrue = ?
+
+{-
+  * press C-c C-l (this means Ctrl-c Ctrl-l) to load the document,
+    and now you can fill the holes
+  * press C-c C-r and agda will try to help you,
+  * you should see λ x → { }
+  * navigate to the hole { } using C-c C-f (forward) or C-c C-b (backward)
+  * to check what agda wants in the hole use C-c C-,
+  * the Goal area should look like
+  Goal: ⊤
+  ————————————————————————————————————————————————————————————
+  x : ⊤
+
+  * this means you have a proof x : ⊤ and you need to give a proof of ⊤
+  * you can now give it a proof of ⊤ and press C-c C-SPC to fill the hole
+
+  There is more than one proof (see answers) - are they the same?
+-}
+
+-- solutions:

Trinitarianism/AsProps2.agda

@@ -0,0 +1,13 @@
+{-
+Two things being equal is also a proposition
+
+-}
+
+
+
+
+-- FalseToTrue : ⊥ → ⊤
+-- FalseToTrue = λ x → trivial
+
+-- FalseToTrue' : ⊥ → ⊤
+-- FalseToTrue' ()