{-# OPTIONS --cubical --allow-unsolved-metas #-} open import Cubical.Core.Everything data ⊥ : Set where data ℕ : Set where zero : ℕ succ : ℕ → ℕ _+_ : ℕ → ℕ → ℕ zero + b = b succ a + b = succ (a + b) one = succ zero two = succ (succ zero) -- the type of ordered pairs of natural numbers data Pair : Set where mk : ℕ → ℕ → Pair -- the type of unordered pairs of natural numbers data UnorderedPair : Set where mk : ℕ → ℕ → UnorderedPair swap : {a b : ℕ} → mk a b ≡ mk b a ex : Pair ex = mk one two ex' : Pair ex' = mk two one unordered-ex : UnorderedPair unordered-ex = mk one two unordered-ex' : UnorderedPair unordered-ex' = mk two one _ : unordered-ex ≡ unordered-ex' _ = swap unordered-sum : UnorderedPair → ℕ unordered-sum (mk a b) = a + b unordered-sum (swap i) = {!!} -- with unordered pairs, the following function should NOT be implementable, and indeed, it isn't first : UnorderedPair → ℕ first (mk a b) = a first (swap i) = {!!} -- In standard Agda, we picture data types as collections of points. -- In Cubical Agda, we picture data types as spaces. data ℤmod4 : Set where zer : ℤmod4 suc : ℤmod4 → ℤmod4 loop : zer ≡ suc (suc (suc (suc zer))) -- A picture of ℤmod4: -- * * * * * * * ... -- v | ^ ^ -- +-->--->---->---->--+ | -- | loop ^ -- | | -- v | -- +--->---->--->--->--+ cong : {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y cong = {!!} _ : suc zer ≡ suc (suc (suc (suc (suc zer)))) _ = cong suc loop data Circle : Set where north : Circle loop : north ≡ north {- cubical/homotopy type theory unlocks a Rosetta stone between - logic - computation - homotopy theory logic computation homotopy theory -------------------------------------------------------------------------------------------------------------------------------- p : x ≡ y proof of the statement that x equals y witness that x equals y path from x to y f : X → Y function algorithm map between the space X and the space Y ⊥ falsity the empty data type the empty space X set type space (up to deformation) -} data ℤ : Set where _⊝_ : ℕ → ℕ → ℤ -- \o- \ominus -- interpretation: 2 ⊝ 5 means: I have 2 €, but I owe 5 €. (So, in total, I have -3 €.) -- 3 ⊝ 6 menas: I have 3 €, but I owe 6 €. (So, in total, I have -3 €.) cancel : (a b : ℕ) → a ⊝ b ≡ succ a ⊝ succ b succℤ : ℤ → ℤ succℤ (a ⊝ b) = succ a ⊝ b succℤ (cancel a b i) = {!!} _+ℤ_ : ℤ → ℤ → ℤ (a ⊝ b) +ℤ (a' ⊝ b') = (a + a') ⊝ (b + b') (x ⊝ x₁) +ℤ cancel a b i = {!!} cancel a b i +ℤ z' = {!!} -- Indeed, in Cubical Agda, the type "x ≡ y" can not only (as usual) be read -- as the type of witnesses that x and y are the same, but it can also be read -- as the type of paths from x to y. -- Figure 8: -- +---+ +---+ -- / \ / \ -- + + + -- \ / \ / -- +---+ +---+ data Figure8 : Set where center : Figure8 loop₁ : center ≡ center loop₂ : center ≡ center -- +---+ -- |###| -- |###| -- +---+ data FilledSquare : Set where upper-left-corner : FilledSquare lower-right-corner : FilledSquare {- with just these constructors, the type looks as follows: * * -} path₁ : upper-left-corner ≡ lower-right-corner {- with just these constructors, the type looks as follows: *->-+ v * -} path₂ : upper-left-corner ≡ lower-right-corner {- with just these constructors, the type looks as follows: *->-+ v v +->-* -} filling : path₁ ≡ path₂ -- logical reading: for any set/type X, for any element x : X, it is the case that x equals x. -- computational reading: "refl" is a function which inputs a set/type X and an element x : X, and outputs a witness that x equals x. -- homotopical reading: for any space X, for any point x : X, there is a path from x to x. refl : (X : Set) (x : X) → x ≡ x refl X x = λ i → x symm : (X : Set) (x y : X) → x ≡ y → y ≡ x symm X x y p = λ i → p (~ i) -- in blackboard mathematics: p (1 - i) -- A path γ in a type X is, internally in Cubical Agda, formalized as a function from I to X, where I is the unit interval. -- -- * γ 0 * γ 1 -- \ ^ γ 0.9 -- +---+ γ 0.3 | -- \ | -- +-->-->-->-+ -- γ 0.5 {- open import Padova2024.EquationalReasoning -- ex and ex' are NOT the same: lemma : ex ≡ ex' → ⊥ lemma () -} -- How can we define the type of unordered pairs of natural numbers? -- Then ex and ex' would be the same. -- Option 1: just reuse the type Pair of ordered pairs, and promise -- to ourselves that we will never make us of the accidental ordering -- Option 2: use sorted pairs data _≤_ : ℕ → ℕ → Set where base : {b : ℕ} → zero ≤ b step : {a b : ℕ} → a ≤ b → succ a ≤ succ b data OrderedPair : Set where mk : (a b : ℕ) → a ≤ b → OrderedPair data _⊎_ (X Y : Set) : Set where left : X → X ⊎ Y right : Y → X ⊎ Y _≤?_ : (a b : ℕ) → (a ≤ b) ⊎ (b ≤ a) x ≤? y = {!!} -- a "smart constructor" mk' : ℕ → ℕ → OrderedPair mk' a b with a ≤? b ... | left a≤b = mk a b a≤b ... | right b≤a = mk b a b≤a {- _ : mk' one two ≡ mk' two one _ = refl -} -- Option 3: setoid hell data _×_ (X Y : Set) : Set where _,_ : X → Y → X × Y {- _≈_ : Pair → Pair → Set mk a b ≈ mk a' b' = ((a ≡ a') × (b ≡ b')) ⊎ ((a ≡ b') × (b ≡ a')) _ : ex ≈ ex' _ = right (refl , refl) -} -- A setoid is a type together with a custom equivalence relation on it -- (like Pair together with _≈_). We then promise that we never use _≡_ -- on elements of type Pair, but instead only ever _≈_. sum : Pair → ℕ sum (mk a b) = a + b -- additional proof obligation (coming from the promise, not enforced by Agda): {- lemma-sum-invariant : (z z' : Pair) → z ≈ z' → sum z ≡ sum z' lemma-sum-invariant = {!!} twice-sum : Pair → ℕ twice-sum z = sum z + sum z lemma-twice-sum-invariant : (z z' : Pair) → z ≈ z' → twice-sum z ≡ twice-sum z' lemma-twice-sum-invariant = {!!} -} -- How can we define the type of unordered lists of natural numbers? ("multisets") -- How can we define the type ℤmod4 of "integers modulo 4" -- (where 0 ≡ 4, 1 ≡ 5, 2 ≡ 6, ...)? {- more generally: data Pair (X : Set) : Set where mk : X → X → Pair ex : Pair ℕ ex = mk one two -}