-- Playing with Agda in your browser: agdapad.quasicoherent.io
-- Course on Agda: lets-play-agda.quasicoherent.io

{-# OPTIONS --cubical #-}

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

{-
  Possible projects for this tutorial
  (can also be mixed to some extent):

  1. commutativity of addition
  2. correctness of insertion sort
  3. set theory (via sets as trees)
  4. something else?
-}

-- zero : ℕ : Set : Set₁ : Set₂ : ... : Setω : Setω1 : ...

-- Level

-- Set = the type of all small types
-- Set₁ = the type of all large types
-- Set₂ = the type of all very large types

data ℕ : Set where  -- \bN \alpha \to
  zero : ℕ
  succ : ℕ → ℕ
-- Inhabitants of ℕ are:
-- zero, succ zero, succ (succ zero), succ (succ (succ zero)), ...
-- Ctrl-c Ctrl-l: load file
-- in blackboard mathematics: f(x)
-- in Agda:                   f x

one : ℕ
one = succ zero

two : ℕ
two = succ one

twice : ℕ → ℕ
twice zero     = zero
twice (succ x) = succ (succ (twice x))
-- Ctrl-c Ctrl-c: case split
-- Ctrl-c Ctrl-SPACE: ask Agda to accept our input in the hole

{-# BUILTIN NATURAL ℕ #-}

-- In Agda, the activities of proving and programming are unified.
-- For each assertion, we write up in Agda the type of its witnesses.
-- To prove an assertion, we write down an inhabitant of the type of witnesses.

-- For any two natural numbers x and y, there is the type (x ≡ y).
-- This type contains witnesses that x equals y.
-- For instance, the type (zero ≡ one) is empty.
-- For instance, the type (zero ≡ zero) is inhabited.

grande-teorema : (zero ≡ zero)
grande-teorema = refl

grande-teorema' : (twice  ≡ )
grande-teorema' = refl

_+_ : ℕ → (ℕ → ℕ)
zero   + y = y
succ x + y = succ (x + y)

-- Computational reading: "lemma" is a function which inputs a number y : ℕ
-- and which outputs a witness that zero + y equals y.
-- Logical reading: For every number y : ℕ, zero + y equals y.
lemma : (y : ℕ) → (zero + y ≡ y)   -- \==
lemma y = refl
-- Ctrl-c Ctrl-COMMA: display the current situation
-- Ctrl-c Ctrl-a:     automatic mode

-- In Cubical Agda, there is an inbuilt type I representing the unit interval.
-- i0 : I
-- i1 : I
-- (i½ : I)
refl' : {X : Set} → {a : X} → (a ≡ a)
refl' {X} {a} = λ i → a
-- Ctrl-c Ctrl-r: automatic mode, but just for one step
-- on a blackboard: (i ↦ ...)
-- in lambda calculus: λi. ...

symm' : {X : Set} → {a b : X} → a ≡ b → b ≡ a
symm' p = λ i → p (~ i)
-- Here p is a path from a to b, so a function I → X such that p i0 is a and p i1 is b.
-- We need to construct a path q from b to a.
-- On a blackboard: q(i) := p(1-i)
-- On a blackboard: q    := (i ↦ p(1-i))

-- Logical reading: For every type X, for every type X, for every elements a, b : X,
-- for every function f : X → Y, if a equals b, then f(a) equals f(b).
-- Computational reading "cong'" is a function which inputs
-- 1. a type X (implicitly)
-- 2. a type Y (implicitly)
-- 3. an element a : X (implicitly)
-- 4. an element b : X (implicitly)
-- 5. a function f : X → Y
-- 6. a witness that a equals b
-- and outputs a witness that f(a) equals f(b).
cong' : {X Y : Set} → {a b : X} → (f : X → Y) → a ≡ b → f a ≡ f b
-- cong' f p = λ i → f (p i)
cong' f p i = f (p i)

lemma' : (x : ℕ) → (x + zero ≡ x)
lemma' zero     = refl
lemma' (succ x) = cong' succ (lemma' x)

data OrderedPair : Set where
  mk : ℕ → ℕ → OrderedPair

data UnorderedPair : Set where
  mk : ℕ → ℕ → UnorderedPair
  swap : (a b : ℕ) → mk a b ≡ mk b a

data S¹ : Set where
  base : S¹
  loop : base ≡ base