diff --git a/Plan.org b/Plan.org index 734dad3..1e8cd13 100644 --- a/Plan.org +++ b/Plan.org @@ -6,7 +6,7 @@ ** 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 + - Big-ass-boss: Loop space of S^1 = Z - Try to balance hiding cubical implementations whilst exploiting their advantages ** Barriers @@ -76,3 +76,13 @@ + 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 + + +** Minibosses +- _+_ unique on the naturals + + axiomatize addition on naturals + + naturals is a set + + fun extensionality + + contractability + + propositions + + propositions closed under sigma types diff --git a/Trinitarianism/Quest0Preamble.agda b/Trinitarianism/Preambles/P0.agda similarity index 57% rename from Trinitarianism/Quest0Preamble.agda rename to Trinitarianism/Preambles/P0.agda index 95c03ec..b00cdb3 100644 --- a/Trinitarianism/Quest0Preamble.agda +++ b/Trinitarianism/Preambles/P0.agda @@ -1,3 +1,3 @@ -module Trinitarianism.Quest0Preamble where +module Trinitarianism.Preambles.P0 where open import Cubical.Core.Everything hiding (_∨_) public diff --git a/Trinitarianism/Preambles/P1.agda b/Trinitarianism/Preambles/P1.agda new file mode 100644 index 0000000..c80ca6f --- /dev/null +++ b/Trinitarianism/Preambles/P1.agda @@ -0,0 +1,6 @@ +module Trinitarianism.Preambles.P1 where + +open import Cubical.Core.Everything public +open import Cubical.Data.Unit public renaming (Unit to ⊤) +open import Cubical.Data.Empty public using (⊥) +open import Cubical.Data.Nat public hiding (isEven) diff --git a/Trinitarianism/Preambles/P2.agda b/Trinitarianism/Preambles/P2.agda new file mode 100644 index 0000000..3cdcc62 --- /dev/null +++ b/Trinitarianism/Preambles/P2.agda @@ -0,0 +1,5 @@ +module Trinitarianism.Preambles.P2 where + +open import Cubical.Core.Everything public +open import Cubical.Data.Nat public hiding (_+_ ; isEven) +open import Trinitarianism.Quest1Solutions public diff --git a/Trinitarianism/Quest0.agda b/Trinitarianism/Quest0.agda index 72b5ce8..c7a4575 100644 --- a/Trinitarianism/Quest0.agda +++ b/Trinitarianism/Quest0.agda @@ -1,5 +1,5 @@ module Trinitarianism.Quest0 where -open import Trinitarianism.Quest0Preamble +open import Trinitarianism.Preambles.P0 data ⊤ : Type where tt : ⊤ diff --git a/Trinitarianism/Quest0.md b/Trinitarianism/Quest0.md index 375c1b1..be77259 100644 --- a/Trinitarianism/Quest0.md +++ b/Trinitarianism/Quest0.md @@ -59,8 +59,10 @@ TrueToTrue = {!!} and you need to give a p/r/g.e. of `⊤` - you can give it a p/r/g.e. of `⊤` and press `C-c C-SPC` to fill the hole -There is more than one proof (see solutions) - are they the same? -Here is an important one: +There is more than one proof (see solutions) - are they 'the same'? +What is 'the same'? + +Here is an important solution: ```agda TrueToTrue' : ⊤ → ⊤ diff --git a/Trinitarianism/Quest0Solutions.agda b/Trinitarianism/Quest0Solutions.agda index decb41d..45fddad 100644 --- a/Trinitarianism/Quest0Solutions.agda +++ b/Trinitarianism/Quest0Solutions.agda @@ -1,5 +1,5 @@ module Trinitarianism.Quest0Solutions where -open import Trinitarianism.Quest0Preamble +open import Trinitarianism.Preambles.P0 data ⊤ : Type where diff --git a/Trinitarianism/Quest1.agda b/Trinitarianism/Quest1.agda index 6f1fa15..2b10192 100644 --- a/Trinitarianism/Quest1.agda +++ b/Trinitarianism/Quest1.agda @@ -1,7 +1,6 @@ module Trinitarianism.Quest1 where -open import Cubical.Core.Everything -open import Cubical.Data.Nat hiding (isEven) +open import Trinitarianism.Preambles.P1 isEven : ℕ → Type isEven n = {!!} diff --git a/Trinitarianism/Quest1.md b/Trinitarianism/Quest1.md index f3e1652..38af238 100644 --- a/Trinitarianism/Quest1.md +++ b/Trinitarianism/Quest1.md @@ -1,4 +1,4 @@ -# Dependent Types +# Dependent Types and Sigma Types In a 'place to do maths' we would like to be able to express and 'prove' @@ -84,6 +84,7 @@ There are three interpretations of `isEven : ℕ → Type`. i.e. an object in the over-category `Type↓ℕ`. Pictorially, it looks like + isEven @@ -92,6 +93,9 @@ There are three interpretations of `isEven : ℕ → Type`. `isEven n` is called the _fiber over `n`_. In this particular example the fibers are either empty or singleton. + +In general given a type `A : Type`, +a _dependent type over `A`_ is a term of type `A → Type`. You can check if `2` is even by asking agda to 'normalize' it: do `C-c C-n` (`n` for normalize) and type in `isEven 2`. @@ -140,6 +144,17 @@ where `a : A` and `b : B a`. There are two ways of using a term in a sigma type. We can extract the first part using `fst` or the second part using `snd`. +Given `x : Σ A B` there are three interpretations of `fst` and `snd`: +- Viewing `x` as a proof of existence + `fst x` provides the witness of existence and `snd` provides the proof + of the property +- Viewing `x` as a recipe `fst` extracts the first component and + `snd` extracts the second component +- Viewing `x` as a point in the total space of a bundle + `fst x` is the point that `x` is over in the base space and `snd x` + is the point in the fiber that `x` represents. + In particular you can interpret `fst` as projection from the total space + to the base space, collapsing fibers. For example to define a map that takes an even natural and divides it by two we can ```agda @@ -147,7 +162,7 @@ div2 : Σ ℕ isEven → ℕ div2 x = ? ``` - Load the file, go to the hole and case on `x` - (you might want to rename `fst₁` and `snd₁`). + (you might want to rename `fst₁` and `snd₁`). ```agda div2 : Σ ℕ isEven → ℕ div2 (fst₁ , snd₁) = {!!} @@ -174,3 +189,4 @@ since if they were `div2 (2 , tt)` would be 'the same' `div2 (36/2 , tt)`, hence `1` would be 'the same' as `18`. > Are they 'the same'? What is 'the same'? + diff --git a/Trinitarianism/Quest1Solutions.agda b/Trinitarianism/Quest1Solutions.agda index 74a09dc..b158b69 100644 --- a/Trinitarianism/Quest1Solutions.agda +++ b/Trinitarianism/Quest1Solutions.agda @@ -1,9 +1,6 @@ module Trinitarianism.Quest1Solutions where -open import Cubical.Core.Everything -open import Cubical.Data.Unit renaming (Unit to ⊤) -open import Cubical.Data.Empty -open import Cubical.Data.Nat hiding (isEven) +open import Trinitarianism.Preambles.P1 isEven : ℕ → Type isEven zero = ⊤ diff --git a/Trinitarianism/Quest2.agda b/Trinitarianism/Quest2.agda new file mode 100644 index 0000000..c2de761 --- /dev/null +++ b/Trinitarianism/Quest2.agda @@ -0,0 +1,9 @@ +module Trinitarianism.Quest2 where + +open import Trinitarianism.Preambles.P2 + +_+_ : ℕ → ℕ → ℕ +n + m = {!!} + +SumOfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst + y .fst) +SumOfEven x y = {!!} diff --git a/Trinitarianism/Quest2.md b/Trinitarianism/Quest2.md new file mode 100644 index 0000000..728d49a --- /dev/null +++ b/Trinitarianism/Quest2.md @@ -0,0 +1,64 @@ +# Pi Types + +We will try to formulate and prove the statement +> The sum of two even naturals is even. +To do so we must define `+` on the naturals. +Addition takes in two naturals and spits out a +natural, so it should have type `ℕ → ℕ → ℕ`. +```agda +_+_ : ℕ → ℕ → ℕ +n + m = ? +``` +Agda supports the notation `_+_` (without spaces) +which means from now on you can write `0 + 1` +and so on (with spaces). +Try coming up with a sensible definition yourself, +it may not look exactly like ours. +
+ Hint + `n + 0` should be `n` and `n + (m + 1)` should be `(n + m) + 1` +
+ +Now we can make the statement: +```agda +SumOfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst + y .fst) +SumOfEven x y = ? +``` +> Tip: `x .fst` is another notation for `fst x`. +> This works for all sigma types. +There are three ways to interpret this: +- For all even naturals `x` and for all even naturals `y`, + their sum is even. +- `isEven (x .fst + y .fst)` is a construction depending on two recipes + `x` and `y`. + Given two recipes `x` and `y` of `Σ ℕ isEven`, + we break them down into their first components, + apply the conversion `_+_`, + and form a recipe for `isEven` of the result. +- `isEven (_ .fst + _ .fst)` is a bundle over the categorical product + `Σ ℕ isEven × Σ ℕ isEven` and `SumOfEven` is a _section_ of the bundle. + +More generally given `A : Type` and `B : A → Type` we can form the _pi type_ +`(x : A) → B x : Type` (in other languages `Π (x : ℕ), isEven n`). +The notation suggests that these behave like functions, +and indeed in the special case where the fiber is constant +with respect to the base a section is just a term of type `A → B`, +i.e. a function. Hence pi types are also known as +_dependent function types_. + +We are now in a position to prove the statement. Have fun! + +_Important_: Once you have proven the statement, +check out our two ways of defining addition `_+_` and `_+'_` +(in the solutions). +Use `C-c C-n` to check that they compute the same values +on different examples. +Uncomment the code for `Sum'OfEven` in the solutions, +it is just `SumOfEven` but with `+`s changed for `+'`s. +Load the file. Does the proof still work? + +In our proof of `SumOfEven` we explicitely used the definition of `_+_`, +which means that if we wanted to use our proof on someone else's +definition of addition, things might break. +> But `_+_` and `_+'_` compute the same values. +> Are `_+_` and `_+'_` 'the same'? What is 'the same'? diff --git a/Trinitarianism/Quest2Solutions.agda b/Trinitarianism/Quest2Solutions.agda new file mode 100644 index 0000000..56f3250 --- /dev/null +++ b/Trinitarianism/Quest2Solutions.agda @@ -0,0 +1,23 @@ +module Trinitarianism.Quest2Solutions where + +open import Trinitarianism.Preambles.P2 + +_+_ : ℕ → ℕ → ℕ +n + zero = n +n + suc m = suc (n + m) + +_+'_ : ℕ → ℕ → ℕ +zero +' n = n +suc m +' n = suc (m +' n) + +SumOfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst + y .fst) +SumOfEven x (zero , hy) = x .snd +SumOfEven x (suc (suc y) , hy) = SumOfEven x (y , hy) + +{- + +Sum'OfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst +' y .fst) +Sum'OfEven x (zero , hy) = x .snd +Sum'OfEven x (suc (suc y) , hy) = Sum'OfEven x (y , hy) + +-} diff --git a/_build/2.6.2/agda/Trinitarianism/Preambles/P0.agdai b/_build/2.6.2/agda/Trinitarianism/Preambles/P0.agdai new file mode 100644 index 0000000..6ccb441 Binary files /dev/null and b/_build/2.6.2/agda/Trinitarianism/Preambles/P0.agdai differ diff --git a/_build/2.6.2/agda/Trinitarianism/Preambles/P1.agdai b/_build/2.6.2/agda/Trinitarianism/Preambles/P1.agdai new file mode 100644 index 0000000..d4d2fc9 Binary files /dev/null and b/_build/2.6.2/agda/Trinitarianism/Preambles/P1.agdai differ diff --git a/_build/2.6.2/agda/Trinitarianism/Preambles/P2.agdai b/_build/2.6.2/agda/Trinitarianism/Preambles/P2.agdai new file mode 100644 index 0000000..37e8e37 Binary files /dev/null and b/_build/2.6.2/agda/Trinitarianism/Preambles/P2.agdai differ diff --git a/_build/2.6.2/agda/Trinitarianism/Quest0Solutions.agdai b/_build/2.6.2/agda/Trinitarianism/Quest0Solutions.agdai index 10f54e5..84a548e 100644 Binary files a/_build/2.6.2/agda/Trinitarianism/Quest0Solutions.agdai and b/_build/2.6.2/agda/Trinitarianism/Quest0Solutions.agdai differ diff --git a/_build/2.6.2/agda/Trinitarianism/Quest1Solutions.agdai b/_build/2.6.2/agda/Trinitarianism/Quest1Solutions.agdai index fc48c05..70eb87e 100644 Binary files a/_build/2.6.2/agda/Trinitarianism/Quest1Solutions.agdai and b/_build/2.6.2/agda/Trinitarianism/Quest1Solutions.agdai differ diff --git a/_build/2.6.2/agda/Trinitarianism/Quest2.agdai b/_build/2.6.2/agda/Trinitarianism/Quest2.agdai new file mode 100644 index 0000000..6d7bec3 Binary files /dev/null and b/_build/2.6.2/agda/Trinitarianism/Quest2.agdai differ diff --git a/_build/2.6.2/agda/Trinitarianism/Quest2Solutions.agdai b/_build/2.6.2/agda/Trinitarianism/Quest2Solutions.agdai new file mode 100644 index 0000000..207b804 Binary files /dev/null and b/_build/2.6.2/agda/Trinitarianism/Quest2Solutions.agdai differ