{-# OPTIONS --erased-cubical --safe #-}
import Equality.Path as P
module H-level.Truncation.Propositional.Non-recursive
{e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where
private
open module PD = P.Derived-definitions-and-properties eq
hiding (elim)
open import Prelude
open import Colimit.Sequential eq as C using (Colimit)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F
open import H-level equality-with-J
open import H-level.Closure equality-with-J
import H-level.Truncation.Propositional eq as T
open import H-level.Truncation.Propositional.Non-recursive.Erased eq
as N using (∥_∥ᴱ)
open import H-level.Truncation.Propositional.One-step eq as O
using (∥_∥¹; ∥_∥¹-out-^; ∣_∣-out-^)
private
variable
a p : Level
A B : Type a
P : A → Type p
e x : A
∥_∥ : Type a → Type a
∥ A ∥ = Colimit ∥ A ∥¹-out-^ O.∣_∣
∣_∣ : A → ∥ A ∥
∣_∣ = C.∣_∣
record Elim {A : Type a} (P : ∥ A ∥ → Type p) : Type (a ⊔ p) where
no-eta-equality
field
∣∣ʳ : ∀ x → P ∣ x ∣
is-propositionʳ : ∀ x → Is-proposition (P x)
open Elim public
elim : Elim P → (x : ∥ A ∥) → P x
elim {A} {P} e = C.elim λ where
.C.Elim.∣∣ʳ {n} → helper n
.C.Elim.∣∣≡∣∣ʳ _ → E.is-propositionʳ _ _ _
where
module E = Elim e
helper : ∀ n (x : ∥ A ∥¹-out-^ n) → P C.∣ x ∣
helper zero = E.∣∣ʳ
helper (suc n) = O.elim λ where
.O.Elim.∣∣ʳ x → subst P (sym (C.∣∣≡∣∣ x)) (helper n x)
.O.Elim.∣∣-constantʳ _ _ → E.is-propositionʳ _ _ _
_ : elim e ∣ x ∣ ≡ e .∣∣ʳ x
_ = refl _
∥∥-proposition : Is-proposition ∥ A ∥
∥∥-proposition {A} = elim λ where
.is-propositionʳ → Π≡-proposition ext
.∣∣ʳ x → C.elim λ where
.C.Elim.∣∣ʳ → lemma₁ _ x
.C.Elim.∣∣≡∣∣ʳ {n} y →
subst (∣ x ∣ ≡_) (C.∣∣≡∣∣ y) (lemma₁ (suc n) x O.∣ y ∣) ≡⟨ sym trans-subst ⟩
trans (lemma₁ (1 + n) x O.∣ y ∣) (C.∣∣≡∣∣ y) ≡⟨⟩
trans (trans (sym (trans (C.∣∣≡∣∣ (∣ x ∣-out-^ (1 + n)))
(lemma₀ (1 + n) x)))
(trans (cong C.∣_∣
(O.∣∣-constant
(∣ x ∣-out-^ (1 + n)) O.∣ y ∣))
(C.∣∣≡∣∣ O.∣ y ∣)))
(C.∣∣≡∣∣ y) ≡⟨ trans (cong (λ eq → trans (trans eq
(trans (cong C.∣_∣ (O.∣∣-constant _ _))
(C.∣∣≡∣∣ _)))
(C.∣∣≡∣∣ _)) $
sym-trans _ _) $
trans (trans-assoc _ _ _) $
trans (trans-assoc _ _ _) $
cong (trans (sym (lemma₀ (1 + n) _))) $
sym $ trans-assoc _ _ _ ⟩
trans (sym (lemma₀ (1 + n) x))
(trans (trans (sym (C.∣∣≡∣∣ (∣ x ∣-out-^ (1 + n))))
(trans (cong C.∣_∣
(O.∣∣-constant
(∣ x ∣-out-^ (1 + n)) O.∣ y ∣))
(C.∣∣≡∣∣ O.∣ y ∣)))
(C.∣∣≡∣∣ y)) ≡⟨ cong (λ eq → trans (sym (lemma₀ (1 + n) _))
(trans (trans (sym (C.∣∣≡∣∣ _)) eq) (C.∣∣≡∣∣ _))) $ sym $
lemma₂ _ _ _ _ _ ⟩
trans (sym (lemma₀ (1 + n) x))
(trans (trans (sym (C.∣∣≡∣∣ (∣ x ∣-out-^ (1 + n))))
(trans (C.∣∣≡∣∣ (∣ x ∣-out-^ (1 + n)))
(cong C.∣_∣ (O.∣∣-constant _ _))))
(C.∣∣≡∣∣ y)) ≡⟨ cong (λ eq → trans (sym (lemma₀ (1 + n) _)) (trans eq (C.∣∣≡∣∣ _))) $
trans-sym-[trans] _ _ ⟩
trans (sym (lemma₀ (1 + n) x))
(trans (cong C.∣_∣ (O.∣∣-constant _ _)) (C.∣∣≡∣∣ y)) ≡⟨⟩
lemma₁ n x y ∎
where
lemma₀ : ∀ n (x : A) → C.∣ ∣ x ∣-out-^ n ∣ ≡ ∣ x ∣
lemma₀ zero x = ∣ x ∣ ∎
lemma₀ (suc n) x =
C.∣ O.∣ ∣ x ∣-out-^ n ∣ ∣ ≡⟨ C.∣∣≡∣∣ (∣ x ∣-out-^ n) ⟩
C.∣ ∣ x ∣-out-^ n ∣ ≡⟨ lemma₀ n x ⟩∎
∣ x ∣ ∎
lemma₁ : ∀ n (x : A) (y : ∥ A ∥¹-out-^ n) → ∣ x ∣ ≡ C.∣ y ∣
lemma₁ n x y =
∣ x ∣ ≡⟨ sym (lemma₀ (suc n) x) ⟩
C.∣ ∣ x ∣-out-^ (suc n) ∣ ≡⟨⟩
C.∣ O.∣ ∣ x ∣-out-^ n ∣ ∣ ≡⟨ cong C.∣_∣ (O.∣∣-constant _ _) ⟩
C.∣ O.∣ y ∣ ∣ ≡⟨ C.∣∣≡∣∣ y ⟩∎
C.∣ y ∣ ∎
lemma₂ :
∀ n (x y : ∥ A ∥¹-out-^ n) (p : x ≡ y) (q : O.∣ x ∣ ≡ O.∣ y ∣) →
trans (C.∣∣≡∣∣ {P = ∥ A ∥¹-out-^} x) (cong C.∣_∣ p) ≡
trans (cong C.∣_∣ q) (C.∣∣≡∣∣ y)
lemma₂ n x y p q =
trans (C.∣∣≡∣∣ x) (cong C.∣_∣ p) ≡⟨ PD.elim
(λ {x y} p → trans (C.∣∣≡∣∣ x) (cong C.∣_∣ p) ≡
trans (cong C.∣_∣ (cong O.∣_∣ p)) (C.∣∣≡∣∣ y))
(λ x →
trans (C.∣∣≡∣∣ x) (cong C.∣_∣ (refl _)) ≡⟨ cong (trans _) $ cong-refl _ ⟩
trans (C.∣∣≡∣∣ x) (refl _) ≡⟨ trans-reflʳ _ ⟩
C.∣∣≡∣∣ x ≡⟨ sym $ trans-reflˡ _ ⟩
trans (refl _) (C.∣∣≡∣∣ x) ≡⟨ cong (flip trans _) $ sym $
trans (cong (cong C.∣_∣) $ cong-refl _) $
cong-refl _ ⟩∎
trans (cong C.∣_∣ (cong O.∣_∣ (refl _))) (C.∣∣≡∣∣ x) ∎)
p ⟩
trans (cong C.∣_∣ (cong O.∣_∣ p)) (C.∣∣≡∣∣ y) ≡⟨ cong (flip trans _) $
cong-preserves-Constant
(λ u v →
C.∣ u ∣ ≡⟨ sym (C.∣∣≡∣∣ u) ⟩
C.∣ O.∣ u ∣ ∣ ≡⟨ cong C.∣_∣ (O.∣∣-constant _ _) ⟩
C.∣ O.∣ v ∣ ∣ ≡⟨ C.∣∣≡∣∣ v ⟩∎
C.∣ v ∣ ∎)
_ _ ⟩∎
trans (cong C.∣_∣ q) (C.∣∣≡∣∣ y) ∎
∥∥≃∥∥ : ∥ A ∥ ≃ T.∥ A ∥
∥∥≃∥∥ = Eq.⇔→≃
∥∥-proposition
T.truncation-is-proposition
(elim λ where
.∣∣ʳ → T.∣_∣
.is-propositionʳ _ → T.truncation-is-proposition)
(T.rec ∥∥-proposition ∣_∣)
∥∥→≃ :
(T.∥ A ∥ → B)
≃
(∃ λ (f : ∀ n → ∥ A ∥¹-out-^ n → B) →
∀ n x → f (suc n) O.∣ x ∣ ≡ f n x)
∥∥→≃ {A} {B} =
(T.∥ A ∥ → B) ↝⟨ →-cong ext (inverse ∥∥≃∥∥) F.id ⟩
(∥ A ∥ → B) ↝⟨ C.universal-property ⟩□
(∃ λ (f : ∀ n → ∥ A ∥¹-out-^ n → B) →
∀ n x → f (suc n) O.∣ x ∣ ≡ f n x) □
∥∥ᴱ→∥∥ : ∥ A ∥ᴱ → ∥ A ∥
∥∥ᴱ→∥∥ = N.elim λ where
.N.∣∣ʳ → ∣_∣
.N.is-propositionʳ _ → ∥∥-proposition
@0 ∥∥ᴱ≃∥∥ : ∥ A ∥ᴱ ≃ ∥ A ∥
∥∥ᴱ≃∥∥ = Eq.↔→≃
∥∥ᴱ→∥∥
(elim λ @0 where
.∣∣ʳ → N.∣_∣
.is-propositionʳ _ → N.∥∥ᴱ-proposition)
(elim λ @0 where
.∣∣ʳ _ → refl _
.is-propositionʳ _ → mono₁ 1 ∥∥-proposition)
(N.elim λ where
.N.∣∣ʳ _ → refl _
.N.is-propositionʳ _ → mono₁ 1 N.∥∥ᴱ-proposition)