{-# 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
open import Agda.Builtin.Nat renaming (Nat to ℕ) public
open import Agda.Builtin.FromNat public
open import Agda.Builtin.FromNeg public

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

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 with adjusted f-g, but a full proof here would
         make this file unnecessarily long. -}
      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

_×_ : Type → Type → Type
A × B = Σ A (λ _ → B)

≡× : ∀ {A B : Type} (x y : A × B) → Type
≡× (x₁ , x₂) (y₁ , y₂) = (x₁ ≡ y₁) × (x₂ ≡ y₂)

≡×-econv : ∀ {A B : Type} (x y : A × B) → (x ≡ y) ≃ (≡× x y)
≡×-econv x y = equiv f g f-g g-f where
  f : x ≡ y → ≡× x y
  f refl = refl , refl

  g : ≡× x y → x ≡ y
  g (refl , refl) = refl

  f-g : ∀ (p : ≡× x y) → f (g p) ≡ p
  f-g (refl , refl) = refl

  g-f : ∀ (p : x ≡ y) → g (f p) ≡ p
  g-f refl = refl

{- the lecture on 2/20 stopped here -}

{- dependent paths -}

PathOver : ∀ {A : Type} (B : A → Type) {x y} → x ≡ y → B x → B y → Type
PathOver B refl u v = u ≡ v

infix 30 PathOver
syntax PathOver B p u v = u ≡ v [ B ↓ p ]

≡Σ : ∀ {A : Type} {B : A → Type} → (x y : Σ A B) → Type
≡Σ {B = B} (x₁ , x₂) (y₁ , y₂) = Σ (x₁ ≡ y₁) (λ p → x₂ ≡ y₂ [ B ↓ p ])

≡Σ-econv : ∀ {A : Type} {B : A → Type} (x y : Σ A B) → (x ≡ y) ≃ (≡Σ x y)
≡Σ-econv x y = equiv f g f-g g-f where
  f : x ≡ y → ≡Σ x y
  f refl = refl , refl

  g : ≡Σ x y → x ≡ y
  g (refl , refl) = refl

  f-g : ∀ (p : ≡Σ x y) → f (g p) ≡ p
  f-g (refl , refl) = refl

  g-f : ∀ (p : x ≡ y) → g (f p) ≡ p
  g-f refl = refl

≡⊔ : ∀ {A B : Type} (x y : A ⊔ B) → Type
≡⊔ (inl a₁) (inl a₂) = a₁ ≡ a₂
≡⊔ (inr b₁) (inr b₂) = b₁ ≡ b₂
≡⊔ (inl _) (inr _) = ⊥
≡⊔ (inr _) (inl _) = ⊥

≡⊔-econv : ∀ {A B : Type} (x y : A ⊔ B) → (x ≡ y) ≃ (≡⊔ x y)
≡⊔-econv {A} {B} x y = equiv (f x y) (g x y) (f-g x y) (g-f x y) where
  f' : (x : A ⊔ B) → (≡⊔ x x)
  f' (inl a) = refl
  f' (inr b) = refl

  f : (x y : A ⊔ B) → (x ≡ y) → (≡⊔ x y)
  f x x refl = f' x

  g : (x y : A ⊔ B) → (≡⊔ x y) → (x ≡ y)
  g (inl a₁) (inl a₂) refl = refl
  g (inr b₁) (inr b₂) refl = refl
  g (inl a₁) (inr b₂) e = abort e
  g (inr b₁) (inl a₂) e = abort e

  {- This also work:

  g : (x y : A ⊔ B) → (≡⊔ x y) → (x ≡ y)
  g (inl a₁) (inl a₂) p = ap inl p
  g (inr b₁) (inr b₂) p = ap inr p
  g (inl a₁) (inr b₂) e = abort e
  g (inr b₁) (inl a₂) e = abort e

  The function g can also be done with the absurd pattern.

  g : (x y : A ⊔ B) → (≡⊔ x y) → (x ≡ y)
  g (inl a₁) (inl a₂) refl = refl
  g (inr b₁) (inr b₂) refl = refl
  g (inl a₁) (inr b₂) ()
  g (inr b₁) (inl a₂) ()

  We however want to avoid the absurd pattern "()" in this file (except
  "abort" itself) because Agda can go very far to determine whether
  some type is empty. While it is convenient, it may hurt your
  understanding of the underlying theory. It is better to use only
  "abort" before having a good grasp of the theory.

  In principle, all usages of the absurd pattern can be implemented
  by "abort" and universes in our type theory on paper. The universes
  are essential, because without them there are counter-models that
  invalidate some absurd patterns in Agda.
  -}

  {- Often, to prove a property about a function f,
     you should first try following the definition of f.

     For example, if f : Bool → C is defined by pattern matching
     on the input, with two branches matching true and false,
     then it is expected that most properties of the function f
     can be proved by pattern matching on the input as well.

     There are some theorems which need more creativity,
     but not in this practice. -}

  {- For example, this follows the definition of g. -}
  f-g : (x y : A ⊔ B) → ∀ p → f x y (g x y p) ≡ p
  f-g (inl a₁) (inl a₂) refl = refl
  f-g (inr b₁) (inr b₂) refl = refl
  f-g (inl a₁) (inr b₂) e = abort e
  f-g (inr b₁) (inl a₂) e = abort e

  {- These follow the definition of f. -}
  g-f' : (x : A ⊔ B) → g x x (f' x) ≡ refl
  g-f' (inl a) = refl
  g-f' (inr b) = refl

  g-f : (x y : A ⊔ B) → ∀ p → g x y (f x y p) ≡ p
  g-f x x refl = g-f' x

≡ℕ : ∀ (x y : ℕ) → Type
≡ℕ zero zero = ⊤
≡ℕ (suc n) (suc m) = ≡ℕ n m
≡ℕ zero (suc m) = ⊥
≡ℕ (suc n) zero = ⊥

≡ℕ-econv : ∀ (x y : ℕ) → (x ≡ y) ≃ (≡ℕ x y)
≡ℕ-econv x y = equiv (f x y) (g x y) (f-g x y) (g-f x y) where
  f' : (x : ℕ) → (≡ℕ x x)
  f' zero = tt
  f' (suc n) = f' n

  f : (x y : ℕ) → (x ≡ y) → (≡ℕ x y)
  f x x refl = f' x

  g : (x y : ℕ) → (≡ℕ x y) → (x ≡ y)
  g zero zero tt = refl
  g (suc n) (suc m) p = ap suc (g n m p)
  g zero (suc m) e = abort e
  g (suc n) zero e = abort e

  f-ap-suc : (x y : ℕ) → (p : x ≡ y) → f (suc x) (suc y) (ap suc p) ≡ f x y p
  f-ap-suc x x refl = refl

  f-g : (x y : ℕ) → ∀ p → f x y (g x y p) ≡ p
  f-g zero zero tt = refl
  f-g (suc x) (suc y) p = f-ap-suc x y (g x y p) ∙ f-g x y p
  f-g zero (suc _) e = abort e
  f-g (suc _) zero e = abort e

  g-f' : (x : ℕ) → g x x (f' x) ≡ refl
  g-f' zero = refl
  g-f' (suc n) = ap (ap suc) (g-f' n)

  g-f : (x y : ℕ) → ∀ p → g x y (f x y p) ≡ p
  g-f x x refl = g-f' x

¬0≡suc : ∀ (n : ℕ) → ¬ (zero ≡ suc n)
¬0≡suc n p = abort (–> (≡ℕ-econv zero (suc n)) p)
{- You can finish the proof with

   ¬0≡suc n ()

   but please try to use only "abort" and the above lemmas.
   Also, check out the definition of "–>".
-}

{- The importance of "pred" is that pred(suc n) = n.
   That is, it can cancel a "suc". -}
pred : ℕ → ℕ
pred zero = zero
pred (suc n) = n

ℕ-has-dec : ∀ (n m : ℕ) → (n ≡ m) ⊔ (¬ (n ≡ m))
ℕ-has-dec zero zero = inl refl
ℕ-has-dec (suc n) (suc m) with ℕ-has-dec n m
... | inl n≡m = inl (ap suc n≡m)
... | inr n≢m = inr (λ sucn≡sucm → n≢m (ap pred sucn≡sucm))
ℕ-has-dec zero (suc m) = inr (λ 0=sucm → ¬0≡suc m 0=sucm)
ℕ-has-dec (suc m) zero = inr (λ sucm=0 → ¬0≡suc m (! sucm=0))

postulate -- Homework 2, Part 2
  hedberg : ∀ {A : Type} → (∀ (x y : A) → (x ≡ y) ⊔ (¬ (x ≡ y))) → is-set A

ℕ-is-set : is-set ℕ
ℕ-is-set = hedberg ℕ-has-dec

{- function extensionality gives us a way to reason about
   identifications between functions -}

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})

≡Π : ∀ {A : Type} {B : A → Type} (f g : (x : A) → B x) → Type
≡Π {A = A} f g = (x : A) → f x ≡ g x

≡Π-econv : ∀ {A : Type} {B : A → Type} (f g : (x : A) → B x) → (f ≡ g) ≃ ≡Π f g
≡Π-econv f g = happly , funext

{- this is the most used part of the function extensionality -}
λ≡ : ∀ {A : Type} {B : A → Type} {f g : (x : A) → B x} → ≡Π f g → f ≡ g
λ≡ {f = f} {g = g} h = <– (≡Π-econv f g) h