{-# OPTIONS --erased-cubical --safe #-}
import Equality.Path as P
module H-level.Truncation.Propositional.Erased
{e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where
open P.Derived-definitions-and-properties eq hiding (elim)
open import Prelude as P
open import Logical-equivalence using (_⇔_)
open import Bijection equality-with-J as Bijection using (_↔_)
import Colimit.Sequential.Very-erased eq as C
open import Embedding equality-with-J as Emb using (Is-embedding)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
using (_≃_; Is-equivalence)
open import Equivalence.Erased equality-with-J as EEq
using (_≃ᴱ_; Is-equivalenceᴱ)
open import Equivalence.Erased.Contractible-preimages equality-with-J
as ECP using (Contractibleᴱ; _⁻¹ᴱ_)
open import Equivalence-relation equality-with-J
open import Erased.Cubical eq as Er using (Erased; [_])
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional.One-step eq as O
using (∥_∥¹-out-^)
import H-level.Truncation.Propositional.Non-recursive.Erased eq as N
open import Monad equality-with-J
open import Preimage equality-with-J using (_⁻¹_)
open import Surjection equality-with-J using (_↠_; Split-surjective)
private
variable
a b ℓ p r : Level
A A₁ A₂ B B₁ B₂ C : Type a
P Q : A → Type p
R : A → A → Type r
f g k x y : A
data ∥_∥ᴱ (A : Type a) : Type a where
∣_∣ : A → ∥ A ∥ᴱ
@0 truncation-is-propositionᴾ : P.Is-proposition ∥ A ∥ᴱ
@0 truncation-is-proposition : Is-proposition ∥ A ∥ᴱ
truncation-is-proposition =
_↔_.from (H-level↔H-level 1) truncation-is-propositionᴾ
record Elimᴾ′ {A : Type a} (P : ∥ A ∥ᴱ → Type p) : Type (a ⊔ p) where
no-eta-equality
field
∣∣ʳ : (x : A) → P ∣ x ∣
@0 truncation-is-propositionʳ :
(p : P x) (q : P y) →
P.[ (λ i → P (truncation-is-propositionᴾ x y i)) ] p ≡ q
open Elimᴾ′ public
elimᴾ′ : Elimᴾ′ P → (x : ∥ A ∥ᴱ) → P x
elimᴾ′ {A = A} {P = P} e = helper
where
module E = Elimᴾ′ e
helper : (x : ∥ A ∥ᴱ) → P x
helper ∣ x ∣ = E.∣∣ʳ x
helper (truncation-is-propositionᴾ x y i) =
E.truncation-is-propositionʳ (helper x) (helper y) i
record Elimᴾ {A : Type a} (P : ∥ A ∥ᴱ → Type p) : Type (a ⊔ p) where
no-eta-equality
field
∣∣ʳ : (x : A) → P ∣ x ∣
@0 truncation-is-propositionʳ :
(x : ∥ A ∥ᴱ) → P.Is-proposition (P x)
open Elimᴾ public
elimᴾ : Elimᴾ P → (x : ∥ A ∥ᴱ) → P x
elimᴾ e = elimᴾ′ λ where
.∣∣ʳ → E.∣∣ʳ
.truncation-is-propositionʳ _ _ →
P.heterogeneous-irrelevance E.truncation-is-propositionʳ
where
module E = Elimᴾ e
record Recᴾ (A : Type a) (B : Type b) : Type (a ⊔ b) where
no-eta-equality
field
∣∣ʳ : A → B
@0 truncation-is-propositionʳ : P.Is-proposition B
open Recᴾ public
recᴾ : Recᴾ A B → ∥ A ∥ᴱ → B
recᴾ r = elimᴾ λ where
.∣∣ʳ → R.∣∣ʳ
.truncation-is-propositionʳ _ → R.truncation-is-propositionʳ
where
module R = Recᴾ r
record Elim {A : Type a} (P : ∥ A ∥ᴱ → Type p) : Type (a ⊔ p) where
no-eta-equality
field
∣∣ʳ : (x : A) → P ∣ x ∣
@0 truncation-is-propositionʳ :
(x : ∥ A ∥ᴱ) → Is-proposition (P x)
open Elim public
elim : Elim P → (x : ∥ A ∥ᴱ) → P x
elim e = elimᴾ λ where
.∣∣ʳ → E.∣∣ʳ
.truncation-is-propositionʳ →
_↔_.to (H-level↔H-level 1) ∘ E.truncation-is-propositionʳ
where
module E = Elim e
record Rec (A : Type a) (B : Type b) : Type (a ⊔ b) where
no-eta-equality
field
∣∣ʳ : A → B
@0 truncation-is-propositionʳ : Is-proposition B
open Rec public
rec : Rec A B → ∥ A ∥ᴱ → B
rec r = recᴾ λ where
.∣∣ʳ → R.∣∣ʳ
.truncation-is-propositionʳ →
_↔_.to (H-level↔H-level 1) R.truncation-is-propositionʳ
where
module R = Rec r
∥∥ᴱ≃∥∥ᴱ : ∥ A ∥ᴱ ≃ N.∥ A ∥ᴱ
∥∥ᴱ≃∥∥ᴱ = Eq.↔→≃
(rec λ where
.∣∣ʳ → N.∣_∣
.truncation-is-propositionʳ → N.∥∥ᴱ-proposition)
(N.elim λ where
.N.∣∣ʳ → ∣_∣
.N.is-propositionʳ _ → truncation-is-proposition)
(N.elim λ where
.N.∣∣ʳ _ → refl _
.N.is-propositionʳ _ → mono₁ 1 N.∥∥ᴱ-proposition)
(elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ → mono₁ 1 truncation-is-proposition)
∥∥ᴱ-map : (A → B) → ∥ A ∥ᴱ → ∥ B ∥ᴱ
∥∥ᴱ-map f = rec λ where
.∣∣ʳ → ∣_∣ ∘ f
.truncation-is-propositionʳ → truncation-is-proposition
mutual
∥∥ᴱ-cong-⇔ : A ⇔ B → ∥ A ∥ᴱ ≃ᴱ ∥ B ∥ᴱ
∥∥ᴱ-cong-⇔ A⇔B = ∥∥ᴱ-cong-⇔′ (∣_∣ ∘ _⇔_.to A⇔B) (∣_∣ ∘ _⇔_.from A⇔B)
∥∥ᴱ-cong-⇔′ : (A → ∥ B ∥ᴱ) → (B → ∥ A ∥ᴱ) → ∥ A ∥ᴱ ≃ᴱ ∥ B ∥ᴱ
∥∥ᴱ-cong-⇔′ A→∥B∥ B→∥A∥ = EEq.⇔→≃ᴱ
truncation-is-proposition
truncation-is-proposition
(rec λ where
.∣∣ʳ → A→∥B∥
.truncation-is-propositionʳ → truncation-is-proposition)
(rec λ where
.∣∣ʳ → B→∥A∥
.truncation-is-propositionʳ → truncation-is-proposition)
private
∥∥ᴱ-cong-↔ : A ↔ B → ∥ A ∥ᴱ ↔ ∥ B ∥ᴱ
∥∥ᴱ-cong-↔ A↔B = record
{ surjection = record
{ logical-equivalence = record
{ to = ∥∥ᴱ-map (_↔_.to A↔B)
; from = ∥∥ᴱ-map (_↔_.from A↔B)
}
; right-inverse-of = elim λ where
.∣∣ʳ x →
∣ _↔_.to A↔B (_↔_.from A↔B x) ∣ ≡⟨ cong ∣_∣ (_↔_.right-inverse-of A↔B x) ⟩∎
∣ x ∣ ∎
.truncation-is-propositionʳ _ →
mono₁ 1 truncation-is-proposition
}
; left-inverse-of = elim λ where
.∣∣ʳ x →
∣ _↔_.from A↔B (_↔_.to A↔B x) ∣ ≡⟨ cong ∣_∣ (_↔_.left-inverse-of A↔B x) ⟩∎
∣ x ∣ ∎
.truncation-is-propositionʳ _ →
mono₁ 1 truncation-is-proposition
}
∥∥ᴱ-cong : A ↝[ ⌊ k ⌋-sym ] B → ∥ A ∥ᴱ ↝[ ⌊ k ⌋-sym ] ∥ B ∥ᴱ
∥∥ᴱ-cong {k = logical-equivalence} = _≃ᴱ_.logical-equivalence ∘
∥∥ᴱ-cong-⇔
∥∥ᴱ-cong {k = bijection} = ∥∥ᴱ-cong-↔
∥∥ᴱ-cong {k = equivalence} = from-isomorphism ∘ ∥∥ᴱ-cong-↔ ∘
from-isomorphism
∥∥ᴱ-cong {k = equivalenceᴱ} = ∥∥ᴱ-cong-⇔ ∘
_≃ᴱ_.logical-equivalence
∥∥ᴱ↔ : @0 Is-proposition A → ∥ A ∥ᴱ ↔ A
∥∥ᴱ↔ A-prop = record
{ surjection = record
{ logical-equivalence = record
{ to = rec λ where
.∣∣ʳ → id
.truncation-is-propositionʳ → A-prop
; from = ∣_∣
}
; right-inverse-of = λ _ → refl _
}
; left-inverse-of = elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ → mono₁ 1 truncation-is-proposition
}
inhabited⇒∥∥ᴱ≃ᴱ⊤ : ∥ A ∥ᴱ → ∥ A ∥ᴱ ≃ᴱ ⊤
inhabited⇒∥∥ᴱ≃ᴱ⊤ ∥a∥ =
EEq.inhabited→Is-proposition→≃ᴱ⊤ ∥a∥ truncation-is-proposition
not-inhabited⇒∥∥ᴱ↔⊥ : ¬ A → ∥ A ∥ᴱ ↔ ⊥ {ℓ = ℓ}
not-inhabited⇒∥∥ᴱ↔⊥ {A = A} =
¬ A ↝⟨ (λ ¬a → rec λ where
.∣∣ʳ → ¬a
.truncation-is-propositionʳ → ⊥-propositional) ⟩
¬ ∥ A ∥ᴱ ↝⟨ inverse ∘ Bijection.⊥↔uninhabited ⟩□
∥ A ∥ᴱ ↔ ⊥ □
¬∥∥ᴱ↔¬ : ¬ ∥ A ∥ᴱ ↔ ¬ A
¬∥∥ᴱ↔¬ {A = A} = record
{ surjection = record
{ logical-equivalence = record
{ to = λ f → f ∘ ∣_∣
; from = λ ¬A → rec λ where
.∣∣ʳ → ¬A
.truncation-is-propositionʳ → ⊥-propositional
}
; right-inverse-of = λ _ → ¬-propositional ext _ _
}
; left-inverse-of = λ _ → ¬-propositional ext _ _
}
idempotent : ∥ A ⊎ A ∥ᴱ ≃ᴱ ∥ A ∥ᴱ
idempotent = ∥∥ᴱ-cong-⇔ (record { to = P.[ id , id ]; from = inj₁ })
mutual
universal-property :
@0 Is-proposition B →
(∥ A ∥ᴱ → B) ≃ (A → B)
universal-property B-prop = universal-property-Π (λ _ → B-prop)
universal-property-Π :
@0 (∀ x → Is-proposition (P x)) →
((x : ∥ A ∥ᴱ) → P x) ≃ ((x : A) → P ∣ x ∣)
universal-property-Π {A = A} {P = P} P-prop =
((x : ∥ A ∥ᴱ) → P x) ↝⟨ Eq.↔⇒≃ (record
{ surjection = record
{ logical-equivalence = record
{ to = λ f → ∣ f ∘ ∣_∣ ∣
; from = rec λ where
.∣∣ʳ f → elim λ where
.∣∣ʳ → f
.truncation-is-propositionʳ → P-prop
.truncation-is-propositionʳ →
Π-closure ext 1 λ _ → P-prop _
}
; right-inverse-of = elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ →
mono₁ 1 truncation-is-proposition
}
; left-inverse-of = λ f → ⟨ext⟩ $ elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ →
mono₁ 1 (P-prop _)
}) ⟩
∥ ((x : A) → P ∣ x ∣) ∥ᴱ ↔⟨ ∥∥ᴱ↔ (Π-closure ext 1 λ _ → P-prop _) ⟩□
((x : A) → P ∣ x ∣) □
_ :
(@0 B-prop : Is-proposition B)
(f : ∥ A ∥ᴱ → B) →
_≃_.to (universal-property B-prop) f ≡ f ∘ ∣_∣
_ = λ _ _ → refl _
_ :
(@0 B-prop : Is-proposition B)
(f : A → B) (x : A) →
_≃_.from (universal-property B-prop) f ∣ x ∣ ≡ f x
_ = λ _ _ _ → refl _
∥∥ᴱ→≃ :
(∥ A ∥ᴱ → B)
≃
(∃ λ (f : A → B) →
Erased (∃ λ (g : ∀ n → ∥ A ∥¹-out-^ (suc n) → B) →
(∀ x → g zero O.∣ x ∣ ≡ f x) ×
(∀ n x → g (suc n) O.∣ x ∣ ≡ g n x)))
∥∥ᴱ→≃ {A = A} {B = B} =
(∥ A ∥ᴱ → B) ↝⟨ →-cong ext ∥∥ᴱ≃∥∥ᴱ F.id ⟩
(N.∥ A ∥ᴱ → B) ↝⟨ C.universal-property ⟩□
(∃ λ (f : A → B) →
Erased (∃ λ (g : ∀ n → ∥ A ∥¹-out-^ (suc n) → B) →
(∀ x → g zero O.∣ x ∣ ≡ f x) ×
(∀ n x → g (suc n) O.∣ x ∣ ≡ g n x))) □
Σ-Π-∥∥ᴱ-Erased-≡-≃ :
{@0 g : (x : ∥ A ∥ᴱ) → P x} →
(∃ λ (f : (x : ∥ A ∥ᴱ) → P x) → Erased (f ≡ g)) ≃
(∃ λ (f : (x : A) → P ∣ x ∣) → Erased (f ≡ g ∘ ∣_∣))
Σ-Π-∥∥ᴱ-Erased-≡-≃ {A = A} {P = P} {g = g} =
(∃ λ (f : (x : ∥ A ∥ᴱ) → P x) → Erased (f ≡ g)) ↝⟨ (Σ-cong lemma λ _ → Er.Erased-cong (inverse $ Eq.≃-≡ lemma)) ⟩
(∃ λ (f : (x : N.∥ A ∥ᴱ) → P (_≃_.from ∥∥ᴱ≃∥∥ᴱ x)) →
Erased (f ≡ g ∘ _≃_.from ∥∥ᴱ≃∥∥ᴱ)) ↝⟨ N.Σ-Π-∥∥ᴱ-Erased-≡-≃ ⟩□
(∃ λ (f : (x : A) → P ∣ x ∣) → Erased (f ≡ g ∘ ∣_∣)) □
where
lemma = Π-cong-contra ext (inverse ∥∥ᴱ≃∥∥ᴱ) λ _ → Eq.id
constant-endofunction⇒h-stable :
{f : A → A} → @0 Constant f → ∥ A ∥ᴱ → A
constant-endofunction⇒h-stable {A = A} {f = f} c =
∥ A ∥ᴱ ↝⟨ (rec λ where
.∣∣ʳ x → f x , [ c (f x) x ]
.truncation-is-propositionʳ → prop) ⟩
(∃ λ (x : A) → Erased (f x ≡ x)) ↝⟨ proj₁ ⟩□
A □
where
@0 prop : _
prop = $⟨ fixpoint-lemma f c ⟩
Is-proposition (∃ λ x → f x ≡ x) ↝⟨ H-level-cong _ 1 (∃-cong λ _ → inverse $ Er.erased Er.Erased↔) ⦂ (_ → _) ⟩□
Is-proposition (∃ λ x → Erased (f x ≡ x)) □
constant-endofunction⇔h-stable :
(∃ λ (f : A → A) → Erased (Constant f)) ⇔ (∥ A ∥ᴱ → A)
constant-endofunction⇔h-stable = record
{ to = λ (_ , [ c ]) → constant-endofunction⇒h-stable c
; from = λ f → f ∘ ∣_∣
, [ (λ x y →
f ∣ x ∣ ≡⟨ cong f $ truncation-is-proposition _ _ ⟩∎
f ∣ y ∣ ∎)
]
}
∥∥ᴱ×≃ᴱ : (∥ A ∥ᴱ × A) ≃ᴱ A
∥∥ᴱ×≃ᴱ = EEq.↔→≃ᴱ
proj₂
(λ x → ∣ x ∣ , x)
refl
(λ _ → cong (_, _) (truncation-is-proposition _ _))
_ : _≃ᴱ_.right-inverse-of ∥∥ᴱ×≃ᴱ x ≡ refl _
_ = refl _
∥∥ᴱ×∥∥ᴱ↔∥×∥ᴱ : (∥ A ∥ᴱ × ∥ B ∥ᴱ) ↔ ∥ A × B ∥ᴱ
∥∥ᴱ×∥∥ᴱ↔∥×∥ᴱ = record
{ surjection = record
{ logical-equivalence = record
{ from = λ p → ∥∥ᴱ-map proj₁ p , ∥∥ᴱ-map proj₂ p
; to = uncurry $ rec λ where
.∣∣ʳ x → rec λ where
.∣∣ʳ y → ∣ x , y ∣
.truncation-is-propositionʳ →
truncation-is-proposition
.truncation-is-propositionʳ →
Π-closure ext 1 λ _ →
truncation-is-proposition
}
; right-inverse-of = elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ →
mono₁ 1 truncation-is-proposition
}
; left-inverse-of = uncurry $ elim λ where
.∣∣ʳ _ → elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ →
mono₁ 1 $
×-closure 1 truncation-is-proposition
truncation-is-proposition
.truncation-is-propositionʳ _ →
Π-closure ext 1 λ _ →
mono₁ 1 $
×-closure 1 truncation-is-proposition
truncation-is-proposition
}
private
H-level-×₁-lemma :
(A → ∥ B ∥ᴱ) →
∀ n → H-level (suc n) (A × B) → H-level (suc n) A
H-level-×₁-lemma inhabited n h =
[inhabited⇒+]⇒+ n λ a →
flip rec (inhabited a) λ where
.∣∣ʳ b →
proj₁-closure (λ _ → b) (suc n) h
.truncation-is-propositionʳ →
H-level-propositional ext (suc n)
H-level-×₁ :
(A → ∥ B ∥ᴱ) →
∀ n → H-level n (A × B) → H-level n A
H-level-×₁ inhabited zero h =
propositional⇒inhabited⇒contractible
(H-level-×₁-lemma inhabited 0 (mono₁ 0 h))
(proj₁ (proj₁ h))
H-level-×₁ inhabited (suc n) =
H-level-×₁-lemma inhabited n
H-level-×₂ :
(B → ∥ A ∥ᴱ) →
∀ n → H-level n (A × B) → H-level n B
H-level-×₂ {B = B} {A = A} inhabited n =
H-level n (A × B) ↝⟨ H-level.respects-surjection (from-bijection ×-comm) n ⟩
H-level n (B × A) ↝⟨ H-level-×₁ inhabited n ⟩□
H-level n B □
flatten′ :
(F : (Type ℓ → Type ℓ) → Type f)
(map : ∀ {G H} → (∀ {A} → G A → H A) → F G → F H)
(f : F ∥_∥ᴱ → ∥ F id ∥ᴱ) →
(∀ x → f (map ∣_∣ x) ≡ ∣ x ∣) →
(∀ x → ∥∥ᴱ-map (map ∣_∣) (f x) ≡ ∣ x ∣) →
∥ F ∥_∥ᴱ ∥ᴱ ↔ ∥ F id ∥ᴱ
flatten′ _ map f f-map map-f = record
{ surjection = record
{ logical-equivalence = record
{ to = rec λ where
.∣∣ʳ → f
.truncation-is-propositionʳ → truncation-is-proposition
; from = ∥∥ᴱ-map (map ∣_∣)
}
; right-inverse-of = elim λ where
.∣∣ʳ → f-map
.truncation-is-propositionʳ _ →
mono₁ 1 truncation-is-proposition
}
; left-inverse-of = elim λ where
.∣∣ʳ → map-f
.truncation-is-propositionʳ _ →
mono₁ 1 truncation-is-proposition
}
flatten : ∥ ∥ A ∥ᴱ ∥ᴱ ↔ ∥ A ∥ᴱ
flatten {A = A} = flatten′
(λ F → F A)
(λ f → f)
id
(λ _ → refl _)
(elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ → mono₁ 1 truncation-is-proposition)
private
∥∃∥∥ᴱ∥ᴱ↔∥∃∥ᴱ : ∥ ∃ (∥_∥ᴱ ∘ P) ∥ᴱ ↔ ∥ ∃ P ∥ᴱ
∥∃∥∥ᴱ∥ᴱ↔∥∃∥ᴱ {P = P} = flatten′
(λ F → ∃ (F ∘ P))
(λ f → Σ-map id f)
(uncurry λ x → ∥∥ᴱ-map (x ,_))
(λ _ → refl _)
(uncurry λ _ → elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ →
mono₁ 1 truncation-is-proposition)
flatten-≃ᴱ :
(F : (Type ℓ → Type ℓ) → Type f)
(map : ∀ {G H} → (∀ {A} → G A → H A) → F G → F H)
(f : F ∥_∥ᴱ → ∥ F id ∥ᴱ) →
@0 (∀ x → f (map ∣_∣ x) ≡ ∣ x ∣) →
@0 (∀ x → ∥∥ᴱ-map (map ∣_∣) (f x) ≡ ∣ x ∣) →
∥ F ∥_∥ᴱ ∥ᴱ ≃ᴱ ∥ F id ∥ᴱ
flatten-≃ᴱ _ map f f-map map-f = EEq.↔→≃ᴱ
(rec λ where
.∣∣ʳ → f
.truncation-is-propositionʳ → truncation-is-proposition)
(∥∥ᴱ-map (map ∣_∣))
(elim λ @0 where
.∣∣ʳ → f-map
.truncation-is-propositionʳ _ →
mono₁ 1 truncation-is-proposition)
(elim λ @0 where
.∣∣ʳ → map-f
.truncation-is-propositionʳ _ →
mono₁ 1 truncation-is-proposition)
infixl 5 _>>=′_
_>>=′_ : ∥ A ∥ᴱ → (A → ∥ B ∥ᴱ) → ∥ B ∥ᴱ
x >>=′ f = _↔_.to flatten (∥∥ᴱ-map f x)
>>=′-associative :
(x : ∥ A ∥ᴱ) →
x >>=′ (λ x → f x >>=′ g) ≡ x >>=′ f >>=′ g
>>=′-associative = elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ → ⇒≡ 1 truncation-is-proposition
instance
raw-monad : Raw-monad (∥_∥ᴱ {a = a})
Raw-monad.return raw-monad = ∣_∣
Raw-monad._>>=_ raw-monad = _>>=′_
monad : Monad (∥_∥ᴱ {a = a})
Monad.raw-monad monad = raw-monad
Monad.left-identity monad _ _ = refl _
Monad.associativity monad x _ _ = >>=′-associative x
Monad.right-identity monad = elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ → ⇒≡ 1 truncation-is-proposition
Surjectiveᴱ :
{A : Type a} {B : Type b} →
(A → B) → Type (a ⊔ b)
Surjectiveᴱ f = ∀ y → ∥ f ⁻¹ᴱ y ∥ᴱ
@0 Surjectiveᴱ-propositional : Is-proposition (Surjectiveᴱ f)
Surjectiveᴱ-propositional =
Π-closure ext 1 λ _ →
truncation-is-proposition
∣∣-surjective : Surjectiveᴱ (∣_∣ {A = A})
∣∣-surjective = elim λ where
.∣∣ʳ x → ∣ x , [ refl _ ] ∣
.truncation-is-propositionʳ _ → truncation-is-proposition
Split-surjective→Surjectiveᴱ :
Split-surjective f → Surjectiveᴱ f
Split-surjective→Surjectiveᴱ s = λ y → ∣ ECP.⁻¹→⁻¹ᴱ (s y) ∣
Surjectiveᴱ×Erased-Is-embedding≃ᴱIs-equivalenceᴱ :
(Surjectiveᴱ f × Erased (Is-embedding f)) ≃ᴱ Is-equivalenceᴱ f
Surjectiveᴱ×Erased-Is-embedding≃ᴱIs-equivalenceᴱ {f = f} = EEq.⇔→≃ᴱ
(×-closure 1
Surjectiveᴱ-propositional
(Er.H-level-Erased 1
(Emb.Is-embedding-propositional ext)))
(EEq.Is-equivalenceᴱ-propositional ext f)
(λ (is-surj , is-emb) →
_⇔_.from EEq.Is-equivalenceᴱ⇔Is-equivalenceᴱ-CP $ λ y →
$⟨ is-surj y ⟩
∥ f ⁻¹ᴱ y ∥ᴱ ↝⟨ (rec λ where
.∣∣ʳ p → ECP.inhabited→Is-proposition→Contractibleᴱ p
(H-level-cong _ 1
ECP.⁻¹≃⁻¹ᴱ
(Emb.embedding→⁻¹-propositional (Er.erased is-emb) _))
.truncation-is-propositionʳ →
ECP.Contractibleᴱ-propositional ext) ⟩□
Contractibleᴱ (f ⁻¹ᴱ y) □)
(λ is-eq@(inv , [ r-inv , _ ]) →
(λ y → $⟨ inv y , [ r-inv y ] ⟩
f ⁻¹ᴱ y ↝⟨ ∣_∣ ⟩
∥ f ⁻¹ᴱ y ∥ᴱ □)
, ($⟨ is-eq ⟩
Is-equivalenceᴱ f ↝⟨ Er.[_]→ ⟩
Erased (Is-equivalenceᴱ f) ↝⟨ Er.map EEq.Is-equivalenceᴱ→Is-equivalence ⟩
Erased (Is-equivalence f) ↝⟨ Er.map Emb.Is-equivalence→Is-embedding ⟩□
Erased (Is-embedding f) □))
∥∥ᴱ-preserves-Is-equivalence-relation :
Is-equivalence-relation R →
Is-equivalence-relation (λ x y → ∥ R x y ∥ᴱ)
∥∥ᴱ-preserves-Is-equivalence-relation R-equiv = record
{ reflexive = ∣ reflexive ∣
; symmetric = symmetric ⟨$⟩_
; transitive = λ p q → transitive ⟨$⟩ p ⊛ q
}
where
open Is-equivalence-relation R-equiv
infixr 1 _∥⊎∥ᴱ_
_∥⊎∥ᴱ_ : Type a → Type b → Type (a ⊔ b)
A ∥⊎∥ᴱ B = ∥ A ⊎ B ∥ᴱ
∣inj₁∣ : A → A ∥⊎∥ᴱ B
∣inj₁∣ = ∣_∣ ∘ inj₁
∣inj₂∣ : B → A ∥⊎∥ᴱ B
∣inj₂∣ = ∣_∣ ∘ inj₂
@0 ∥⊎∥ᴱ-propositional : Is-proposition (A ∥⊎∥ᴱ B)
∥⊎∥ᴱ-propositional = truncation-is-proposition
infixr 1 _∥⊎∥ᴱ-cong_
_∥⊎∥ᴱ-cong_ :
A₁ ↝[ ⌊ k ⌋-sym ] A₂ → B₁ ↝[ ⌊ k ⌋-sym ] B₂ →
(A₁ ∥⊎∥ᴱ B₁) ↝[ ⌊ k ⌋-sym ] (A₂ ∥⊎∥ᴱ B₂)
A₁↝A₂ ∥⊎∥ᴱ-cong B₁↝B₂ = ∥∥ᴱ-cong (A₁↝A₂ ⊎-cong B₁↝B₂)
∥⊎∥ᴱ-comm : A ∥⊎∥ᴱ B ↔ B ∥⊎∥ᴱ A
∥⊎∥ᴱ-comm = ∥∥ᴱ-cong ⊎-comm
truncate-left-∥⊎∥ᴱ : A ∥⊎∥ᴱ B ↔ ∥ A ∥ᴱ ∥⊎∥ᴱ B
truncate-left-∥⊎∥ᴱ =
inverse $
flatten′
(λ F → F _ ⊎ _)
(λ f → ⊎-map f id)
P.[ ∥∥ᴱ-map inj₁ , ∣inj₂∣ ]
P.[ (λ _ → refl _) , (λ _ → refl _) ]
P.[ (elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ →
mono₁ 1 ∥⊎∥ᴱ-propositional)
, (λ _ → refl _)
]
truncate-right-∥⊎∥ᴱ : A ∥⊎∥ᴱ B ↔ A ∥⊎∥ᴱ ∥ B ∥ᴱ
truncate-right-∥⊎∥ᴱ {A = A} {B = B} =
A ∥⊎∥ᴱ B ↝⟨ ∥⊎∥ᴱ-comm ⟩
B ∥⊎∥ᴱ A ↝⟨ truncate-left-∥⊎∥ᴱ ⟩
∥ B ∥ᴱ ∥⊎∥ᴱ A ↝⟨ ∥⊎∥ᴱ-comm ⟩□
A ∥⊎∥ᴱ ∥ B ∥ᴱ □
∥⊎∥ᴱ-assoc : A ∥⊎∥ᴱ (B ∥⊎∥ᴱ C) ↔ (A ∥⊎∥ᴱ B) ∥⊎∥ᴱ C
∥⊎∥ᴱ-assoc {A = A} {B = B} {C = C} =
∥ A ⊎ ∥ B ⊎ C ∥ᴱ ∥ᴱ ↝⟨ inverse truncate-right-∥⊎∥ᴱ ⟩
∥ A ⊎ B ⊎ C ∥ᴱ ↝⟨ ∥∥ᴱ-cong ⊎-assoc ⟩
∥ (A ⊎ B) ⊎ C ∥ᴱ ↝⟨ truncate-left-∥⊎∥ᴱ ⟩□
∥ ∥ A ⊎ B ∥ᴱ ⊎ C ∥ᴱ □
∥⊎∥ᴱ-left-identity : @0 Is-proposition A → ⊥ {ℓ = ℓ} ∥⊎∥ᴱ A ↔ A
∥⊎∥ᴱ-left-identity {A = A} A-prop =
∥ ⊥ ⊎ A ∥ᴱ ↝⟨ ∥∥ᴱ-cong ⊎-left-identity ⟩
∥ A ∥ᴱ ↝⟨ ∥∥ᴱ↔ A-prop ⟩□
A □
∥⊎∥ᴱ-right-identity : @0 Is-proposition A → A ∥⊎∥ᴱ ⊥ {ℓ = ℓ} ↔ A
∥⊎∥ᴱ-right-identity {A = A} A-prop =
A ∥⊎∥ᴱ ⊥ ↔⟨ ∥⊎∥ᴱ-comm ⟩
⊥ ∥⊎∥ᴱ A ↔⟨ ∥⊎∥ᴱ-left-identity A-prop ⟩□
A □
∥⊎∥ᴱ-idempotent : @0 Is-proposition A → (A ∥⊎∥ᴱ A) ≃ᴱ A
∥⊎∥ᴱ-idempotent {A = A} A-prop =
∥ A ⊎ A ∥ᴱ ↝⟨ idempotent ⟩
∥ A ∥ᴱ ↔⟨ ∥∥ᴱ↔ A-prop ⟩□
A □
drop-left-∥⊎∥ᴱ :
@0 Is-proposition B → (A → B) → (A ∥⊎∥ᴱ B) ≃ᴱ B
drop-left-∥⊎∥ᴱ B-prop A→B = EEq.⇔→≃ᴱ
∥⊎∥ᴱ-propositional
B-prop
(rec λ where
.∣∣ʳ → P.[ A→B , id ]
.truncation-is-propositionʳ → B-prop)
∣inj₂∣
drop-right-∥⊎∥ᴱ :
@0 Is-proposition A → (B → A) → (A ∥⊎∥ᴱ B) ≃ᴱ A
drop-right-∥⊎∥ᴱ {A = A} {B = B} A-prop B→A =
A ∥⊎∥ᴱ B ↔⟨ ∥⊎∥ᴱ-comm ⟩
B ∥⊎∥ᴱ A ↝⟨ drop-left-∥⊎∥ᴱ A-prop B→A ⟩□
A □
drop-⊥-right-∥⊎∥ᴱ :
@0 Is-proposition A → ¬ B → A ∥⊎∥ᴱ B ↔ A
drop-⊥-right-∥⊎∥ᴱ A-prop ¬B = record
{ surjection = record
{ logical-equivalence = record
{ to = rec λ where
.∣∣ʳ → P.[ id , ⊥-elim ∘ ¬B ]
.truncation-is-propositionʳ → A-prop
; from = ∣inj₁∣
}
; right-inverse-of = refl
}
; left-inverse-of = elim λ where
.∣∣ʳ → P.[ (λ _ → refl _) , ⊥-elim ∘ ¬B ]
.truncation-is-propositionʳ _ →
mono₁ 1 ∥⊎∥ᴱ-propositional
}
drop-⊥-left-∥⊎∥ᴱ :
@0 Is-proposition B → ¬ A → A ∥⊎∥ᴱ B ↔ B
drop-⊥-left-∥⊎∥ᴱ B-prop ¬A = record
{ surjection = record
{ logical-equivalence = record
{ to = rec λ where
.∣∣ʳ → P.[ ⊥-elim ∘ ¬A , id ]
.truncation-is-propositionʳ → B-prop
; from = ∣inj₂∣
}
; right-inverse-of = refl
}
; left-inverse-of = elim λ where
.∣∣ʳ → P.[ ⊥-elim ∘ ¬A , (λ _ → refl _) ]
.truncation-is-propositionʳ _ →
mono₁ 1 ∥⊎∥ᴱ-propositional
}
Π∥⊎∥ᴱ↔Π×Π :
@0 (∀ x → Is-proposition (P x)) →
((x : A ∥⊎∥ᴱ B) → P x)
↔
((x : A) → P (∣inj₁∣ x)) × ((y : B) → P (∣inj₂∣ y))
Π∥⊎∥ᴱ↔Π×Π {A = A} {B = B} {P = P} P-prop =
((x : A ∥⊎∥ᴱ B) → P x) ↔⟨ universal-property-Π P-prop ⟩
((x : A ⊎ B) → P ∣ x ∣) ↝⟨ Π⊎↔Π×Π ext ⟩□
((x : A) → P (∣inj₁∣ x)) × ((y : B) → P (∣inj₂∣ y)) □
Σ-∥⊎∥ᴱ-distrib-left :
@0 Is-proposition A →
Σ A (λ x → P x ∥⊎∥ᴱ Q x) ↔ Σ A P ∥⊎∥ᴱ Σ A Q
Σ-∥⊎∥ᴱ-distrib-left {P = P} {Q = Q} A-prop =
(∃ λ x → ∥ P x ⊎ Q x ∥ᴱ) ↝⟨ inverse $ ∥∥ᴱ↔ (Σ-closure 1 A-prop λ _ → ∥⊎∥ᴱ-propositional) ⟩
∥ (∃ λ x → ∥ P x ⊎ Q x ∥ᴱ) ∥ᴱ ↝⟨ flatten′
(λ F → (∃ λ x → F (P x ⊎ Q x)))
(λ f → Σ-map id f)
(uncurry λ x → ∥∥ᴱ-map (x ,_))
(λ _ → refl _)
(uncurry λ _ → elim λ where
.∣∣ʳ _ → refl _
.truncation-is-propositionʳ _ →
mono₁ 1 truncation-is-proposition) ⟩
∥ (∃ λ x → P x ⊎ Q x) ∥ᴱ ↝⟨ ∥∥ᴱ-cong ∃-⊎-distrib-left ⟩□
∥ ∃ P ⊎ ∃ Q ∥ᴱ □
Σ-∥⊎∥ᴱ-distrib-right :
@0 (∀ x → Is-proposition (P x)) →
Σ (A ∥⊎∥ᴱ B) P ↔ Σ A (P ∘ ∣inj₁∣) ∥⊎∥ᴱ Σ B (P ∘ ∣inj₂∣)
Σ-∥⊎∥ᴱ-distrib-right {A = A} {B = B} {P = P} P-prop = record
{ surjection = record
{ logical-equivalence = record
{ to = uncurry $ elim λ where
.∣∣ʳ → curry (∣_∣ ∘ _↔_.to ∃-⊎-distrib-right)
.truncation-is-propositionʳ _ →
Π-closure ext 1 λ _ →
∥⊎∥ᴱ-propositional
; from = rec λ where
.∣∣ʳ → Σ-map ∣_∣ id ∘ _↔_.from ∃-⊎-distrib-right
.truncation-is-propositionʳ → prop
}
; right-inverse-of = elim λ where
.∣∣ʳ → P.[ (λ _ → refl _) , (λ _ → refl _) ]
.truncation-is-propositionʳ _ →
mono₁ 1 ∥⊎∥ᴱ-propositional
}
; left-inverse-of = uncurry $ elim λ where
.∣∣ʳ → P.[ (λ _ _ → refl _) , (λ _ _ → refl _) ]
.truncation-is-propositionʳ _ →
Π-closure ext 1 λ _ →
mono₁ 1 prop
}
where
@0 prop : _
prop = Σ-closure 1 ∥⊎∥ᴱ-propositional P-prop
¬∥⊎∥ᴱ¬↔¬× :
Dec (¬ A) → Dec (¬ B) →
(¬ A ∥⊎∥ᴱ ¬ B) ≃ᴱ (¬ (A × B))
¬∥⊎∥ᴱ¬↔¬× {A = A} {B = B} dec-¬A dec-¬B = EEq.⇔→≃ᴱ
∥⊎∥ᴱ-propositional
(¬-propositional ext)
(rec λ where
.∣∣ʳ → ¬⊎¬→׬
.truncation-is-propositionʳ → ¬-propositional ext)
(∣_∣ ∘ _↠_.from (¬⊎¬↠¬× ext dec-¬A dec-¬B))