{-
  Options for now:
  1. Exercises
  2. Cubical Agda
  3. The surjection that shouldn't be (introducing to forcing)
  4. Peano arithmetic
  5. Tiny toy programming language
  7. Demonstration of local network hacking
-}

{-# OPTIONS --cubical --allow-unsolved-metas #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude

data ℤmod4 : Set where
  zero : ℤmod4           -- this is a point constructor
  succ : ℤmod4 → ℤmod4   -- this too
  wrap : succ (succ (succ (succ zero))) ≡ zero   -- this is a so-called "path constructor"
{-
  *    *    *    *    *    *    *    *    *   ....
  ^    ^              |    |
  |    |              |    |
  +-------------------+    |
       |                   |
       +-------------------+
-}

one : ℤmod4
one = succ zero

five : ℤmod4
five = succ (succ (succ (succ (succ zero))))

_ : five ≡ one
_ = cong succ wrap

data UnorderedPair (A : Set) : Set where
  pair : A → A → UnorderedPair A
  swap : (x y : A) → pair x y ≡ pair y x

example-pair : UnorderedPair ℤmod4
example-pair = pair one zero

example-pair' : UnorderedPair ℤmod4
example-pair' = pair zero one

_ : example-pair ≡ example-pair'
_ = swap one zero

-- The UnorderedPair construction above succeeds in making the following definition impossible.
first : {A : Set} → UnorderedPair A → A
first (pair x y)   = x
first (swap x y i) = {!!}

data Circle : Set where
  base : Circle
  loop : base ≡ base

refl' : {X : Set} → (x : X) → x ≡ x
refl' x = λ i → x
-- Internally, in cubical Agda, a path in a space X is a function γ : I → X,
-- where I = [0, 1] is the unit interval. We think of I as the continuous unit interval
-- containing lots of points (for instance 0, 0.1, 0.2, 0.5, 1/π, 0.999, 1).
-- But behind the scenes, I is implemented in a more economical manner.
-- The only points of I which are actually accessible to Agda code are i0 and i1.

sym' : {X : Set} {a b : X} → a ≡ b → b ≡ a
sym' p = λ i → p (~ i)     -- ~ i = i1 - i
-- We have: p : I → X with p i0 = a and p i1 = b.
-- We want: q : I → X with q i0 = b and q i1 = a.

trans : {X : Set} {a b c : X} → a ≡ b → b ≡ c → a ≡ c
trans p q = p ∙ q

cong' : {X Y : Set} {a b : X} → (f : X → Y) → a ≡ b → f a ≡ f b
cong' f p = λ i → f (p i)
-- We have: p : I → X with p i0 = a   and p i1 = b.
-- We want: 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

open import Padova2025.ProvingBasics.Equality.Base renaming (_≡_ to _≡ᵢ_; refl to reflᵢ)

theorem : {X : Set} {a b : X} → a ≡ᵢ b → a ≡ b
theorem {X} {a} {b} reflᵢ = refl' a
-- theorem {a = a} reflᵢ = refl' a

theorem' : {X : Set} {a b : X} → a ≡ b → a ≡ᵢ b
theorem' = {!J!}


open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic

data ℤ : Set where
  _⊝_ : (credit : ℕ) → (debt : ℕ) → ℤ
  cancel : (a b : ℕ) → a ⊝ b ≡ succ a ⊝ succ b

-- In cubical Agda, we can avoid the setoid hell.
-- (Setoid hell = having to deal with equivalence relations all the time)
-- In standard Agda, we would need to do the following.

data ℤ' : Set where   -- the proto-integers
  _⊝'_ : (credit : ℕ) → (debt : ℕ) → ℤ'

_≈_ : ℤ' → ℤ' → Set
(a ⊝' b) ≈ (u ⊝' v) = (a + v) ≡ᵢ (u + b)
{-
a-b  =  u-v
a+v  =  u+b
-}

succℤ' : ℤ' → ℤ'
succℤ' (a ⊝' b) = succ a ⊝' b

succℤ'-≈ : {x y : ℤ'} → x ≈ y → succℤ' x ≈ succℤ' y
succℤ'-≈ = {!!}

{-
f : ℤ' → ℤ'
f x = ....succℤ'....

f-≈ : {x y : ℤ'} → x ≈ y → f x ≈ f y
f-≈ = ?
-}

example-int : ℤ
example-int = succ (succ (succ zero)) ⊝ succ zero

example-int' : ℤ
example-int' = succ (succ (succ (succ zero))) ⊝ succ (succ zero)

minusone : ℤ
minusone = zero ⊝ succ zero

succℤ : ℤ → ℤ
succℤ (credit ⊝ debt) = succ credit ⊝ debt
succℤ (cancel a b i)  = cancel (succ a) b i

_ = example-int ≡ example-int'
_ = cancel (succ (succ (succ zero))) (succ zero)

{-
  * γ(0)            * γ(1)
  |                /γ(0.999)
  |γ(0.1)  γ(0.5) /
   \         /\  /
    \       /  \/
     +-->--+
-}

data Segment : Set where
  start : Segment
  end   : Segment
  walk  : start ≡ end
{-
  *->-->-->--*              *              *
                             \            /
                              \          /
                               +---->---+
-}

data FilledSquare : Set where     --   *----+
  upper-left  : FilledSquare      --   |####v
  lower-right : FilledSquare      --   +-->-*
  p           : upper-left ≡ lower-right
  q           : upper-left ≡ lower-right
  filler      : p ≡ q

{-
data Sphere : Set where
  base : Sphere
  surf : (refl) ≡ (refl)
-}

{-
  Standard Agda                                  Cubical Agda
  type X                                         space X (up to homotopy equivalence)  
  empty type ⊥                                   empty space
  value a : X                                    points a : X
  type a ≡ b of equality witnesses               space a ≡ b of paths from a to b
  refl : a ≡ a                                   refl : a ≡ a, the constant path from a to a
  given p : a ≡ b, we have sym p : b ≡ a         sym p, the same path as p, but in reverse
  trans p q                                      trans p q (also written p ∙ q), the path obtained by joining p and q

  uniqueness of identity proofs (UIP)            ----
  "Given p and q of type a ≡ b, we have p ≡ q."  "Given any two paths, they are the same."
-}