{-# OPTIONS --cubical --allow-unsolved-metas #-} open import Cubical.Core.Everything {- ROSETTA STONE for TRANSLATING between THREE SUBJECTS: 1. logic 2. computer science 3. homotopy theory (dealing with shapes) x ≡ y 1. "the values x and y are the same" 2. "the type of witnesses that x and y are the same" 3. "the space of paths from x to y" x ≡ y → y ≡ x 1. "if x is the same as y, then also y is the same as x" 2. "there is a function transforming witnesses that x ≡ y into witnesses that y ≡ x" 3. ??? ⊥ 1. "contradiction" 2. "the empty type" 3. "the empty space" In Cubical Agda, we picture types to be spaces. Every value of a type is then pictured as a point of the associated space. Here is a picture of the space associated to ℕ: 0 1 2 3 4 5 ... In this space, there is no path between 0 and 1. Here is a picture of another space: +----+ |####| |####| +----+ In this space, there is a path from every point to every other point. Here is a picture of yet another space: A----B C |####| /#\ |####| +---+ +----+ In this space, there is a path from A to B, but there is no path from A to C. In logic, if a ≡ b and b ≡ c, then we may conclude that a ≡ c. In homotopy theory, if we have a path from a to b and if we have a path from b to c, then we may concatenate those two paths to obtain a path from a to c. -} data ℕ : Set where zero : ℕ succ : ℕ → ℕ _+_ : ℕ → ℕ → ℕ zero + b = b succ a + b = succ (a + b) -- "Pair X" is the type of (ordered) pairs of values of X. data Pair (X : Set) : Set where mk : X → X → Pair X first : {X : Set} → Pair X → X first (mk a b) = a -- "UnorderedPair X" is the type of unordered pairs of values of X. data UnorderedPair (X : Set) : Set where mk : X → X → UnorderedPair X swap : (a b : X) → mk a b ≡ mk b a first' : {X : Set} → UnorderedPair X → X first' (mk a b) = a first' (swap a b i) = {!!} -- We are happy that this hole cannot be filled in. sum' : UnorderedPair ℕ → ℕ sum' (mk a b) = a + b sum' (swap a b i) = {!!} -- We are happy that this hole can be filled in. -- In Cubical Agda, there can be more witnesses of equality than -- just provided by "refl". For instance, "swap" provides additional -- witnesses. -- Let's define the type of numbers modulo 4: -- -4=0, -3=1, -2=2, -1=3, 0, 1, 2, 3, 4=0, 5=1, 6=2, 7=3, 8=4, ... data ℤmod4 : Set where zer : ℤmod4 suc : ℤmod4 → ℤmod4 wrap : (x : ℤmod4) → x ≡ suc (suc (suc (suc x))) data ℤmod4' : Set where zer' : ℤmod4' suc' : ℤmod4' → ℤmod4' wrap' : zer' ≡ suc' (suc' (suc' (suc' zer'))) -- Here is a picture of ℤmod4': -- +----------------+ -- | | -- 0 1 2 3 4 5 6 7 8 9 10 ... -- | | | | -- +------------------+ | -- | | -- +-----------------+ data S¹ : Set where base : S¹ loop : base ≡ base -- Here is a picture of the circle (just the boundary, not filled in): -- * -- / \ -- \_A base' : S¹ base' = loop i1 -- If p is any path in Cubical Agda, then p i0 is its beginning -- and p i1 is its end. And "p i0.5" would be its midpoint. -- And "p i0.25" would be its first-quarter-point. refl : {X : Set} {x : X} → x ≡ x refl {X} {x} i = x -- refl {X} {x} = λ i → x symm : {X : Set} {a b : X} → a ≡ b → b ≡ a symm {X} {a} {b} p i = p (~ i) -- symm {X} {a} {b} p = λ i → p (~ i) cong : {X Y : Set} {a b : X} → (f : X → Y) → a ≡ b → f a ≡ f b cong = {!!} -- The following principle is called "function extensionality". -- It is often expected by blackboard mathematicians. -- It is available (by a one-line proof) in Cubical Agda. -- It is not available in standard Agda. funext : {X Y : Set} {f g : X → Y} → ((x : X) → f x ≡ g x) → f ≡ g funext = {!!} -- How many paths are there from base to base? -- How many values does the same "base ≡ base" have? -- refl, loop, loop · loop, loop · loop · loop, ..., -- symm loop, symm loop · symm loop, ... -- We will also have the path loop · refl · loop, -- however this path will be the SAME as loop · loop. -- The path loop · symm loop will be the SAME as refl. data Interval : Set where left : Interval right : Interval seg : left ≡ right -- Here is a picture of the interval: -- +--------+ -- Here is a picture of yet another space: data Foo : Set where left : Foo right : Foo seg₁ : left ≡ right seg₂ : left ≡ right -- +----+ -- / \ -- + + -- \ / -- +----+ -- +---+ -- |###| -- |###| -- +---+ data FilledSquare : Set where upper-left-corner : FilledSquare lower-right-corner : FilledSquare path₁ : upper-left-corner ≡ lower-right-corner path₂ : upper-left-corner ≡ lower-right-corner body : path₁ ≡ path₂ toℕ : ℤmod4' → ℕ toℕ zer' = zero toℕ (suc' x) = succ (toℕ x) toℕ (wrap' i) = {!!} -- Note: toℕ (suc' zer') will be succ zero. -- toℕ (suc' (suc' (suc' (suc' (suc' zer'))))) will be 5. -- And (suc' zer') is the same as (suc' (suc' (suc' (suc' (suc' zer'))))). -- So, by congruence, also 1 should be the same as 5 in ℕ. _ : suc zer ≡ suc (suc (suc (suc (suc zer)))) _ = wrap (suc zer) _ : suc' zer' ≡ suc' (suc' (suc' (suc' (suc' zer')))) _ = {!cong suc' wrap'!} example : UnorderedPair ℕ example = mk (succ zero) (succ (succ zero)) example' : UnorderedPair ℕ example' = mk (succ (succ zero)) (succ zero) dream : example ≡ example' dream = swap (succ zero) (succ (succ zero)) -- How can we define the type of unordered pairs of values of X? -- One answer: Use sorted ordered pairs to represent -- unordered pairs. For instance, the unordered pair -- of the numbers 20 and 5 would be represented by -- (5 , 20). The unordered pair of the numbers 5 and 20 -- would be the SAME unordered pair and it would be -- represented by the same ordered pair (5 , 20). -- This is a good approach, HOWEVER it requires some -- ordering on X. -- Second answer: Just promise to never use ≡. -- Instead only use a custom-tailored approximate -- equality ≈. _≈_ : {X : Set} → Pair X → Pair X → Set (mk a b) ≈ (mk a' b') = {!(a ≡ a' × b ≡ b') ⊎ (a ≡ b' × b ≡ a')!} -- This is called the "setoid hell".