{-# 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.
-}
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.
-}
-- Remember to remove all 'magic'!