{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.PropositionalTruncation.Properties where
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation.Base
private
variable
ℓ : Level
A B C : Type ℓ
∥∥-isPropDep : (P : A → Type ℓ) → isOfHLevelDep 1 (λ x → ∥ P x ∥)
∥∥-isPropDep P = isOfHLevel→isOfHLevelDep 1 (λ _ → squash)
rec : {P : Type ℓ} → isProp P → (A → P) → ∥ A ∥ → P
rec Pprop f ∣ x ∣ = f x
rec Pprop f (squash x y i) = Pprop (rec Pprop f x) (rec Pprop f y) i
rec2 : {P : Type ℓ} → isProp P → (A → A → P) → ∥ A ∥ → ∥ A ∥ → P
rec2 Pprop f ∣ x ∣ ∣ y ∣ = f x y
rec2 Pprop f ∣ x ∣ (squash y z i) = Pprop (rec2 Pprop f ∣ x ∣ y) (rec2 Pprop f ∣ x ∣ z) i
rec2 Pprop f (squash x y i) z = Pprop (rec2 Pprop f x z) (rec2 Pprop f y z) i
elim : {P : ∥ A ∥ → Type ℓ} → ((a : ∥ A ∥) → isProp (P a))
→ ((x : A) → P ∣ x ∣) → (a : ∥ A ∥) → P a
elim Pprop f ∣ x ∣ = f x
elim Pprop f (squash x y i) =
isOfHLevel→isOfHLevelDep 1 Pprop
(elim Pprop f x) (elim Pprop f y) (squash x y) i
elim2 : {P : ∥ A ∥ → ∥ A ∥ → Type ℓ}
(Bset : ((x y : ∥ A ∥) → isProp (P x y)))
(f : (a b : A) → P ∣ a ∣ ∣ b ∣)
(x y : ∥ A ∥) → P x y
elim2 Pprop f = elim (λ _ → isPropΠ (λ _ → Pprop _ _))
(λ a → elim (λ _ → Pprop _ _) (f a))
elim3 : {P : ∥ A ∥ → ∥ A ∥ → ∥ A ∥ → Type ℓ}
(Bset : ((x y z : ∥ A ∥) → isProp (P x y z)))
(g : (a b c : A) → P (∣ a ∣) ∣ b ∣ ∣ c ∣)
(x y z : ∥ A ∥) → P x y z
elim3 Pprop g = elim2 (λ _ _ → isPropΠ (λ _ → Pprop _ _ _))
(λ a b → elim (λ _ → Pprop _ _ _) (g a b))
propTruncIsProp : isProp ∥ A ∥
propTruncIsProp x y = squash x y
propTruncIdempotent≃ : isProp A → ∥ A ∥ ≃ A
propTruncIdempotent≃ {A = A} hA = isoToEquiv f
where
f : Iso ∥ A ∥ A
Iso.fun f = rec hA (idfun A)
Iso.inv f x = ∣ x ∣
Iso.rightInv f _ = refl
Iso.leftInv f = elim (λ _ → isProp→isSet propTruncIsProp _ _) (λ _ → refl)
propTruncIdempotent : isProp A → ∥ A ∥ ≡ A
propTruncIdempotent hA = ua (propTruncIdempotent≃ hA)
elim' : {P : ∥ A ∥ → Type ℓ} → ((a : ∥ A ∥) → isProp (P a)) →
((x : A) → P ∣ x ∣) → (a : ∥ A ∥) → P a
elim' {P = P} Pprop f a =
rec (Pprop a) (λ x → transp (λ i → P (squash ∣ x ∣ a i)) i0 (f x)) a
map : (A → B) → (∥ A ∥ → ∥ B ∥)
map f = rec squash (∣_∣ ∘ f)
map2 : (A → B → C) → (∥ A ∥ → ∥ B ∥ → ∥ C ∥)
map2 f = rec (isPropΠ λ _ → squash) (map ∘ f)
module SetElim (Bset : isSet B) where
Bset' : isSet' B
Bset' = isSet→isSet' Bset
rec→Set : (f : A → B) (kf : 2-Constant f) → ∥ A ∥ → B
helper : (f : A → B) (kf : 2-Constant f) → (t u : ∥ A ∥)
→ rec→Set f kf t ≡ rec→Set f kf u
rec→Set f kf ∣ x ∣ = f x
rec→Set f kf (squash t u i) = helper f kf t u i
helper f kf ∣ x ∣ ∣ y ∣ = kf x y
helper f kf (squash t u i) v
= Bset' (helper f kf t v) (helper f kf u v) (helper f kf t u) refl i
helper f kf t (squash u v i)
= Bset' (helper f kf t u) (helper f kf t v) refl (helper f kf u v) i
kcomp : (f : ∥ A ∥ → B) → 2-Constant (f ∘ ∣_∣)
kcomp f x y = cong f (squash ∣ x ∣ ∣ y ∣)
Fset : isSet (A → B)
Fset = isSetΠ (const Bset)
Kset : (f : A → B) → isSet (2-Constant f)
Kset f = isSetΠ (λ _ → isSetΠ (λ _ → isProp→isSet (Bset _ _)))
setRecLemma
: (f : ∥ A ∥ → B)
→ rec→Set (f ∘ ∣_∣) (kcomp f) ≡ f
setRecLemma f i t
= elim {P = λ t → rec→Set (f ∘ ∣_∣) (kcomp f) t ≡ f t}
(λ t → Bset _ _) (λ x → refl) t i
mkKmap : (∥ A ∥ → B) → Σ (A → B) 2-Constant
mkKmap f = f ∘ ∣_∣ , kcomp f
fib : (g : Σ (A → B) 2-Constant) → fiber mkKmap g
fib (g , kg) = rec→Set g kg , refl
eqv : (g : Σ (A → B) 2-Constant) → ∀ fi → fib g ≡ fi
eqv g (f , p) =
Σ≡Prop (λ f → isOfHLevelΣ 2 Fset Kset _ _)
(cong (uncurry rec→Set) (sym p) ∙ setRecLemma f)
trunc→Set≃ : (∥ A ∥ → B) ≃ (Σ (A → B) 2-Constant)
trunc→Set≃ .fst = mkKmap
trunc→Set≃ .snd .equiv-proof g = fib g , eqv g
e : B → Σ (A → B) 2-Constant
e b = const b , λ _ _ → refl
eval : A → (γ : Σ (A → B) 2-Constant) → B
eval a₀ (g , _) = g a₀
e-eval : ∀ (a₀ : A) γ → e (eval a₀ γ) ≡ γ
e-eval a₀ (g , kg) i .fst a₁ = kg a₀ a₁ i
e-eval a₀ (g , kg) i .snd a₁ a₂ = Bset' refl (kg a₁ a₂) (kg a₀ a₁) (kg a₀ a₂) i
e-isEquiv : A → isEquiv (e {A = A})
e-isEquiv a₀ = isoToIsEquiv (iso e (eval a₀) (e-eval a₀) λ _ → refl)
preEquiv₁ : ∥ A ∥ → B ≃ Σ (A → B) 2-Constant
preEquiv₁ t = e , rec (isPropIsEquiv e) e-isEquiv t
preEquiv₂ : (∥ A ∥ → Σ (A → B) 2-Constant) ≃ Σ (A → B) 2-Constant
preEquiv₂ = isoToEquiv (iso to const (λ _ → refl) retr)
where
to : (∥ A ∥ → Σ (A → B) 2-Constant) → Σ (A → B) 2-Constant
to f .fst x = f ∣ x ∣ .fst x
to f .snd x y i = f (squash ∣ x ∣ ∣ y ∣ i) .snd x y i
retr : retract to const
retr f i t .fst x = f (squash ∣ x ∣ t i) .fst x
retr f i t .snd x y
= Bset'
(λ j → f (squash ∣ x ∣ ∣ y ∣ j) .snd x y j)
(f t .snd x y)
(λ j → f (squash ∣ x ∣ t j) .fst x)
(λ j → f (squash ∣ y ∣ t j) .fst y)
i
trunc→Set≃₂ : (∥ A ∥ → B) ≃ Σ (A → B) 2-Constant
trunc→Set≃₂ = compEquiv (equivΠCod preEquiv₁) preEquiv₂
open SetElim public using (rec→Set; trunc→Set≃)
elim→Set
: {P : ∥ A ∥ → Type ℓ}
→ (∀ t → isSet (P t))
→ (f : (x : A) → P ∣ x ∣)
→ (kf : ∀ x y → PathP (λ i → P (squash ∣ x ∣ ∣ y ∣ i)) (f x) (f y))
→ (t : ∥ A ∥) → P t
elim→Set {A = A} {P = P} Pset f kf t
= rec→Set (Pset t) g gk t
where
g : A → P t
g x = transp (λ i → P (squash ∣ x ∣ t i)) i0 (f x)
gk : 2-Constant g
gk x y i = transp (λ j → P (squash (squash ∣ x ∣ ∣ y ∣ i) t j)) i0 (kf x y i)
RecHProp : (P : A → hProp ℓ) (kP : ∀ x y → P x ≡ P y) → ∥ A ∥ → hProp ℓ
RecHProp P kP = rec→Set isSetHProp P kP
module GpdElim (Bgpd : isGroupoid B) where
Bgpd' : isGroupoid' B
Bgpd' = isGroupoid→isGroupoid' Bgpd
module _ (f : A → B) (3kf : 3-Constant f) where
open 3-Constant 3kf
rec→Gpd : ∥ A ∥ → B
pathHelper : (t u : ∥ A ∥) → rec→Gpd t ≡ rec→Gpd u
triHelper₁
: (t u v : ∥ A ∥)
→ Square (pathHelper t u) (pathHelper t v) refl (pathHelper u v)
triHelper₂
: (t u v : ∥ A ∥)
→ Square (pathHelper t v) (pathHelper u v) (pathHelper t u) refl
rec→Gpd ∣ x ∣ = f x
rec→Gpd (squash t u i) = pathHelper t u i
pathHelper ∣ x ∣ ∣ y ∣ = link x y
pathHelper (squash t u j) v = triHelper₂ t u v j
pathHelper ∣ x ∣ (squash u v j) = triHelper₁ ∣ x ∣ u v j
triHelper₁ ∣ x ∣ ∣ y ∣ ∣ z ∣ = coh₁ x y z
triHelper₁ (squash s t i) u v
= Bgpd'
(triHelper₁ s u v)
(triHelper₁ t u v)
(triHelper₂ s t u)
(triHelper₂ s t v)
(λ i → refl)
(λ i → pathHelper u v)
i
triHelper₁ ∣ x ∣ (squash t u i) v
= Bgpd'
(triHelper₁ ∣ x ∣ t v)
(triHelper₁ ∣ x ∣ u v)
(triHelper₁ ∣ x ∣ t u)
(λ i → pathHelper ∣ x ∣ v)
(λ i → refl)
(triHelper₂ t u v)
i
triHelper₁ ∣ x ∣ ∣ y ∣ (squash u v i)
= Bgpd'
(triHelper₁ ∣ x ∣ ∣ y ∣ u)
(triHelper₁ ∣ x ∣ ∣ y ∣ v)
(λ i → link x y)
(triHelper₁ ∣ x ∣ u v)
(λ i → refl)
(triHelper₁ ∣ y ∣ u v)
i
triHelper₂ ∣ x ∣ ∣ y ∣ ∣ z ∣ = coh₂ x y z
triHelper₂ (squash s t i) u v
= Bgpd'
(triHelper₂ s u v)
(triHelper₂ t u v)
(triHelper₂ s t v)
(λ i → pathHelper u v)
(triHelper₂ s t u)
(λ i → refl)
i
triHelper₂ ∣ x ∣ (squash t u i) v
= Bgpd'
(triHelper₂ ∣ x ∣ t v)
(triHelper₂ ∣ x ∣ u v)
(λ i → pathHelper ∣ x ∣ v)
(triHelper₂ t u v)
(triHelper₁ ∣ x ∣ t u)
(λ i → refl)
i
triHelper₂ ∣ x ∣ ∣ y ∣ (squash u v i)
= Bgpd'
(triHelper₂ ∣ x ∣ ∣ y ∣ u)
(triHelper₂ ∣ x ∣ ∣ y ∣ v)
(triHelper₁ ∣ x ∣ u v)
(triHelper₁ ∣ y ∣ u v)
(λ i → link x y)
(λ i → refl)
i
preEquiv₁ : (∥ A ∥ → Σ (A → B) 3-Constant) ≃ Σ (A → B) 3-Constant
preEquiv₁ = isoToEquiv (iso fn const (λ _ → refl) retr)
where
open 3-Constant
fn : (∥ A ∥ → Σ (A → B) 3-Constant) → Σ (A → B) 3-Constant
fn f .fst x = f ∣ x ∣ .fst x
fn f .snd .link x y i = f (squash ∣ x ∣ ∣ y ∣ i) .snd .link x y i
fn f .snd .coh₁ x y z i j
= f (squash ∣ x ∣ (squash ∣ y ∣ ∣ z ∣ i) j) .snd .coh₁ x y z i j
retr : retract fn const
retr f i t .fst x = f (squash ∣ x ∣ t i) .fst x
retr f i t .snd .link x y j
= f (squash (squash ∣ x ∣ ∣ y ∣ j) t i) .snd .link x y j
retr f i t .snd .coh₁ x y z
= Bgpd'
(λ k j → f (cb k j i0) .snd .coh₁ x y z k j )
(λ k j → f (cb k j i1) .snd .coh₁ x y z k j)
(λ k j → f (cb i0 j k) .snd .link x y j)
(λ k j → f (cb i1 j k) .snd .link x z j)
(λ _ → refl)
(λ k j → f (cb j i1 k) .snd .link y z j)
i
where
cb : I → I → I → ∥ _ ∥
cb i j k = squash (squash ∣ x ∣ (squash ∣ y ∣ ∣ z ∣ i) j) t k
e : B → Σ (A → B) 3-Constant
e b .fst _ = b
e b .snd = record
{ link = λ _ _ _ → b
; coh₁ = λ _ _ _ _ _ → b
}
eval : A → Σ (A → B) 3-Constant → B
eval a₀ (g , _) = g a₀
module _ where
open 3-Constant
e-eval : ∀(a₀ : A) γ → e (eval a₀ γ) ≡ γ
e-eval a₀ (g , 3kg) i .fst x = 3kg .link a₀ x i
e-eval a₀ (g , 3kg) i .snd .link x y = λ j → 3kg .coh₁ a₀ x y j i
e-eval a₀ (g , 3kg) i .snd .coh₁ x y z
= Bgpd'
(λ _ _ → g a₀)
(3kg .coh₁ x y z)
(λ k j → 3kg .coh₁ a₀ x y j k)
(λ k j → 3kg .coh₁ a₀ x z j k)
(λ _ → refl)
(λ k j → 3kg .coh₁ a₀ y z j k)
i
e-isEquiv : A → isEquiv (e {A = A})
e-isEquiv a₀ = isoToIsEquiv (iso e (eval a₀) (e-eval a₀) λ _ → refl)
preEquiv₂ : ∥ A ∥ → B ≃ Σ (A → B) 3-Constant
preEquiv₂ t = e , rec (isPropIsEquiv e) e-isEquiv t
trunc→Gpd≃ : (∥ A ∥ → B) ≃ Σ (A → B) 3-Constant
trunc→Gpd≃ = compEquiv (equivΠCod preEquiv₂) preEquiv₁
open GpdElim using (rec→Gpd; trunc→Gpd≃) public
squashᵗ
: ∀(x y z : A)
→ Square (squash ∣ x ∣ ∣ y ∣) (squash ∣ x ∣ ∣ z ∣) refl (squash ∣ y ∣ ∣ z ∣)
squashᵗ x y z i = squash ∣ x ∣ (squash ∣ y ∣ ∣ z ∣ i)
elim→Gpd
: (P : ∥ A ∥ → Type ℓ)
→ (∀ t → isGroupoid (P t))
→ (f : (x : A) → P ∣ x ∣)
→ (kf : ∀ x y → PathP (λ i → P (squash ∣ x ∣ ∣ y ∣ i)) (f x) (f y))
→ (3kf : ∀ x y z
→ SquareP (λ i j → P (squashᵗ x y z i j)) (kf x y) (kf x z) refl (kf y z))
→ (t : ∥ A ∥) → P t
elim→Gpd {A = A} P Pgpd f kf 3kf t = rec→Gpd (Pgpd t) g 3kg t
where
g : A → P t
g x = transp (λ i → P (squash ∣ x ∣ t i)) i0 (f x)
open 3-Constant
3kg : 3-Constant g
3kg .link x y i
= transp (λ j → P (squash (squash ∣ x ∣ ∣ y ∣ i) t j)) i0 (kf x y i)
3kg .coh₁ x y z i j
= transp (λ k → P (squash (squashᵗ x y z i j) t k)) i0 (3kf x y z i j)
RecHSet : (P : A → TypeOfHLevel ℓ 2) → 3-Constant P → ∥ A ∥ → TypeOfHLevel ℓ 2
RecHSet P 3kP = rec→Gpd (isOfHLevelTypeOfHLevel 2) P 3kP