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

open import Prelude hiding (id ; Bool ; ℕ)

comm× : {A B : Type} → A × B → B × A
comm× (a , b) = b , a

thm : {A B : Set} → A → (A → B) → B
thm a f = f a

-- id : {A : Type} → A → A
-- id a = a

data Bool : Set where
  true  : Bool
  false : Bool

not : Bool → Bool
not true  = false
not false = true

not-not : (b : Bool) → not (not b) ≡ b
not-not true = refl
not-not false = refl

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

-- -- data _≡'_ {ℓ} {A : Type ℓ} : (x y : A) → Type ℓ where
  -- -- refl : {x : A} → x ≡' x

-- data _≡'_ {ℓ} {A : Type ℓ} (x : A) : (y : A) → Type ℓ where
  -- refl : x ≡' x

sym : {A : Type} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

quadruple : ℕ → ℕ
quadruple n = double (double n)
  where
  double : ℕ → ℕ
  double zero = zero
  double (suc n) = suc (suc (double n))

-- id : {ℓ : Level} {A : Type ℓ} → A → A
-- id a = a

-- Levels
private variable
  ℓ ℓ' : Level

arr : (A : Type ℓ) (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
arr A B = A → B

-- Capturing implicit arguments

-- id : {ℓ : Level} {A : Type ℓ} → A → A
-- id {ℓ} {A} a = a

-- id : {ℓ : Level} {A : Type ℓ} → A → A
-- id {A = A} a = a

-- arr : {ℓ ℓ' : Level} (A : Type ℓ) (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
-- arr A B = A → B

id : {ℓ : Level} {A : Type ℓ} → A → A
id = λ x → x

not' : Bool → Bool
not' = λ { true → false ; false → {!true!} }

module Int where
  int : Type
  int = {!!}

  add : int → int → int
  add = {!!}

module _ {ℓ ℓ' : Level} (A : Type ℓ) (B : Type ℓ') where
  f : A → B
  f = {!!}

  g : B → A
  g = {!!}

---
--- Equality
---

_*_ : ℕ → ℕ → ℕ
zero * n = zero
suc m * n = n + (m * n)

cong : {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

unitl : (n : ℕ) → zero + n ≡ n
unitl n = refl

unitr : (n : ℕ) → n + zero ≡ n
unitr zero = refl
unitr (suc n) = cong suc (unitr n)

-- infixl 6 _+_
-- infixl 7 _*_

-- *-suc : (m n : ℕ) → m * suc n ≡ m + m * n
-- *-suc zero n = refl
-- *-suc (suc m) n =
  -- suc (n + m * suc n)   ≡⟨ cong (λ m → suc (n + m)) (*-suc m n) ⟩
  -- suc (n + (m + m * n)) ≡⟨ cong suc {!!} ⟩ -- sym (+-assoc n m (m * n))
  -- suc ((n + m) + m * n) ≡⟨ cong (λ x → suc (x + m * n)) {!!} ⟩ -- +-comm n m
  -- suc ((m + n) + m * n) ≡⟨ cong suc {!!} ⟩ -- +-assoc m n (m * n)
  -- suc (m + (n + m * n)) ∎

+-comm : (m n : ℕ) → m + n ≡ n + m
+-comm zero n = sym (unitr n)
+-comm (suc m) n =
  suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩
  suc (n + m) ≡⟨ {!!} ⟩
  n + suc m ∎

---
--- Optional
---

-- data ⊤ : Type where
  -- tt : ⊤

-- data ⊥ : Type where

-- ¬ : Type → Type
-- ¬ A = A → ⊥

data List (A : Type) : Type where
  [] : List A
  _∷_ : A → List A → List A

length : {A : Type} → List A → ℕ
length [] = zero
length (x ∷ l) = suc (length l)

-- concat : {A : Set} → List A → List A → List A
-- concat [] m = m
-- concat (x ∷ l) m = x ∷ concat l m

-- length

data Vec (A : Type) : ℕ → Type where
  [] : Vec A zero
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

Vec' : Type → ℕ → Type
Vec' A n = Σ (List A) (λ l → length l ≡ n)

data Fin : ℕ → Type where
  Fzero : {n : ℕ} → Fin (suc n)
  Fsuc  : {n : ℕ} → Fin n → Fin (suc n)