{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Everything
open import Cubical.Data.Unit
open import Cubical.HITs.PropositionalTruncation renaming (elim to ∥∥-elim)
open import Cubical.HITs.SetQuotients renaming (elim to /-elim)

module _ {ℓ₁ ℓ₂} (A : Type ℓ₁) (B : Type ℓ₂) (Bset : isSet B)
  (f : A → B) (fConst : ∀ a₁ a₂ → f a₁ ≡ f a₂) where

  SquashedA : Type ℓ₁
  SquashedA = A / λ _ _ → Unit

  -- Uses elimProp from Cubical.HITs.SetQuotients
  SquashedAIsProp : ∀ (x y : SquashedA) → x ≡ y
  SquashedAIsProp = elimProp
    {B = λ x → ∀ (y : SquashedA) → x ≡ y}
    (λ x → isPropΠ (λ y → squash/ x y))
    (λ a → elimProp
      {B = λ y → [ a ] ≡ y}
      (λ y → squash/ [ a ] y)
      (λ b → eq/ a b tt))

  -- Use elim from Cubical.HITs.SetQuotients (renamed to /-elim)
  task1 : SquashedA → B
  task1 = /-elim (λ _ → Bset) f (λ a b _ → fConst a b)

  -- Use elim from Cubical.HITs.PropositionalTruncation (renamed to ∥∥-elim)
  task2 : ∥ A ∥ → SquashedA
  task2 = ∥∥-elim (λ _ → SquashedAIsProp) [_]

  task3 : ∥ A ∥ → B
  task3 = task1 ∘ task2

  {- Task 4:

  Try to prove the following lemma "directly" without SquashedA,
  using the pattern matching. Favonia expects that you would be
  stuck, but why?

  task4-stuck : ∥ A ∥ → B
  task4-stuck ∣ a ∣ = f a
  task4-stuck (squash x y i) = ?

  What are the difficulties you encountered? How did we avoid this
  with SquashedA? Please reflect upon Tasks 1 and 2.

  <YOUR REFLECTION HERE>

  -}

  task5 : task3 ∘ ∣_∣ ≡ f
  task5 = refl

  {- Task 6:

  In one or two sentences, explain the significance of your answer to Task 5:
  There is something more than the typing of task5 is telling you.

  <YOUR REFLECTION UPON SOMETHING NOT KNOWN BY THE TYPING>

  -}

  -- Remember to remove all 'magic'!