{-# OPTIONS --without-K --type-in-type #-}

open import Agda.Primitive renaming (_⊔_ to lmax) public
open import Agda.Builtin.Sigma public
open import Agda.Builtin.Unit public
open import Agda.Builtin.Equality public
import Agda.Builtin.Nat
open Agda.Builtin.Nat hiding (_*_; _+_) renaming (Nat to ℕ) public
_+_ = Agda.Builtin.Nat._+_
_*_ = Agda.Builtin.Nat._*_
infixl 80 _+_
infixl 85 _*_
open import Agda.Builtin.FromNat public
open import Agda.Builtin.FromNeg public

data TLevel : Set where
  ⟨-2⟩ : TLevel
  suc : (t : TLevel) → TLevel

postulate
  magic : ∀ {i} {X : Set i} → X

Type : Set₁
Type = Set -- a better name for Set

data _⊔_ (A : Type) (B : Type) : Type where
  inl : A → A ⊔ B
  inr : B → A ⊔ B
infixr 4 _⊔_

data ⊥ : Type where

abort : {A : Type} → ⊥ → A
abort ()

¬_ : Type → Type
¬ A = A → ⊥

{- START of Agda hack to write numerals directly -}
instance
  Numℕ : Number ℕ
  Number.Constraint Numℕ _ = ⊤
  Number.fromNat    Numℕ n = n
  NumTLevel : Number TLevel
  Number.Constraint NumTLevel _ = ⊤
  Number.fromNat    NumTLevel k = natToTLevel k
    where
      natToTLevel : ∀ ℕ → {{_ : ⊤}} → TLevel
      natToTLevel 0 = suc (suc ⟨-2⟩)
      natToTLevel (suc n) = suc (natToTLevel n)
  NegTLevel : Negative TLevel
  Negative.Constraint NegTLevel 0 = ⊤
  Negative.Constraint NegTLevel 1 = ⊤
  Negative.Constraint NegTLevel 2 = ⊤
  Negative.Constraint NegTLevel _ = ⊥
  Negative.fromNeg    NegTLevel 0 = suc (suc ⟨-2⟩)
  Negative.fromNeg    NegTLevel 1 = suc ⟨-2⟩
  Negative.fromNeg    NegTLevel 2 = ⟨-2⟩
  Negative.fromNeg    NegTLevel (suc (suc (suc _))) ⦃()⦄
{- END of the Agda hack to write numerals -}

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

{- groupoidal aspects -}

_∙_ : ∀ {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
refl ∙ q = q
infixr 80 _∙_

!_ : ∀ {A : Type} {x y : A} → x ≡ y → y ≡ x
! refl = refl
infixr 100 !_

∙-unit-r : ∀ {A : Type} {x y : A} (q : x ≡ y) → q ∙ refl ≡ q
∙-unit-r refl = refl

∙-unit-l : ∀ {A : Type} {x y : A} (q : x ≡ y) → refl ∙ q ≡ q
∙-unit-l q = refl

!-inv-l : ∀ {A : Type} {x y : A} (p : x ≡ y) → (! p) ∙ p ≡ refl
!-inv-l refl = refl

!-inv-r : ∀ {A : Type} {x y : A} (p : x ≡ y) → p ∙ (! p) ≡ refl
!-inv-r refl = refl

!-! : ∀ {A : Type} {x y : A} (p : x ≡ y) → ! (! p) ≡ p
!-! refl = refl

∙-assoc : ∀ {A : Type} {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
  → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
∙-assoc refl q r = refl

{- functorial aspects -}

ap-∙ : ∀ {A B : Type} (f : A → B) {x y z : A} (p : x ≡ y) (q : y ≡ z)
  → ap f (p ∙ q) ≡ ap f p ∙ ap f q
ap-∙ f refl q = refl

ap-! : ∀ {A B : Type} (f : A → B) {x y : A} (p : x ≡ y) → ap f (! p) ≡ ! (ap f p)
ap-! f refl = refl

{- we like truncation levels more today -}

is-contr : Type → Type
is-contr A = Σ A (λ x → (y : A) → x ≡ y)

has-level : TLevel → Type → Type
has-level ⟨-2⟩ A = is-contr A
has-level (suc n) A = (x y : A) → has-level n (x ≡ y)

is-prop : Type → Type
is-prop = has-level -1

is-set : Type → Type
is-set = has-level 0

record is-equiv {A B : Type} (f : A → B) : Type where
  field
    g : B → A
    f-g : ∀ (b : B) → f (g b) ≡ b
    g-f : ∀ (a : A) → g (f a) ≡ a
    adj : ∀ (a : A) → ap f (g-f a) ≡ f-g (f a)

infix 30 _≃_
_≃_ : Type → Type → Type
A ≃ B = Σ (A → B) is-equiv

{- quasi-inverses -> equivalences -}
is-eq : ∀ {A B : Type} (f : A → B) (g : B → A) (f-g : (y : B) → f (g y) ≡ y) (g-f : (x : A) → g (f x) ≡ x) → is-equiv f
is-eq {A} {B} f g f-g g-f =
  record {g = g; f-g = f-g'; g-f = g-f; adj = adj} where
    abstract
      {- adjusting f-g -}
      f-g' : (y : B) → f (g y) ≡ y
      f-g' b = ! (ap (λ y → f (g y)) (f-g b)) ∙ ap f (g-f (g b)) ∙ f-g b

      {- you can prove this -}
      postulate
        adj : (a : A) → ap f (g-f a) ≡ f-g' (f a)

equiv : ∀ {A B : Type} (f : A → B) (g : B → A) (f-g : (y : B) → f (g y) ≡ y) (g-f : (x : A) → g (f x) ≡ x) → A ≃ B
equiv f g f-g g-f = f , is-eq f g f-g g-f

–> : ∀ {A B : Type} → A ≃ B → (A → B)
–> e a = fst e a

<– : ∀ {A B : Type} → A ≃ B → (B → A)
<– e b = is-equiv.g (snd e) b

---------------------------------------------------------------------------
-- Part I: best Agda hacks: equational reasoning

infixr 10 _≡⟨_⟩_
infix  15 _≡∎

_≡⟨_⟩_ : ∀ {A : Type} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ refl ⟩ refl = refl

_≡∎ : ∀ {A : Type} (x : A) → x ≡ x
_ ≡∎ = refl

---------------------------------------------------------------------------

+-0-r : ∀ n → n + 0 ≡ n
+-0-r 0 = refl
+-0-r (suc n) = ap suc (+-0-r n)

+-suc-r : ∀ n m → n + suc m ≡ suc (n + m)
+-suc-r 0 m = refl
+-suc-r (suc n) m =
  (suc n) + (suc m)
    ≡⟨ refl ⟩
  suc (n + (suc m))
    ≡⟨ ap suc (+-suc-r n m) ⟩
  suc (suc n + m)
    ≡∎

+-comm : ∀ n m → n + m ≡ m + n
+-comm 0 m = ! (+-0-r m)
+-comm (suc n) m =
  (suc n) + m
    ≡⟨ refl ⟩
  suc (n + m)
    ≡⟨ ap suc (+-comm n m) ⟩
  suc (m + n)
    ≡⟨ ! (+-suc-r m n) ⟩
  m + suc n
    ≡∎

+-assoc : ∀ n m o → (n + m) + o ≡ n + (m + o)
+-assoc 0 _ _ = refl
+-assoc (suc n) _ _ = ap suc (+-assoc n _ _)

*-0-r : ∀ n → n * 0 ≡ 0
*-0-r 0 = refl
*-0-r (suc n) = *-0-r n

*-suc-r : ∀ m n → m * suc n ≡ m + m * n
*-suc-r 0 n = refl
*-suc-r (suc m) n =
  suc m * suc n
    ≡⟨ refl ⟩
  suc n + m * suc n
    ≡⟨ ap (suc n +_) (*-suc-r m n) ⟩
  (suc n + (m + m * n))
    ≡⟨ ! (+-assoc (suc n) m (m * n)) ⟩
  ((suc n + m) + m * n)
    ≡⟨ ap (λ k → suc k + m * n) (+-comm n m) ⟩
  suc (m + n) + m * n
    ≡⟨ +-assoc (suc m) n (m * n) ⟩
  suc m + (suc m) * n
    ≡∎

-- Don't do this, please:
-- ap (suc n +_) (*-suc-r m n) ∙ ! (+-assoc (suc n) m (m * n)) ∙ ap (λ k → suc k + m * n) (+-comm n m) ∙ +-assoc (suc m) n (m * n)

*-comm : ∀ n m → n * m ≡ m * n
*-comm = magic

{- BONUS -}

*-distrib-+-r : ∀ m n o → (n + o) * m ≡ n * m + o * m
*-distrib-+-r = magic

*-assoc : ∀ n m o → (n * m) * o ≡ n * (m * o)
*-assoc = magic

---------------------------------------------------------------------------
-- Part II: vectors

data Vector (A : Type) : ℕ → Type where
  --        ^^^^^^^^^^   ^^^
  --        parameters   indexes
  [] : Vector A 0
  _∷_ : ∀ {n : ℕ} → A → Vector A n → Vector A (suc n)

_++_ : ∀ {A : Type} {n m : ℕ} → Vector A n → Vector A m → Vector A (n + m)
[] ++ v = v
(x ∷ v₁) ++ v₂ = x ∷ (v₁ ++ v₂)

---------------------------------------------------------------------------
-- Part III (optional): finish the univalence

coe : ∀ {A B : Type} → A ≡ B → A → B
coe refl a = a

coe! : ∀ {A B : Type} → A ≡ B → B → A
coe! refl b = b

{- another name for id-to-equiv -}
coe-is-equiv : ∀ {A B : Type} (p : A ≡ B) → is-equiv (coe p)
coe-is-equiv {A} {B} p = is-eq (coe p) (coe! p) (f-g p) (g-f p) where

  f-g : ∀ {A B : Type} (p : A ≡ B) (b : B) → coe p (coe! p b) ≡ b
  f-g refl b = refl

  g-f : ∀ {A B : Type} (p : A ≡ B) (a : A) → coe! p (coe p a) ≡ a
  g-f refl a = refl

coe-equiv : ∀ {A B : Type} → A ≡ B → A ≃ B
coe-equiv p = coe p , coe-is-equiv p

postulate
  univalence : ∀ {A B : Type} → is-equiv (coe-equiv {A} {B})

ua : ∀ {A B : Type} → A ≃ B → A ≡ B
ua = is-equiv.g univalence

coe-ua : ∀ {A B : Type} (e : A ≃ B) (a : A) → coe (ua e) a ≡ –> e a
coe-ua e a = ap (λ e → –> e a) (is-equiv.f-g univalence e)
{- hints: what is –> (coe-equiv ...) a? -}

---------------------------------------------------------------------------
-- Part IV (optional): fibrations v.s. dependent types

happly : ∀ {A : Type} {B : A → Type} {f g : (x : A) → B x} (p : f ≡ g) → (x : A) → f x ≡ g x
happly p x = ap (λ f → f x) p

postulate
  funext : ∀ {A : Type} {B : A → Type} {f g : (x : A) → B x} → is-equiv (happly {f = f} {g = g})

{- this is the most used part of the function extensionality -}
λ≡ : ∀ {A : Type} {B : A → Type} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g
λ≡ {f = f} {g = g} h = is-equiv.g funext h

fiber : ∀ {A B : Type} → (A → B) → B → Type
fiber {A = A} f b = Σ A (λ a → f a ≡ b)

lemma₀ : ∀ {A B : Type} (f : A → B) → Σ B (λ b → fiber f b) ≡ A
lemma₀ = magic

lemma₁ : ∀ {B : Type} (F : B → Type) → fiber {A = Σ B F} {B = B} fst ≡ F
lemma₁ = magic

theorem : ∀ {B : Type} → (B → Type) ≃ Σ Type (λ A → (A → B))
theorem = magic

---------------------------------------------------------------------------
-- Part V (optional^2): when you have gone far

_⁻¹ : ∀ {A B : Type} → A ≃ B → B ≃ A
_⁻¹ = magic

_∘e_ : ∀ {A B C : Type} → B ≃ C → A ≃ B → A ≃ C
_∘e_ = magic

contr≃unit : ∀ {A : Type} → is-contr A → A ≃ ⊤
contr≃unit = magic