{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
open import Prelude hiding (id; _∘_)
module Bi-invertibility
{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 Derived-definitions-and-properties eq
open import Equivalence eq as Eq using (_≃_; Is-equivalence)
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 : Hom A B → Type h
Has-left-inverse f = ∃ λ f⁻¹ → f⁻¹ ∘ f ≡ id
Has-right-inverse : Hom A B → Type h
Has-right-inverse f = ∃ λ f⁻¹ → f ∘ f⁻¹ ≡ id
Is-bi-invertible : Hom A B → Type h
Is-bi-invertible f =
Has-left-inverse f × Has-right-inverse f
Has-quasi-inverse : Hom A B → Type h
Has-quasi-inverse f =
∃ λ f⁻¹ → 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 :
(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 Has-quasi-inverse→Is-bi-invertible
module More
(left-identity : {A B : Obj} (f : Hom A B) → id ∘ f ≡ f)
(right-identity : {A B : Obj} (f : Hom A B) → f ∘ id ≡ f)
(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
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 ∎)
Has-left-inverse-contractible :
Has-quasi-inverse f → Contractible (Has-left-inverse f)
Has-left-inverse-contractible {f} (f⁻¹ , f∘f⁻¹≡id , f⁻¹∘f≡id) =
bijection⁻¹-contractible (record
{ surjection = record
{ logical-equivalence = record
{ to = _∘ f
; from = _∘ f⁻¹
}
; right-inverse-of = λ g →
(g ∘ f⁻¹) ∘ f ≡⟨ sym $ associativity _ _ _ ⟩
g ∘ f⁻¹ ∘ f ≡⟨ cong (g ∘_) f⁻¹∘f≡id ⟩
g ∘ id ≡⟨ right-identity _ ⟩∎
g ∎
}
; left-inverse-of = λ g →
(g ∘ f) ∘ f⁻¹ ≡⟨ sym $ associativity _ _ _ ⟩
g ∘ f ∘ f⁻¹ ≡⟨ cong (g ∘_) f∘f⁻¹≡id ⟩
g ∘ id ≡⟨ right-identity _ ⟩∎
g ∎
})
id
Has-right-inverse-contractible :
Has-quasi-inverse f → Contractible (Has-right-inverse f)
Has-right-inverse-contractible {f} (f⁻¹ , f∘f⁻¹≡id , f⁻¹∘f≡id) =
bijection⁻¹-contractible (record
{ surjection = record
{ logical-equivalence = record
{ to = f ∘_
; from = f⁻¹ ∘_
}
; right-inverse-of = λ g →
f ∘ f⁻¹ ∘ g ≡⟨ associativity _ _ _ ⟩
(f ∘ f⁻¹) ∘ g ≡⟨ cong (_∘ g) f∘f⁻¹≡id ⟩
id ∘ g ≡⟨ left-identity _ ⟩∎
g ∎
}
; left-inverse-of = λ g →
f⁻¹ ∘ f ∘ g ≡⟨ associativity _ _ _ ⟩
(f⁻¹ ∘ f) ∘ g ≡⟨ cong (_∘ g) f⁻¹∘f≡id ⟩
id ∘ g ≡⟨ left-identity _ ⟩∎
g ∎
})
id
Is-bi-invertible-propositional :
(f : Hom A B) → Is-proposition (Is-bi-invertible f)
Is-bi-invertible-propositional f =
[inhabited⇒+]⇒+ 0 λ b →
let q = Is-bi-invertible→Has-quasi-inverse b in
mono₁ 0 $
×-closure 0
(Has-left-inverse-contractible q)
(Has-right-inverse-contractible q)
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 = $⟨ (λ inv → Σ-closure 1
(mono₁ 0 $ Has-right-inverse-contractible inv)
(λ _ → s)) ⟩
(Has-quasi-inverse f →
Is-proposition (∃ λ ((f⁻¹ , _) : Has-right-inverse f) →
f⁻¹ ∘ f ≡ id)) ↝⟨ (∀-cong _ λ _ → H-level-cong _ 1 (inverse Σ-assoc)) ⟩
(Has-quasi-inverse f → Is-proposition (Has-quasi-inverse f)) ↝⟨ [inhabited⇒+]⇒+ 0 ⟩□
Is-proposition (Has-quasi-inverse f) □
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 = $⟨ (λ inv → Σ-closure 1
(mono₁ 0 $ Has-left-inverse-contractible inv)
(λ _ → s)) ⟩
(Has-quasi-inverse f →
Is-proposition (∃ λ ((f⁻¹ , _) : Has-left-inverse f) →
f ∘ f⁻¹ ≡ id)) ↝⟨ (∀-cong _ λ _ → H-level-cong _ 1 lemma) ⟩
(Has-quasi-inverse f → Is-proposition (Has-quasi-inverse f)) ↝⟨ [inhabited⇒+]⇒+ 0 ⟩□
Is-proposition (Has-quasi-inverse f) □
where
lemma =
(∃ λ ((f⁻¹ , _) : Has-left-inverse f) → f ∘ f⁻¹ ≡ id) ↔⟨⟩
(∃ λ ((f⁻¹ , _) : ∃ λ f⁻¹ → f⁻¹ ∘ f ≡ id) → f ∘ f⁻¹ ≡ id) ↝⟨ inverse Σ-assoc ⟩
(∃ λ f⁻¹ → f⁻¹ ∘ f ≡ id × f ∘ f⁻¹ ≡ id) ↝⟨ (∃-cong λ _ → ×-comm) ⟩
(∃ λ f⁻¹ → f ∘ f⁻¹ ≡ id × f⁻¹ ∘ f ≡ id) ↔⟨⟩
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
{ logical-equivalence = record
{ to = Has-quasi-inverse→Is-bi-invertible _
; from = Is-bi-invertible→Has-quasi-inverse
}
; right-inverse-of = λ _ → Is-bi-invertible-propositional _ _ _
}
≅↠≊ : (A ≅ B) ↠ (A ≊ B)
≅↠≊ = ∃-cong λ _ → Has-quasi-inverse↠Is-bi-invertible
Is-bi-invertible≃Has-quasi-inverse-domain :
{f : Hom A B} →
Is-set (Hom A A) →
Is-bi-invertible f ≃ Has-quasi-inverse f
Is-bi-invertible≃Has-quasi-inverse-domain s =
inverse $ Eq.↔⇒≃ (record
{ surjection = Has-quasi-inverse↠Is-bi-invertible
; left-inverse-of = λ _ →
Has-quasi-inverse-propositional-domain s _ _
})
Is-bi-invertible≃Has-quasi-inverse-codomain :
{f : Hom A B} →
Is-set (Hom B B) →
Is-bi-invertible f ≃ Has-quasi-inverse f
Is-bi-invertible≃Has-quasi-inverse-codomain s =
inverse $ Eq.↔⇒≃ (record
{ surjection = Has-quasi-inverse↠Is-bi-invertible
; left-inverse-of = λ _ →
Has-quasi-inverse-propositional-codomain s _ _
})
≊≃≅-domain :
Is-set (Hom A A) →
(A ≊ B) ≃ (A ≅ B)
≊≃≅-domain s =
∃-cong λ _ → Is-bi-invertible≃Has-quasi-inverse-domain s
≊≃≅-codomain :
Is-set (Hom B B) →
(A ≊ B) ≃ (A ≅ B)
≊≃≅-codomain s =
∃-cong λ _ → Is-bi-invertible≃Has-quasi-inverse-codomain s
equality-characterisation-≊ :
(f g : A ≊ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
equality-characterisation-≊ _ _ =
Eq.↔⇒≃ $ inverse $ ignore-propositional-component $
Is-bi-invertible-propositional _
equality-characterisation-≅-domain :
Is-set (Hom A A) →
(f g : A ≅ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
equality-characterisation-≅-domain s _ _ =
Eq.↔⇒≃ $ inverse $ ignore-propositional-component $
Has-quasi-inverse-propositional-domain s
equality-characterisation-≅-codomain :
Is-set (Hom B B) →
(f g : A ≅ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
equality-characterisation-≅-codomain s _ _ =
Eq.↔⇒≃ $ inverse $ ignore-propositional-component $
Has-quasi-inverse-propositional-codomain s
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@(f⁻¹ , _ , f⁻¹∘f≡id) =
Has-quasi-inverse f ↔⟨ Σ-assoc ⟩
(∃ λ ((f⁻¹ , _) : Has-right-inverse f) → f⁻¹ ∘ f ≡ id) ↔⟨ drop-⊤-left-Σ (_⇔_.to contractible⇔↔⊤ $ Has-right-inverse-contractible q-inv) ⟩
(f⁻¹ ∘ id) ∘ f ≡ id ↝⟨ ≡⇒↝ _ $ cong (λ f′ → f′ ∘ _ ≡ _) $ right-identity _ ⟩
f⁻¹ ∘ f ≡ id ↝⟨ ≡⇒↝ _ $ cong (_≡ _) f⁻¹∘f≡id ⟩□
id ≡ id □
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@(f⁻¹ , f∘f⁻¹≡id , _) =
Has-quasi-inverse f ↔⟨ Σ-assoc F.∘ (∃-cong λ _ → ×-comm) ⟩
(∃ λ ((f⁻¹ , _) : Has-left-inverse f) → f ∘ f⁻¹ ≡ id) ↔⟨ drop-⊤-left-Σ (_⇔_.to contractible⇔↔⊤ $ Has-left-inverse-contractible q-inv) ⟩
f ∘ id ∘ f⁻¹ ≡ id ↝⟨ ≡⇒↝ _ $ cong (λ f′ → _ ∘ f′ ≡ _) $ left-identity _ ⟩
f ∘ f⁻¹ ≡ id ↝⟨ ≡⇒↝ _ $ cong (_≡ _) f∘f⁻¹≡id ⟩□
id ≡ id □
id-≅ : A ≅ A
id-≅ = id , id , left-identity id , right-identity id
≡→≅ : A ≡ B → A ≅ B
≡→≅ = elim (λ {A B} _ → A ≅ B) (λ _ → id-≅)
≡→≅-refl : ≡→≅ (refl A) ≡ id-≅
≡→≅-refl = elim-refl _ _
Univalence-≅ : Type (o ⊔ h)
Univalence-≅ = {A B : Obj} → Is-equivalence (≡→≅ {A = A} {B = B})
≡≃≅→Univalence-≅ :
(∀ {A B} → (A ≡ B) ≃ (A ≅ B)) →
Univalence-≅
≡≃≅→Univalence-≅ ≡≃≅ =
Eq.≡≃→≡→→Is-equivalence (_ ≅_) ≡≃≅ ≡→≅
id-≊ : A ≊ A
id-≊ = id , (id , left-identity id) , (id , right-identity id)
≡→≊ : A ≡ B → A ≊ B
≡→≊ = elim (λ {A B} _ → A ≊ B) (λ _ → id-≊)
≡→≊-refl : ≡→≊ (refl A) ≡ id-≊
≡→≊-refl = elim-refl _ _
Univalence-≊ : Type (o ⊔ h)
Univalence-≊ = {A B : Obj} → Is-equivalence (≡→≊ {A = A} {B = B})
≡≃≊→Univalence-≊ :
(∀ {A B} → (A ≡ B) ≃ (A ≊ B)) →
Univalence-≊
≡≃≊→Univalence-≊ ≡≃≊ =
Eq.≡≃→≡→→Is-equivalence (_ ≊_) ≡≃≊ ≡→≊