{-# OPTIONS --safe #-}

module Multiset.Util.SetTruncation where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
  using
    ( _∘_
    ; const
    )
open import Cubical.Foundations.Equiv

open import Cubical.HITs.SetTruncation as ST
  using
    ( ∥_∥₂
    ; ∣_∣₂
    ; isSetSetTrunc
    )

private
  variable
    ℓ ℓ' : Level
    X A : Type ℓ
    B : X → Type ℓ'

∣_∣₂∗ : ((a : A) → B a) → ((a : A) → ∥ B a ∥₂)
∣ f ∣₂∗ = λ a → ∣ f a ∣₂

mapId : (∣x∣ : ∥ X ∥₂)
  → ST.map (λ x → x) ∣x∣ ≡ ∣x∣
mapId = ST.elim (λ _ → ST.isSetPathImplicit) λ _ → refl

private
  isSetSetPathImplicit : isSet X → {x y : X} → isSet (x ≡ y)
  isSetSetPathImplicit setX = isProp→isSet (setX _ _)

rec∘map : ∀ {ℓy ℓz} {Y : Type ℓy} {Z : Type ℓz}
  → (setZ : isSet Z)
  → (f : X → Y)
  → (g : Y → Z)
  → (x : ∥ X ∥₂)
  → ST.rec setZ g (ST.map f x) ≡ ST.rec setZ (g ∘ f) x
rec∘map setZ f g = ST.elim (λ _ → isSetSetPathImplicit setZ) λ _ → refl

map∘map : ∀ {ℓx ℓy ℓz} {X : Type ℓx} {Y : Type ℓy} {Z : Type ℓz}
  → (f : X → Y)
  → (g : Y → Z)
  → (x : ∥ X ∥₂)
  → ST.map g (ST.map f x) ≡ ST.map (g ∘ f) x
map∘map f g = rec∘map isSetSetTrunc f (∣_∣₂ ∘ g)

map2 : ∀ {ℓy ℓz} {Y : Type ℓy} {Z : Type ℓz}
  → (f : X → Y → Z)
  → ∥ X ∥₂ → ∥ Y ∥₂ → ∥ Z ∥₂
map2 f = ST.rec2 ST.isSetSetTrunc λ x y → ∣ f x y ∣₂

rec∘map2 : ∀ {ℓy ℓz ℓw} {Y : Type ℓy} {Z : Type ℓz} {W : Type ℓw}
  → (setZ : isSet Z)
  → (f : X → W → Y)
  → (g : Y → Z)
  → (x : ∥ X ∥₂)
  → (w : ∥ W ∥₂)
  → ST.rec setZ g (map2 f x w) ≡ ST.rec2 setZ (λ x w → g (f x w)) x w
rec∘map2 {Z = Z} setZ f g = ST.elim2 (λ _ _ → isSetSetPathImplicit setZ) λ _ _ → refl

map∘map2 : ∀ {ℓy ℓz ℓw} {Y : Type ℓy} {Z : Type ℓz} {W : Type ℓw}
  → (g : Y → Z)
  → (f : X → W → Y)
  → (x : ∥ X ∥₂)
  → (w : ∥ W ∥₂)
  → ST.map g (map2 f x w) ≡ map2 (λ x w → g (f x w)) x w
map∘map2 g f = rec∘map2 ST.isSetSetTrunc f (∣_∣₂ ∘ g)

rec2ConstLeft :  ∀ {ℓz ℓw} {Z : Type ℓz} {W : Type ℓw}
  → (setZ : isSet Z)
  → (f : W → Z)
  → (x : ∥ X ∥₂)
  → (w : ∥ W ∥₂)
  → ST.rec2 setZ (λ x w → f w) x w ≡ ST.rec setZ f w
rec2ConstLeft setZ f = ST.elim2 (λ _ _ → isSetSetPathImplicit setZ) (λ _ _ → refl)

rec2ConstRight : ∀ {ℓz ℓw} {Z : Type ℓz} {W : Type ℓw}
  → (setZ : isSet Z)
  → (f : X → Z)
  → (x : ∥ X ∥₂)
  → (w : ∥ W ∥₂)
  → ST.rec2 setZ (λ x w → f x) x w ≡ ST.rec setZ f x
rec2ConstRight setZ f = ST.elim2 (λ _ _ → isSetSetPathImplicit setZ) (λ _ _ → refl)

map2ConstLeft : ∀ {ℓz ℓw} {Z : Type ℓz} {W : Type ℓw}
  → (f : W → Z)
  → (x : ∥ X ∥₂)
  → (w : ∥ W ∥₂)
  → map2 (λ x w → f w) x w ≡ ST.map f w
map2ConstLeft f = rec2ConstLeft ST.isSetSetTrunc (∣_∣₂ ∘ f)

map2IdRight : ∀ {ℓw} {W : Type ℓw}
  → (x : ∥ X ∥₂)
  → (w : ∥ W ∥₂)
  → map2 (λ x w → x) x w ≡ x
map2IdRight = ST.elim2 (λ _ _ → ST.isSetPathImplicit) (λ _ _ → refl)

setTruncIso : {A : Type ℓ} {B : Type ℓ'}
  → Iso A B
  → Iso ∥ A ∥₂ ∥ B ∥₂
setTruncIso {A = A} {B = B} isom = ∥isom∥ where
  open Iso

  ∥isom∥ : Iso _ _
  fun ∥isom∥ = ST.map (isom .fun)
  inv ∥isom∥ = ST.map (isom .inv)
  rightInv ∥isom∥ = ST.elim (λ _ → isProp→isSet (ST.squash₂ _ _)) (cong ∣_∣₂ ∘ isom .rightInv)
  leftInv ∥isom∥ = ST.elim (λ _ → isProp→isSet (ST.squash₂ _ _)) (cong ∣_∣₂ ∘ isom .leftInv)

setTruncEquiv : {A : Type ℓ} {B : Type ℓ'}
  → A ≃ B
  → ∥ A ∥₂ ≃ ∥ B ∥₂
setTruncEquiv {A = A} {B = B} e = isoToEquiv (setTruncIso (equivToIso e))