{-# OPTIONS --allow-unsolved-metas --cubical --guardedness #-}
module session08b where
open import Cubical.Foundations.Prelude
-- Let's define the type of integers modulo four: 0, 1, 2, 3; 4 should be the same as 0.
data ℤmod4 : Set where
zero : ℤmod4
succ : ℤmod4 → ℤmod4
loop : succ (succ (succ (succ zero))) ≡ zero
-- The type ℤmod4 is freely generated by zero, succ and loop.
-- (The existence of `loop` induces many more identifications.)
-- Cubical Agda is like standard Agda, but with a radical reinterpretation
-- of how we think of types and with a radical reimagination of equality.
-- Cubical Agda is an implementation of homotopy type theory.
-- In standard Agda, we think of a type as a collection of values.
-- In cubical Agda, we think of a type as a space.
-- In standard Agda, we picture ⊥ as the empty collection.
-- In cubical Agda, we picture ⊥ as the empty space.
-- In standard Agda, we needed to define _≡_ on our own; and we pictured
-- an inhabitant of the type (x ≡ y) as a witness that x equals y.
-- In cubical Agda, there is a predefined _≡_; and we picture the type (x ≡ y)
-- as the space of paths from x to y.
-- Picture of ℤmod4: * * * * * * * * * * ...
-- | |
-- +-----------+
_ : succ (succ (succ (succ (succ zero)))) ≡ succ zero
_ = cong succ loop
-- Let's define the type of unordered pairs.
-- For comparison, here is the type of ordered pairs:
data Pair (A : Set) : Set where
_,_ : A → A → Pair A
data UnorderedPair (A : Set) : Set where
_,_ : A → A → UnorderedPair A
swap : (x y : A) → (x , y) ≡ (y , x)
up1 : UnorderedPair ℤmod4
up1 = (succ zero , succ (succ zero))
up2 : UnorderedPair ℤmod4
up2 = (succ (succ zero) , succ zero)
_ : up1 ≡ up2
_ = swap (succ zero) (succ (succ zero))
open import Padova2025.ProgrammingBasics.Naturals.Base hiding (one; two; three)
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
first : {A : Set} → UnorderedPair A → A
first (x , y) = x
first (swap x y i) = {!!} -- no way of filling this in
sum : UnorderedPair ℕ → ℕ
sum (a , b) = a + b
sum (swap a b i) = {!!} -- we can fill this in by referring to commutativity of addition
data Circle : Set where
north : Circle
loop : north ≡ north
-- Inhabitants of the type north ≡ north:
-- refl, loop, symm loop, trans loop loop, trans loop (trans loop loop), ...
-- loop ≢ refl, loop ≢ trans loop loop, but trans loop (symm loop) ≡ refl.
-- ++ ++
-- / \ / \
-- Figure 8: + + +
-- \ / \ /
-- ++ ++
data Figure8 : Set where
center : Figure8
loopₗ : center ≡ center
loopᵣ : center ≡ center
-- Note that loopₗ ≢ loopᵣ.
-- [--------]
data Interval : Set where
start : Interval
end : Interval
path : start ≡ end
-- In standard Agda, our custom datatype (x ≡ y) at most contains refl.
-- In cubical Agda, the predefined datatype (x ≡ y) can contain many elements.
-- The following piece of text can be found in any textbook on topology or geometry:
--
-- Def.: A path in a space X is a continuous function γ : [0,1] → X,
-- where [0,1] = { x ∈ ℝ | 0 ≤ x ≤ 1 } is the unit interval.
--
-- The starting point of such a path γ is γ(0).
-- The end point of such a path γ is γ(1).
-- The point γ(0.999) is very close to the end point.
-- The point γ(0.5) is the midpoint of the path.
--
-- γ(0)
-- *
-- \ γ(0.5)
-- \ /\
-- ----- ------*
-- γ(1)
-- Let a, b : X.
-- In cubical Agda, (a ≡ b) is the type of paths from a to b.
-- A path from a to b is a function I → X, where I is a predefined primitive unit interval.
-- Inhabitants of I: i0, i1.
-- It kinda looks like that I also contains i0.5, i0.999 and so on. (But they are not
-- really there in the implementation.)
-- logical reading: For every x, it is the case x ≡ x.
-- computational reading: `refl'` is a function which inputs a type `X` and a value `x : X`
-- and outputs a witness that `x` equals `x`.
-- homotopical reading (roughly): For every x, there is a path from x to x.
refl' : {X : Set} {x : X} → x ≡ x
refl' {X} {x} = λ i → x
-- homotopical reading (roughly): For every x, for every y, for every path from x to y,
-- there is a path from y to x.
symm' : {X : Set} {x y : X} → x ≡ y → y ≡ x
symm' p = λ i → p (~ i)
-- In cubical Agda, "i1 - i" is written `~ i`.
-- symm' p i0 is p i1, so y.
-- symm' p i1 is p i0, so x.
cong' : {X Y : Set} {a b : X} → (f : X → Y) → a ≡ b → f a ≡ f b
cong' f p = λ i → f (p i)
-- f : X → Y
-- p : I → X with p i0 = a and p i1 = b
-- We are looking for a function q : I → Y with q i0 = f a and q i1 = f b.
funext : {X Y : Set} {f g : X → Y} → ((x : X) → f x ≡ g x) → f ≡ g
funext h = λ i x → h x i
-- h is a function which maps an input `x : X` to a path from f x to g x.
-- So h x : I → Y with h x i0 = f x and h x i1 = g x.
data ∥_∥ (X : Set) : Set where
∣_∣ : X → ∥ X ∥
squash : (a b : ∥ X ∥) → a ≡ b
data ℤ : Set where
_⊖_ : ℕ → ℕ → ℤ -- a "point constructor"
cancel : (a b : ℕ) → (a ⊖ b) ≡ (succ a ⊖ succ b) -- a "path constructor"
succℤ : ℤ → ℤ
succℤ (a ⊖ b) = succ a ⊖ b
succℤ (cancel a b i) = cancel (succ a) b i
doublesuccℤ : ℤ → ℤ
doublesuccℤ x = succℤ (succℤ x)
-- The type of paths from north to north (where north : Circle)
-- is of the same size as ℤ. (Given any integer n, we can
-- go around the circle n times and thereby obtain a path from north to north.)
-- Using univalence, we can more precisely show: (north ≡ north) ≡ ℤ.
-- The type of all small types, Set, does not contain a path from Bool to ℕ.
-- But it contains two paths from Bool to Bool: refl, and then a second
-- path obtained from the observation that "not : Bool → Bool" is an equivalence.
-- Any equivalence between types can be upgraded, by univalence, to a path
-- between those types.
-- As a consequence, every isomorphism between monoids can be upgraded to
-- a path between those monoids: M ≅ N → M ≡ N.
-- On a blackboard, "M ≡ N" is a proposition; all there is to know about M ≡ N
-- is whether M ≡ N.
-- In cubical Agda, in contrast, `M ≡ N` can be a nontrivial type containing
-- lots of inhabitants.
data ℤmod4' : Set where
zero : ℤmod4'
one : ℤmod4'
two : ℤmod4'
three : ℤmod4'
iso : ℤmod4 → ℤmod4'
iso = ?
osi : ℤmod4' → ℤmod4
osi = ?
-- size : Set → Card
-- Options for now:
-- 1. Stop
-- 2. Exercises
-- 3. Sets as trees
-- 4. Infinite-time Turing machines
-- 5. Learn how we can use Agda to inspect what is provable