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

open import Agda.Primitive renaming (_⊔_ to lmax) public
open import Agda.Builtin.Bool public
open import Agda.Builtin.Sigma public
open import Agda.Builtin.Unit public
open import Agda.Builtin.Equality public
open import Agda.Builtin.Nat hiding (_*_; _+_) 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

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

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

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

-- Here is the function extensionality

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

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

-- Part I: W-Types

data W (A : Type) (B : A → Type) : Type where
  sup : (a : A) → ((b : B a) → W A B) → W A B

{- task 1-1: Check the ℕ' line below and define a function from Bool to Type
   such that ℕ' ≃ ℕ. -}
task1-1 : Bool → Type
task1-1 true = ⊥
task1-1 false = ⊤
{- Hints: A natural number n can be represented by a chain of nodes of length n.
   What kinds of nodes do you need to construct such a chain? -}

ℕ' : Type
ℕ' = W Bool task1-1

{- task 1-2: Convince me! -}
task1-2 : ℕ' ≃ ℕ
task1-2 = equiv f g f-g g-f where
  f : ℕ' → ℕ
  f (sup true _) = zero
  f (sup false w) = suc (f (w tt))

  g : ℕ → ℕ'
  g zero = sup true abort
  g (suc n) = sup false (λ _ → g n)

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

  g-f : ∀ x → g (f x) ≡ x
  g-f (sup true w') = ap (sup true) (λ≡ (λ c → abort c))
  g-f (sup false w') = ap (sup false) (λ≡ (λ _ → g-f (w' tt)))

{-
task 1-3: Please summarize how function extentionality was used in task1-2. In particular, what could be an issue if there was no function extentionality? Would there be potentially too many or too few elements in ℕ'? How did function extensionality solve the issue?

**Please write down your reflection here.**
-}

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

-- Here is 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

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

-- This is the types Favonia gave in lectures
PathOver : ∀ {A : Type} (C : A → Type) {x y} → x ≡ y → C x → C y → Type
PathOver C refl cx cy = cx ≡ cy

infix 30 PathOver
syntax PathOver C p cx cy = cx ≡ cy [ C ↓ p ]

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

-- Part II

transp : ∀ {A : Type} (C : A → Type) {x y : A} (p : x ≡ y) → C x → C y
transp C p cx = coe (ap C p) cx

-- task 2-1: Give a definition equivalent to PathOver. If you are truly stuck,
-- check Definition 6.2.2 in the HoTT book and transliterate it into Agda.
task2-1 : ∀ {A : Type} (C : A → Type) {x y} → x ≡ y → C x → C y → Type
task2-1 C p cx cy = transp C p cx ≡ cy

{- task 2-2: Come up with transp! using coe! -}
transp! : ∀ {A : Type} (C : A → Type) {x y : A} (p : x ≡ y) → C y → C x
transp! C p cx = coe! (ap C p) cx

{- task 2-3: Find yet another definition of paths over paths using transp!. -}
task2-3 : ∀ {A : Type} (C : A → Type) {x y} → x ≡ y → C x → C y → Type
task2-3 C p cx cy = cx ≡ transp! C p cy

{- task 2-4: A lemma you will find useful. Hints: there was already a more
   general theorem in this file. Where is it? -}
task2-4 : ∀ A → A ≃ A
task2-4 A = coe-equiv refl

{- task 2-5 and bonus 2-1: now, show me your definitions are correct.
   Hints: Favonia once murmured whether the answer is too short.

   Uncomment and finish one of the following for task 2-5. Do both for
   bonus task 2-1.
   -}
task2-5-1 : ∀ {A : Type} (C : A → Type) {x y : A} (p : x ≡ y) (cx : C x) (cy : C y)
  → task2-1 C p cx cy ≃ PathOver C p cx cy
task2-5-1 C refl cx cy = task2-4 (cx ≡ cy)

task2-5-2 : ∀ {A : Type} (C : A → Type) {x y : A} (p : x ≡ y) (cx : C x) (cy : C y)
  → task2-3 C p cx cy ≃ PathOver C p cx cy
task2-5-2 C refl cx cy = task2-4 (cx ≡ cy)


{- task 2-6: path concatenation for paths over paths -}
_∙ᵈ_ : ∀ {A : Type} {C : A → Type} {x y z : A} {p : x ≡ y} {q : y ≡ z} {cx : C x} {cy : C y} {cz : C z}
  → cx ≡ cy [ C ↓ p ] → cy ≡ cz [ C ↓ q ] → cx ≡ cz [ C ↓ p ∙ q ]
_∙ᵈ_ {p = refl} {q = refl} r s = r ∙ s

{- task 2-7: reversal of paths over paths -}
!ᵈ_ : ∀ {A : Type} {C : A → Type} {x y : A} {p : x ≡ y} {cx : C x} {cy : C y}
  → cx ≡ cy [ C ↓ p ] → cy ≡ cx [ C ↓ ! p ]
!ᵈ_ {p = refl} r = ! r

-- Hey, did you remove all the "magic"?