{-# OPTIONS --without-K --safe #-}
open import Equality
module Equivalence.Erased.Contractible-preimages
{reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where
open Derived-definitions-and-properties eq
open import Prelude
open import Bijection eq using (_↔_)
open import Equivalence eq as Eq using (_≃_; Is-equivalence)
import Equivalence.Contractible-preimages eq as CP
open import Erased.Level-1 eq as Erased
open import Function-universe eq hiding (id; _∘_)
open import H-level eq as H-level
open import H-level.Closure eq
open import Preimage eq as Preimage using (_⁻¹_)
open import Surjection eq using (_↠_; Split-surjective)
private
variable
a b ℓ : Level
A B : Type a
c ext k k′ p x y : A
P : A → Type p
f : (x : A) → P x
infix 5 _⁻¹ᴱ_
_⁻¹ᴱ_ : {A : Type a} {@0 B : Type b} → @0 (A → B) → @0 B → Type (a ⊔ b)
f ⁻¹ᴱ y = ∃ λ x → Erased (f x ≡ y)
Contractibleᴱ : Type ℓ → Type ℓ
Contractibleᴱ A = ∃ λ (x : A) → Erased (∀ y → x ≡ y)
Is-equivalenceᴱ : {A : Type a} {B : Type b} → @0 (A → B) → Type (a ⊔ b)
Is-equivalenceᴱ f = ∀ y → Contractibleᴱ (f ⁻¹ᴱ y)
_≃ᴱ_ : Type a → Type b → Type (a ⊔ b)
A ≃ᴱ B = ∃ λ (f : A → B) → Is-equivalenceᴱ f
⁻¹→⁻¹ᴱ : f ⁻¹ y → f ⁻¹ᴱ y
⁻¹→⁻¹ᴱ = Σ-map id [_]→
@0 ⁻¹ᴱ→⁻¹ : f ⁻¹ᴱ x → f ⁻¹ x
⁻¹ᴱ→⁻¹ = Σ-map id erased
@0 ⁻¹≃⁻¹ᴱ : f ⁻¹ y ≃ f ⁻¹ᴱ y
⁻¹≃⁻¹ᴱ {f = f} {y = y} =
(∃ λ x → f x ≡ y) ↝⟨ (∃-cong λ _ → Eq.inverse $ Eq.↔⇒≃ $ erased Erased↔) ⟩□
(∃ λ x → Erased (f x ≡ y)) □
_ : _≃_.to ⁻¹≃⁻¹ᴱ p ≡ ⁻¹→⁻¹ᴱ p
_ = refl _
@0 _ : _≃_.from ⁻¹≃⁻¹ᴱ p ≡ ⁻¹ᴱ→⁻¹ p
_ = refl _
Contractible→Contractibleᴱ : Contractible A → Contractibleᴱ A
Contractible→Contractibleᴱ = Σ-map id [_]→
@0 Contractibleᴱ→Contractible : Contractibleᴱ A → Contractible A
Contractibleᴱ→Contractible = Σ-map id erased
@0 Contractible≃Contractibleᴱ :
Contractible A ≃ Contractibleᴱ A
Contractible≃Contractibleᴱ =
(∃ λ x → ∀ y → x ≡ y) ↝⟨ (∃-cong λ _ → Eq.inverse $ Eq.↔⇒≃ $ erased Erased↔) ⟩□
(∃ λ x → Erased (∀ y → x ≡ y)) □
_ :
_≃_.to Contractible≃Contractibleᴱ c ≡ Contractible→Contractibleᴱ c
_ = refl _
@0 _ :
_≃_.from Contractible≃Contractibleᴱ c ≡ Contractibleᴱ→Contractible c
_ = refl _
Is-equivalence→Is-equivalenceᴱ : CP.Is-equivalence f → Is-equivalenceᴱ f
Is-equivalence→Is-equivalenceᴱ eq y =
⁻¹→⁻¹ᴱ (proj₁ (eq y))
, [ cong ⁻¹→⁻¹ᴱ ∘ proj₂ (eq y) ∘ ⁻¹ᴱ→⁻¹ ]
@0 Is-equivalenceᴱ→Is-equivalence :
Is-equivalenceᴱ f → CP.Is-equivalence f
Is-equivalenceᴱ→Is-equivalence eq y =
⁻¹ᴱ→⁻¹ (proj₁ (eq y))
, cong ⁻¹ᴱ→⁻¹ ∘ erased (proj₂ (eq y)) ∘ ⁻¹→⁻¹ᴱ
private
@0 Is-equivalence≃Is-equivalenceᴱ′ :
{A : Type a} {B : Type b} {f : A → B} →
Extensionality? k (a ⊔ b) (a ⊔ b) →
CP.Is-equivalence f ↝[ k ] Is-equivalenceᴱ f
Is-equivalence≃Is-equivalenceᴱ′ {a = a} {k = k} {f = f} ext =
(∀ y → Contractible (f ⁻¹ y)) ↝⟨ (∀-cong ext′ λ _ → H-level-cong ext 0 ⁻¹≃⁻¹ᴱ) ⟩
(∀ y → Contractible (f ⁻¹ᴱ y)) ↝⟨ (∀-cong ext′ λ _ → from-isomorphism Contractible≃Contractibleᴱ) ⟩□
(∀ y → Contractibleᴱ (f ⁻¹ᴱ y)) □
where
ext′ = lower-extensionality? k a lzero ext
@0 Contractibleᴱ-propositional :
{A : Type a} →
Extensionality a a →
Is-proposition (Contractibleᴱ A)
Contractibleᴱ-propositional ext =
H-level.respects-surjection
(_≃_.surjection Contractible≃Contractibleᴱ)
1
(Contractible-propositional ext)
@0 Is-equivalenceᴱ-propositional :
{A : Type a} {B : Type b} →
Extensionality (a ⊔ b) (a ⊔ b) →
(f : A → B) → Is-proposition (Is-equivalenceᴱ f)
Is-equivalenceᴱ-propositional ext f =
H-level.respects-surjection
(_≃_.surjection $ Is-equivalence≃Is-equivalenceᴱ′ ext)
1
(CP.propositional ext f)
@0 Is-equivalence≃Is-equivalenceᴱ :
{A : Type a} {B : Type b} {f : A → B} →
Extensionality? k (a ⊔ b) (a ⊔ b) →
CP.Is-equivalence f ↝[ k ] Is-equivalenceᴱ f
Is-equivalence≃Is-equivalenceᴱ {k = equivalence} ext =
Eq.with-other-function
(Eq.with-other-inverse
(Is-equivalence≃Is-equivalenceᴱ′ ext)
Is-equivalenceᴱ→Is-equivalence
(λ _ → CP.propositional ext _ _ _))
Is-equivalence→Is-equivalenceᴱ
(λ _ → Is-equivalenceᴱ-propositional ext _ _ _)
Is-equivalence≃Is-equivalenceᴱ = Is-equivalence≃Is-equivalenceᴱ′
_ :
_≃_.to (Is-equivalence≃Is-equivalenceᴱ ext) p ≡
Is-equivalence→Is-equivalenceᴱ p
_ = refl _
@0 _ :
_≃_.from (Is-equivalence≃Is-equivalenceᴱ ext) p ≡
Is-equivalenceᴱ→Is-equivalence p
_ = refl _
≃→≃ᴱ : A CP.≃ B → A ≃ᴱ B
≃→≃ᴱ = Σ-map id Is-equivalence→Is-equivalenceᴱ
@0 ≃ᴱ→≃ : A ≃ᴱ B → A CP.≃ B
≃ᴱ→≃ = Σ-map id Is-equivalenceᴱ→Is-equivalence
@0 ≃≃≃ᴱ :
{A : Type a} {B : Type b} →
Extensionality? k (a ⊔ b) (a ⊔ b) →
(A CP.≃ B) ↝[ k ] (A ≃ᴱ B)
≃≃≃ᴱ {A = A} {B = B} ext =
A CP.≃ B ↔⟨⟩
(∃ λ f → CP.Is-equivalence f) ↝⟨ (∃-cong λ _ → Is-equivalence≃Is-equivalenceᴱ ext) ⟩
(∃ λ f → Is-equivalenceᴱ f) ↔⟨⟩
A ≃ᴱ B □
_ : _≃_.to (≃≃≃ᴱ ext) p ≡ ≃→≃ᴱ p
_ = refl _
@0 _ : _≃_.from (≃≃≃ᴱ ext) p ≡ ≃ᴱ→≃ p
_ = refl _
Erased-⁻¹ᴱ↔Erased-⁻¹ :
{@0 A : Type a} {@0 B : Type b} {@0 f : A → B} {@0 y : B} →
Erased (f ⁻¹ᴱ y) ↔ Erased (f ⁻¹ y)
Erased-⁻¹ᴱ↔Erased-⁻¹ {f = f} {y = y} =
Erased (∃ λ x → Erased (f x ≡ y)) ↝⟨ Erased-Σ↔Σ ⟩
(∃ λ x → Erased (Erased (f (erased x) ≡ y))) ↝⟨ (∃-cong λ _ → Erased-Erased↔Erased) ⟩
(∃ λ x → Erased (f (erased x) ≡ y)) ↝⟨ inverse Erased-Σ↔Σ ⟩□
Erased (∃ λ x → f x ≡ y) □
Erased-Contractibleᴱ↔Erased-Contractible :
{@0 A : Type a} →
Erased (Contractibleᴱ A) ↔ Erased (Contractible A)
Erased-Contractibleᴱ↔Erased-Contractible =
Erased (∃ λ x → Erased (∀ y → x ≡ y)) ↝⟨ Erased-Σ↔Σ ⟩
(∃ λ x → Erased (Erased (∀ y → erased x ≡ y))) ↝⟨ (∃-cong λ _ → Erased-Erased↔Erased) ⟩
(∃ λ x → Erased (∀ y → erased x ≡ y)) ↝⟨ inverse Erased-Σ↔Σ ⟩□
Erased (∃ λ x → ∀ y → x ≡ y) □
Contractibleᴱ-respects-surjection :
(f : A → B) → @0 Split-surjective f →
Contractibleᴱ A → Contractibleᴱ B
Contractibleᴱ-respects-surjection {A = A} {B = B} f s h@(x , _) =
f x
, [ proj₂ (H-level.respects-surjection surj 0
(Contractibleᴱ→Contractible h))
]
where
@0 surj : A ↠ B
surj = record
{ logical-equivalence = record
{ to = f
; from = proj₁ ∘ s
}
; right-inverse-of = proj₂ ∘ s
}
Contractibleᴱ-⁻¹ᴱ :
(@0 f : A → B)
(g : B → A)
(@0 f∘g : ∀ x → f (g x) ≡ x)
(@0 g∘f : ∀ x → g (f x) ≡ x) →
∀ y → Contractibleᴱ (f ⁻¹ᴱ y)
Contractibleᴱ-⁻¹ᴱ {A = A} {B = B} f g f∘g g∘f y =
(g y , [ proj₂ (proj₁ c′) ])
, [ cong ⁻¹→⁻¹ᴱ ∘ proj₂ c′ ∘ ⁻¹ᴱ→⁻¹ ]
where
@0 A↔B : A ↔ B
A↔B = record
{ surjection = record
{ logical-equivalence = record
{ to = f
; from = g
}
; right-inverse-of = f∘g
}
; left-inverse-of = g∘f
}
@0 c′ : Contractible (f ⁻¹ y)
c′ = Preimage.bijection⁻¹-contractible A↔B y
inhabited→Is-proposition→Contractibleᴱ :
A → @0 Is-proposition A → Contractibleᴱ A
inhabited→Is-proposition→Contractibleᴱ x prop = (x , [ prop x ])
Contractibleᴱ-Σ :
Contractibleᴱ A → (∀ x → Contractibleᴱ (P x)) → Contractibleᴱ (Σ A P)
Contractibleᴱ-Σ cA@(a , _) cB =
(a , proj₁ (cB a))
, [ proj₂ $ Σ-closure 0 (Contractibleᴱ→Contractible cA)
(Contractibleᴱ→Contractible ∘ cB)
]
Contractibleᴱ-× :
Contractibleᴱ A → Contractibleᴱ B → Contractibleᴱ (A × B)
Contractibleᴱ-× cA cB = Contractibleᴱ-Σ cA (λ _ → cB)
Contractibleᴱ-Π :
{A : Type a} {P : A → Type p} →
@0 Extensionality a p →
(∀ x → Contractibleᴱ (P x)) → Contractibleᴱ ((x : A) → P x)
Contractibleᴱ-Π ext c =
proj₁ ∘ c
, [ proj₂ $ Π-closure ext 0 (Contractibleᴱ→Contractible ∘ c)
]
Contractibleᴱ-↑ : Contractibleᴱ A → Contractibleᴱ (↑ ℓ A)
Contractibleᴱ-↑ c@(a , _) =
lift a
, [ proj₂ $ ↑-closure 0 (Contractibleᴱ→Contractible c)
]
module []-cong (ax : ∀ {a} → []-cong-axiomatisation a) where
open Erased.[]-cong₃ ax
⁻¹ᴱ-respects-extensional-equality :
{@0 B : Type b} {@0 f g : A → B} {@0 y : B} →
@0 (∀ x → f x ≡ g x) → f ⁻¹ᴱ y ≃ g ⁻¹ᴱ y
⁻¹ᴱ-respects-extensional-equality {f = f} {g = g} {y = y} f≡g =
(∃ λ x → Erased (f x ≡ y)) ↝⟨ (∃-cong λ _ → Erased-cong-≃ (≡⇒↝ _ (cong (_≡ _) $ f≡g _))) ⟩□
(∃ λ x → Erased (g x ≡ y)) □
⁻¹ᴱ[]↔⁻¹[] :
{@0 B : Type b} {f : A → Erased B} {@0 y : B} →
f ⁻¹ᴱ [ y ] ↔ f ⁻¹ [ y ]
⁻¹ᴱ[]↔⁻¹[] {f = f} {y = y} =
(∃ λ x → Erased (f x ≡ [ y ])) ↔⟨ (∃-cong λ _ → Erased-cong-≃ (Eq.≃-≡ $ Eq.↔⇒≃ $ inverse $ erased Erased↔)) ⟩
(∃ λ x → Erased (erased (f x) ≡ y)) ↝⟨ (∃-cong λ _ → Erased-≡↔[]≡[]) ⟩□
(∃ λ x → f x ≡ [ y ]) □
Erased-⁻¹ᴱ :
{@0 A : Type a} {@0 B : Type b} {@0 f : A → B} {@0 y : B} →
Erased (f ⁻¹ᴱ y) ↔ map f ⁻¹ᴱ [ y ]
Erased-⁻¹ᴱ {f = f} {y = y} =
Erased (f ⁻¹ᴱ y) ↝⟨ Erased-⁻¹ᴱ↔Erased-⁻¹ ⟩
Erased (f ⁻¹ y) ↝⟨ Erased-⁻¹ ⟩
map f ⁻¹ [ y ] ↝⟨ inverse ⁻¹ᴱ[]↔⁻¹[] ⟩□
map f ⁻¹ᴱ [ y ] □
Contractibleᴱ-cong :
{A : Type a} {B : Type b} →
@0 Extensionality? k′ (a ⊔ b) (a ⊔ b) →
A ↔[ k ] B → Contractibleᴱ A ↝[ k′ ] Contractibleᴱ B
Contractibleᴱ-cong {A = A} {B = B} ext A↔B =
(∃ λ (x : A) → Erased ((y : A) → x ≡ y)) ↝⟨ (Σ-cong A≃B′ λ _ →
Erased-cong?
(λ ext → Π-cong ext A≃B′ λ _ →
from-isomorphism $ inverse $ Eq.≃-≡ A≃B′)
ext) ⟩
(∃ λ (x : B) → Erased ((y : B) → x ≡ y)) □
where
A≃B′ = from-isomorphism A↔B
Erased-Contractibleᴱ↔Contractibleᴱ-Erased :
{@0 A : Type a} →
@0 Extensionality? k a a →
Erased (Contractibleᴱ A) ↝[ k ] Contractibleᴱ (Erased A)
Erased-Contractibleᴱ↔Contractibleᴱ-Erased {A = A} ext =
Erased (∃ λ x → Erased ((y : A) → x ≡ y)) ↔⟨ Erased-cong-↔ (∃-cong λ _ → erased Erased↔) ⟩
Erased (∃ λ x → (y : A) → x ≡ y) ↔⟨ Erased-Σ↔Σ ⟩
(∃ λ x → Erased ((y : A) → erased x ≡ y)) ↝⟨ (∃-cong λ _ →
Erased-cong?
(λ ext → ∀-cong ext λ _ →
from-isomorphism (inverse $ erased Erased↔))
ext) ⟩
(∃ λ x → Erased ((y : A) → Erased (erased x ≡ y))) ↝⟨ (∃-cong λ _ →
Erased-cong?
(λ ext → Π-cong ext (inverse $ erased Erased↔) λ _ →
from-isomorphism Erased-≡↔[]≡[])
ext) ⟩□
(∃ λ x → Erased ((y : Erased A) → x ≡ y)) □
Contractibleᴱ-Erased↔Contractible-Erased :
{@0 A : Type a} →
Extensionality? k a a →
Contractibleᴱ (Erased A) ↝[ k ] Contractible (Erased A)
Contractibleᴱ-Erased↔Contractible-Erased {A = A} ext =
Contractibleᴱ (Erased A) ↝⟨ inverse-erased-ext? Erased-Contractibleᴱ↔Contractibleᴱ-Erased ext ⟩
Erased (Contractibleᴱ A) ↔⟨ Erased-Contractibleᴱ↔Erased-Contractible ⟩
Erased (Contractible A) ↝⟨ Erased-H-level↔H-level ext 0 ⟩□
Contractible (Erased A) □