{-# OPTIONS --cubical #-}

open import Cubical.Core.Everything
open import Agda.Builtin.Nat
ℕ = Nat
open import Agda.Builtin.Unit

_×_ : ∀ {ℓ₁ ℓ₂ : Level} (A : Type ℓ₁) (B : Type ℓ₂) → Type (ℓ-max ℓ₁ ℓ₂)
A × B = Σ A (λ _ → B)

is-contr : ∀ {ℓ : Level} (A : Type ℓ) → Type ℓ
is-contr A = Σ A (λ x → ∀ y → x ≡ y)

is-prop : ∀ {ℓ : Level} (A : Type ℓ) → Type ℓ
is-prop A = (x y : A) → x ≡ y

refl : ∀ {ℓ : Level} {A : Type ℓ} {x : A} → x ≡ x
refl {x = x} = λ i → x

_∙_ : ∀ {ℓ : Level} {A : Type ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
_∙_ {A = A} {x = x} p q i = hcomp (λ j → λ { (i = i0) → x ; (i = i1) → q j }) (p i)
infixr 80 _∙_

!_ : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x
!_ p i = p (~ i)
infixr 100 !_

is-equiv = isEquiv

is-eq : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {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 = A} {B = B} f g f-g g-f = record {equiv-proof = λ b → (g b , f-g b) , lemma b} where
  postulate -- to keep this file small
    lemma : ∀ (b : B) (y : Σ A (λ a → f a ≡ b)) → (g b , f-g b) ≡ y

equiv : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {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 {A = A} {B = B} f g f-g g-f = f , is-eq f g f-g g-f

–> : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : Type ℓ₂} → A ≃ B → (A → B)
–> (f , _) = f

<–' : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : Type ℓ₂} {f : A → B} → is-equiv f → (B → A)
<–' iseq b = fst (fst (equiv-proof iseq b))

<– : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : Type ℓ₂} → A ≃ B → (B → A)
<– (_ , iseq) = <–' iseq

<–-inv-r : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : Type ℓ₂} (e : A ≃ B) →
  ∀ b → –> e (<– e b) ≡ b
<–-inv-r (_ , iseq) b = snd (fst (equiv-proof iseq b))

<–-inv-l : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : Type ℓ₂} (e : A ≃ B) →
  ∀ a → <– e (–> e a) ≡ a
<–-inv-l (e @ (_ , iseq)) a i = fst (snd (equiv-proof iseq (–> e a)) (a , refl) i)

-- Task 1: ℕ is the most general ℕ-Alg

ℕ-Alg : ∀ (ℓ : Level) → Type (ℓ-suc ℓ)
ℕ-Alg ℓ = Σ (Type ℓ) (λ X → X × (X → X))

ℕ-Hom : ∀ {ℓ ℓ' : Level} → ℕ-Alg ℓ → ℕ-Alg ℓ' → Type (ℓ-max ℓ ℓ')
ℕ-Hom (X , Xzero , Xsuc) (Y , Yzero , Ysuc) =
  Σ (X → Y) (λ h → (h Xzero ≡ Yzero) × (∀ x → h (Xsuc x) ≡ Ysuc (h x)))

ℕ-ℕ-Alg : ℕ-Alg ℓ-zero
ℕ-ℕ-Alg = ℕ , zero , suc

task1-1 : ∀ {ℓ : Level} (alg : ℕ-Alg ℓ) → ℕ-Hom ℕ-ℕ-Alg alg
task1-1 (X , Xzero , Xsuc) = h , refl , (λ x → refl)  where
  h : ℕ → X
  h zero = Xzero
  h (suc n) = Xsuc (h n)

is-ℕ-initial : ∀ {ℓ₁ : Level} (alg₁ : ℕ-Alg ℓ₁) (ℓ₂ : Level) → Type (ℓ-max ℓ₁ (ℓ-suc ℓ₂))
is-ℕ-initial alg₁ ℓ₂ = (alg₂ : ℕ-Alg ℓ₂) → is-contr (ℕ-Hom alg₁ alg₂)

-- "e @ pattern" is an "as" pattern. For example, the "e @ (x, y)" pattern
-- will bind "e" to the entire pair and also "x" and "y" to individual components.
ℕ-initiality : ∀ {ℓ} → is-ℕ-initial ℕ-ℕ-Alg ℓ
ℕ-initiality (alg @ (X , Xzero , Xsuc)) = task1-1 alg , path where
  path : ∀ (mor : ℕ-Hom ℕ-ℕ-Alg alg) → task1-1 alg ≡ mor
  path (h' , h'-zero , h'-suc) i = task1-2 i , task1-3 i , bonus1 i where
    h = fst (task1-1 alg)
    h-zero = fst (snd (task1-1 alg))
    h-suc = snd (snd (task1-1 alg))

    task1-2 : h ≡ h'
    task1-2 i zero = h'-zero (~ i)
    task1-2 i (suc n) = ((λ i → Xsuc (task1-2 i n)) ∙ (! (h'-suc n))) i

    task1-3 : (λ i → task1-2 i zero ≡ Xzero) [ h-zero ≡ h'-zero ]
    task1-3 i j = h'-zero (~ i ∨ j)

    bonus1 : (λ i → ∀ n → task1-2 i (suc n) ≡ Xsuc (task1-2 i n)) [ h-suc ≡ h'-suc ]
    bonus1 i n = square i where
      square : (λ i → task1-2 i (suc n) ≡ Xsuc (task1-2 i n)) [ h-suc n ≡ h'-suc n ]
      square i j = hfill (λ j → λ { (i = i0) → Xsuc (h n) ; (i = i1) → h'-suc n (~ j) }) (inS (Xsuc (task1-2 i n))) (~ j)

postulate -- remove "postulate" to do the bonus task
  bonus2 :  ∀ {ℓ : Level} (alg : ℕ-Alg ℓ) → is-ℕ-initial alg ℓ-zero → is-ℕ-initial alg ℓ → fst alg ≃ ℕ

-- Task 2: ∥ A ∥ is the best (-1)-type approximating the type A.

data ∥_∥ {ℓ : Level} (A : Type ℓ) : Type ℓ where
  inc : A → ∥ A ∥
  prop : (x y : ∥ A ∥) → x ≡ y

task2-1 : ∥ ℕ ∥ ≃ ⊤
task2-1 = equiv (λ _ → tt) (λ _ → inc zero) (λ _ → refl) (λ _ → prop _ _)

task2-2 : ∀ {ℓ : Level} (A : Type ℓ) → is-prop ∥ A ∥
task2-2 A x y = prop x y

-- Hints: sometimes, there is a simple solution without pattern matching.
task2-3 : ∀ {ℓ : Level} (A : Type ℓ) → ∥ ∥ A ∥ ∥ ≃ ∥ A ∥
task2-3 A = equiv f g f-g g-f where
  f : ∥ ∥ A ∥ ∥ → ∥ A ∥
  f (inc x) = x
  f (prop x y i) = prop (f x) (f y) i

  g : ∥ A ∥ → ∥ ∥ A ∥ ∥
  g a = inc a

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

  g-f : ∀ x → g (f x) ≡ x
  g-f x = prop (g (f x)) x

-- Hints: check out "is-eq".
-- Hints: again, sometimes, there is a simple solution without pattern matching.
task2-4 : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : Type ℓ₂} → is-prop B
  → is-equiv (λ (f : ∥ A ∥ → B) → λ (a : A) → (f (inc a)))
task2-4 {A = A} {B = B} Bprop = is-eq f g f-g g-f where
  f = (λ (m : ∥ A ∥ → B) → λ (a : A) → (m (inc a)))

  g : (A → B) → (∥ A ∥ → B)
  g m (inc x) = m x
  g m (prop x y i) = Bprop (g m x) (g m y) i

  f-g : ∀ m → f (g m) ≡ m
  f-g m i = m

  g-f : ∀ m → g (f m) ≡ m
  g-f m i x = Bprop (g (f m) x) (m x) i

-- Check out <–'.
bonus3 : ∀ {ℓ₁ ℓ₂} (A : Type ℓ₁) {C : Type ℓ₂}
  → (C-inc : A → C) (C-is-prop : is-prop C)
  → ({B : Type ℓ₁} → is-prop B → is-equiv (λ (f : C → B) → λ (a : A) → (f (C-inc a))))
  → C ≃ ∥ A ∥
bonus3 A {C = C} Cinc Cprop univ = equiv f g f-g g-f where
  f : C → ∥ A ∥
  f = <–' (univ prop) inc

  g : ∥ A ∥ → C
  g = <–' (task2-4 Cprop) Cinc

  f-g : ∀ x → f (g x) ≡ x
  f-g x i = prop (f (g x)) x i

  g-f : ∀ x → g (f x) ≡ x
  g-f x i = Cprop (g (f x)) x i

-- Don't forget to kill all "magic" in the file!

-- APPENDIX: examples of higher inductive types
data S¹ : Type₀ where
  base : S¹
  loop : base ≡ base

data T² : Type₀ where
  base : T²
  loop₀ : base ≡ base
  loop₁ : base ≡ base
  surf : (λ i → loop₀ i ≡ loop₀ i) [ loop₁ ≡ loop₁ ]

T²≃S¹×S¹ : T² ≃ S¹ × S¹
T²≃S¹×S¹ = equiv f g f-g g-f where
  f : T² → S¹ × S¹
  f base       = base   , base
  f (loop₀ i)  = loop i , base
  f (loop₁ i)  = base   , loop i
  f (surf i j) = loop i , loop j

  g : S¹ × S¹ → T²
  g (base   , base  ) = base
  g (loop i , base  ) = loop₀ i
  g (base   , loop i) = loop₁ i
  g (loop i , loop j) = surf i j

  f-g : ∀ x → f (g x) ≡ x
  f-g (base   , base)   = refl
  f-g (loop _ , base)   = refl
  f-g (base   , loop _) = refl
  f-g (loop _ , loop _) = refl

  g-f : ∀ x → g (f x) ≡ x
  g-f base       = refl
  g-f (loop₀ _)  = refl
  g-f (loop₁ _)  = refl
  g-f (surf _ _) = refl