{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
open import Prelude as P hiding (id; _∘_; [_,_])
module Bi-invertibility.Erased
{e⁺}
(eq : ∀ {a p} → Equality-with-J a p e⁺)
{o h}
(Obj : Type o)
(Hom : Obj → Obj → Type h)
(id : {A : Obj} → Hom A A)
(_∘′_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C)
where
open import Bi-invertibility eq Obj Hom id _∘′_ as Bi
using (Has-left-inverse; Has-right-inverse; Is-bi-invertible;
Has-quasi-inverse; _≊_; _≅_)
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq using (_≃_)
open import Equivalence.Erased eq as EEq using (_≃ᴱ_)
open import Equivalence.Erased.Contractible-preimages eq as ECP
using (Contractibleᴱ)
open import Erased.Without-box-cong eq
open import Function-universe eq as F hiding (id; _∘_)
open import Logical-equivalence using (_⇔_)
open import H-level eq
open import H-level.Closure eq
open import Preimage eq
open import Surjection eq using (_↠_)
private
variable
A B : Obj
f : Hom A B
infixr 9 _∘_
_∘_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C
_∘_ = _∘′_
Has-left-inverseᴱ : @0 Hom A B → Type h
Has-left-inverseᴱ f = ∃ λ f⁻¹ → Erased (f⁻¹ ∘ f ≡ id)
Has-right-inverseᴱ : @0 Hom A B → Type h
Has-right-inverseᴱ f = ∃ λ f⁻¹ → Erased (f ∘ f⁻¹ ≡ id)
Is-bi-invertibleᴱ : @0 Hom A B → Type h
Is-bi-invertibleᴱ f =
Has-left-inverseᴱ f × Has-right-inverseᴱ f
Has-quasi-inverseᴱ : @0 Hom A B → Type h
Has-quasi-inverseᴱ f =
∃ λ f⁻¹ → Erased (f ∘ f⁻¹ ≡ id × f⁻¹ ∘ f ≡ id)
infix 4 _≊ᴱ_ _≅ᴱ_
_≊ᴱ_ : Obj → Obj → Type h
A ≊ᴱ B = ∃ λ (f : Hom A B) → Is-bi-invertibleᴱ f
_≅ᴱ_ : Obj → Obj → Type h
A ≅ᴱ B = ∃ λ (f : Hom A B) → Has-quasi-inverseᴱ f
Has-quasi-inverseᴱ→Is-bi-invertibleᴱ :
(@0 f : Hom A B) → Has-quasi-inverseᴱ f → Is-bi-invertibleᴱ f
Has-quasi-inverseᴱ→Is-bi-invertibleᴱ _ (f⁻¹ , [ f∘f⁻¹≡id , f⁻¹∘f≡id ]) =
(f⁻¹ , [ f⁻¹∘f≡id ])
, (f⁻¹ , [ f∘f⁻¹≡id ])
≅ᴱ→≊ᴱ : A ≅ᴱ B → A ≊ᴱ B
≅ᴱ→≊ᴱ = ∃-cong λ f → Has-quasi-inverseᴱ→Is-bi-invertibleᴱ f
Has-left-inverse→Has-left-inverseᴱ :
Has-left-inverse f → Has-left-inverseᴱ f
Has-left-inverse→Has-left-inverseᴱ = Σ-map P.id [_]→
@0 Has-left-inverse≃Has-left-inverseᴱ :
Has-left-inverse f ≃ Has-left-inverseᴱ f
Has-left-inverse≃Has-left-inverseᴱ {f} =
(∃ λ f⁻¹ → f⁻¹ ∘ f ≡ id ) ↔⟨ (∃-cong λ _ → inverse $ erased Erased↔) ⟩□
(∃ λ f⁻¹ → Erased (f⁻¹ ∘ f ≡ id)) □
Has-right-inverse→Has-right-inverseᴱ :
Has-right-inverse f → Has-right-inverseᴱ f
Has-right-inverse→Has-right-inverseᴱ = Σ-map P.id [_]→
@0 Has-right-inverse≃Has-right-inverseᴱ :
Has-right-inverse f ≃ Has-right-inverseᴱ f
Has-right-inverse≃Has-right-inverseᴱ {f} =
(∃ λ f⁻¹ → f ∘ f⁻¹ ≡ id ) ↔⟨ (∃-cong λ _ → inverse $ erased Erased↔) ⟩□
(∃ λ f⁻¹ → Erased (f ∘ f⁻¹ ≡ id)) □
Is-bi-invertible→Is-bi-invertibleᴱ :
Is-bi-invertible f → Is-bi-invertibleᴱ f
Is-bi-invertible→Is-bi-invertibleᴱ =
Σ-map Has-left-inverse→Has-left-inverseᴱ
Has-right-inverse→Has-right-inverseᴱ
@0 Is-bi-invertible≃Is-bi-invertibleᴱ :
Is-bi-invertible f ≃ Is-bi-invertibleᴱ f
Is-bi-invertible≃Is-bi-invertibleᴱ {f} =
Has-left-inverse f × Has-right-inverse f ↝⟨ Has-left-inverse≃Has-left-inverseᴱ ×-cong
Has-right-inverse≃Has-right-inverseᴱ ⟩□
Has-left-inverseᴱ f × Has-right-inverseᴱ f □
Has-quasi-inverse→Has-quasi-inverseᴱ :
Has-quasi-inverse f → Has-quasi-inverseᴱ f
Has-quasi-inverse→Has-quasi-inverseᴱ = Σ-map P.id [_]→
@0 Has-quasi-inverse≃Has-quasi-inverseᴱ :
Has-quasi-inverse f ≃ Has-quasi-inverseᴱ f
Has-quasi-inverse≃Has-quasi-inverseᴱ {f} =
(∃ λ f⁻¹ → f ∘ f⁻¹ ≡ id × f⁻¹ ∘ f ≡ id ) ↔⟨ (∃-cong λ _ → inverse $ erased Erased↔) ⟩□
(∃ λ f⁻¹ → Erased (f ∘ f⁻¹ ≡ id × f⁻¹ ∘ f ≡ id)) □
≊→≊ᴱ : A ≊ B → A ≊ᴱ B
≊→≊ᴱ = Σ-map P.id Is-bi-invertible→Is-bi-invertibleᴱ
@0 ≊≃≊ᴱ : (A ≊ B) ≃ (A ≊ᴱ B)
≊≃≊ᴱ {A} {B} =
(∃ λ (f : Hom A B) → Is-bi-invertible f) ↝⟨ (∃-cong λ _ → Is-bi-invertible≃Is-bi-invertibleᴱ) ⟩□
(∃ λ (f : Hom A B) → Is-bi-invertibleᴱ f) □
≅→≅ᴱ : A ≅ B → A ≅ᴱ B
≅→≅ᴱ = Σ-map P.id Has-quasi-inverse→Has-quasi-inverseᴱ
@0 ≅≃≅ᴱ : (A ≅ B) ≃ (A ≅ᴱ B)
≅≃≅ᴱ {A} {B} =
(∃ λ (f : Hom A B) → Has-quasi-inverse f) ↝⟨ (∃-cong λ _ → Has-quasi-inverse≃Has-quasi-inverseᴱ) ⟩□
(∃ λ (f : Hom A B) → Has-quasi-inverseᴱ f) □
module More
(@0 left-identity : {A B : Obj} (f : Hom A B) → id ∘ f ≡ f)
(@0 right-identity : {A B : Obj} (f : Hom A B) → f ∘ id ≡ f)
(@0 associativity : {A B C D : Obj}
(f : Hom C D) (g : Hom B C) (h : Hom A B) →
f ∘ (g ∘ h) ≡ (f ∘ g) ∘ h)
where
private
module @0 BiM =
Bi.More left-identity right-identity associativity
Is-bi-invertibleᴱ→Has-quasi-inverseᴱ :
Is-bi-invertibleᴱ f → Has-quasi-inverseᴱ f
Is-bi-invertibleᴱ→Has-quasi-inverseᴱ
{f} ((f⁻¹₁ , [ f⁻¹₁∘f≡id ]) , (f⁻¹₂ , [ f∘f⁻¹₂≡id ])) =
(f⁻¹₁ ∘ f ∘ f⁻¹₂)
, [ (f ∘ f⁻¹₁ ∘ f ∘ f⁻¹₂ ≡⟨ cong (f ∘_) $ associativity _ _ _ ⟩
f ∘ (f⁻¹₁ ∘ f) ∘ f⁻¹₂ ≡⟨ cong (λ f′ → f ∘ f′ ∘ f⁻¹₂) f⁻¹₁∘f≡id ⟩
f ∘ id ∘ f⁻¹₂ ≡⟨ cong (f ∘_) $ left-identity _ ⟩
f ∘ f⁻¹₂ ≡⟨ f∘f⁻¹₂≡id ⟩∎
id ∎)
, ((f⁻¹₁ ∘ f ∘ f⁻¹₂) ∘ f ≡⟨ cong (λ f′ → (f⁻¹₁ ∘ f′) ∘ f) f∘f⁻¹₂≡id ⟩
(f⁻¹₁ ∘ id) ∘ f ≡⟨ cong (_∘ f) $ right-identity _ ⟩
f⁻¹₁ ∘ f ≡⟨ f⁻¹₁∘f≡id ⟩∎
id ∎)
]
Contractibleᴱ-Has-left-inverseᴱ :
{@0 f : Hom A B} →
Has-quasi-inverseᴱ f → Contractibleᴱ (Has-left-inverseᴱ f)
Contractibleᴱ-Has-left-inverseᴱ {f} (f⁻¹ , [ f∘f⁻¹≡id , f⁻¹∘f≡id ]) =
ECP.Contractibleᴱ-⁻¹ᴱ
(_∘ f)
(_∘ f⁻¹)
(λ g →
(g ∘ f⁻¹) ∘ f ≡⟨ sym $ associativity _ _ _ ⟩
g ∘ f⁻¹ ∘ f ≡⟨ cong (g ∘_) f⁻¹∘f≡id ⟩
g ∘ id ≡⟨ right-identity _ ⟩∎
g ∎)
(λ g →
(g ∘ f) ∘ f⁻¹ ≡⟨ sym $ associativity _ _ _ ⟩
g ∘ f ∘ f⁻¹ ≡⟨ cong (g ∘_) f∘f⁻¹≡id ⟩
g ∘ id ≡⟨ right-identity _ ⟩∎
g ∎)
id
Contractibleᴱ-Has-right-inverseᴱ :
{@0 f : Hom A B} →
Has-quasi-inverseᴱ f → Contractibleᴱ (Has-right-inverseᴱ f)
Contractibleᴱ-Has-right-inverseᴱ {f} (f⁻¹ , [ f∘f⁻¹≡id , f⁻¹∘f≡id ]) =
ECP.Contractibleᴱ-⁻¹ᴱ
(f ∘_)
(f⁻¹ ∘_)
(λ g →
f ∘ f⁻¹ ∘ g ≡⟨ associativity _ _ _ ⟩
(f ∘ f⁻¹) ∘ g ≡⟨ cong (_∘ g) f∘f⁻¹≡id ⟩
id ∘ g ≡⟨ left-identity _ ⟩∎
g ∎)
(λ g →
f⁻¹ ∘ f ∘ g ≡⟨ associativity _ _ _ ⟩
(f⁻¹ ∘ f) ∘ g ≡⟨ cong (_∘ g) f⁻¹∘f≡id ⟩
id ∘ g ≡⟨ left-identity _ ⟩∎
g ∎)
id
@0 Is-bi-invertibleᴱ-propositional :
(f : Hom A B) → Is-proposition (Is-bi-invertibleᴱ f)
Is-bi-invertibleᴱ-propositional f = $⟨ BiM.Is-bi-invertible-propositional f ⟩
Is-proposition (Is-bi-invertible f) ↝⟨ H-level-cong _ 1 Is-bi-invertible≃Is-bi-invertibleᴱ ⦂ (_ → _) ⟩
Is-proposition (Is-bi-invertibleᴱ f) □
@0 Has-quasi-inverseᴱ-propositional-domain :
{f : Hom A B} →
Is-set (Hom A A) →
Is-proposition (Has-quasi-inverseᴱ f)
Has-quasi-inverseᴱ-propositional-domain {f} s =
$⟨ BiM.Has-quasi-inverse-propositional-domain s ⟩
Is-proposition (Has-quasi-inverse f) ↝⟨ H-level-cong _ 1 Has-quasi-inverse≃Has-quasi-inverseᴱ ⦂ (_ → _) ⟩□
Is-proposition (Has-quasi-inverseᴱ f) □
@0 Has-quasi-inverseᴱ-propositional-codomain :
{f : Hom A B} →
Is-set (Hom B B) →
Is-proposition (Has-quasi-inverseᴱ f)
Has-quasi-inverseᴱ-propositional-codomain {f} s =
$⟨ BiM.Has-quasi-inverse-propositional-codomain s ⟩
Is-proposition (Has-quasi-inverse f) ↝⟨ H-level-cong _ 1 Has-quasi-inverse≃Has-quasi-inverseᴱ ⦂ (_ → _) ⟩□
Is-proposition (Has-quasi-inverseᴱ f) □
Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ :
Has-quasi-inverseᴱ f ⇔ Is-bi-invertibleᴱ f
Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ = record
{ to = Has-quasi-inverseᴱ→Is-bi-invertibleᴱ _
; from = Is-bi-invertibleᴱ→Has-quasi-inverseᴱ
}
≅ᴱ⇔≊ᴱ : (A ≅ᴱ B) ⇔ (A ≊ᴱ B)
≅ᴱ⇔≊ᴱ = ∃-cong λ _ → Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ
Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-domain :
{f : Hom A B} →
@0 Is-set (Hom A A) →
Is-bi-invertibleᴱ f ≃ᴱ Has-quasi-inverseᴱ f
Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-domain s = EEq.⇔→≃ᴱ
(Is-bi-invertibleᴱ-propositional _)
(Has-quasi-inverseᴱ-propositional-domain s)
(_⇔_.from Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ)
(_⇔_.to Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ)
Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-codomain :
{f : Hom A B} →
@0 Is-set (Hom B B) →
Is-bi-invertibleᴱ f ≃ᴱ Has-quasi-inverseᴱ f
Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-codomain s = EEq.⇔→≃ᴱ
(Is-bi-invertibleᴱ-propositional _)
(Has-quasi-inverseᴱ-propositional-codomain s)
(_⇔_.from Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ)
(_⇔_.to Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ)
≊ᴱ≃ᴱ≅ᴱ-domain :
@0 Is-set (Hom A A) →
(A ≊ᴱ B) ≃ᴱ (A ≅ᴱ B)
≊ᴱ≃ᴱ≅ᴱ-domain s =
∃-cong λ _ → Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-domain s
≊ᴱ≃ᴱ≅ᴱ-codomain :
@0 Is-set (Hom B B) →
(A ≊ᴱ B) ≃ᴱ (A ≅ᴱ B)
≊ᴱ≃ᴱ≅ᴱ-codomain s =
∃-cong λ _ → Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-codomain s
@0 equality-characterisation-≊ᴱ :
(f g : A ≊ᴱ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
equality-characterisation-≊ᴱ f g =
f ≡ g ↝⟨ inverse $ Eq.≃-≡ (inverse ≊≃≊ᴱ) ⟩
_≃_.from ≊≃≊ᴱ f ≡ _≃_.from ≊≃≊ᴱ g ↝⟨ BiM.equality-characterisation-≊ _ _ ⟩□
proj₁ f ≡ proj₁ g □
@0 equality-characterisation-≅ᴱ-domain :
Is-set (Hom A A) →
(f g : A ≅ᴱ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
equality-characterisation-≅ᴱ-domain s f g =
f ≡ g ↝⟨ inverse $ Eq.≃-≡ (inverse ≅≃≅ᴱ) ⟩
_≃_.from ≅≃≅ᴱ f ≡ _≃_.from ≅≃≅ᴱ g ↝⟨ BiM.equality-characterisation-≅-domain s _ _ ⟩□
proj₁ f ≡ proj₁ g □
@0 equality-characterisation-≅ᴱ-codomain :
Is-set (Hom B B) →
(f g : A ≅ᴱ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
equality-characterisation-≅ᴱ-codomain s f g =
f ≡ g ↝⟨ inverse $ Eq.≃-≡ (inverse ≅≃≅ᴱ) ⟩
_≃_.from ≅≃≅ᴱ f ≡ _≃_.from ≅≃≅ᴱ g ↝⟨ BiM.equality-characterisation-≅-codomain s _ _ ⟩□
proj₁ f ≡ proj₁ g □
@0 Has-quasi-inverseᴱ≃id≡id-domain :
{f : Hom A B} →
Has-quasi-inverseᴱ f →
Has-quasi-inverseᴱ f ≃ (id ≡ id {A = A})
Has-quasi-inverseᴱ≃id≡id-domain {f} q-inv =
Has-quasi-inverseᴱ f ↝⟨ inverse Has-quasi-inverse≃Has-quasi-inverseᴱ ⟩
Has-quasi-inverse f ↝⟨ BiM.Has-quasi-inverse≃id≡id-domain (_≃_.from Has-quasi-inverse≃Has-quasi-inverseᴱ q-inv) ⟩□
id ≡ id □
@0 Has-quasi-inverseᴱ≃id≡id-codomain :
{f : Hom A B} →
Has-quasi-inverseᴱ f →
Has-quasi-inverseᴱ f ≃ (id ≡ id {A = B})
Has-quasi-inverseᴱ≃id≡id-codomain {f} q-inv =
Has-quasi-inverseᴱ f ↝⟨ inverse Has-quasi-inverse≃Has-quasi-inverseᴱ ⟩
Has-quasi-inverse f ↝⟨ BiM.Has-quasi-inverse≃id≡id-codomain (_≃_.from Has-quasi-inverse≃Has-quasi-inverseᴱ q-inv) ⟩□
id ≡ id □