{-# 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
-}