{-# OPTIONS --without-K #-}
open import Equality
module Category
{reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where
open import Bijection eq hiding (id; _∘_; inverse; finally-↔)
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq
using (_≃_; ⟨_,_⟩; module _≃_; Is-equivalence)
open import Function-universe eq hiding (id) renaming (_∘_ to _⊚_)
open import H-level eq
open import H-level.Closure eq
open import Logical-equivalence using (module _⇔_)
open import Prelude as P hiding (id)
open import Univalence-axiom eq
Precategory′ : (ℓ₁ ℓ₂ : Level) → Set (lsuc (ℓ₁ ⊔ ℓ₂))
Precategory′ ℓ₁ ℓ₂ =
∃ λ (Obj : Set ℓ₁) →
∃ λ (HOM : Obj → Obj → SET ℓ₂) →
let Hom = λ X Y → proj₁ (HOM X Y) in
∃ λ (id : ∀ {X} → Hom X X) →
∃ λ (_∙_ : ∀ {X Y Z} → Hom X Y → Hom Y Z → Hom X Z) →
(∀ {X Y} {f : Hom X Y} → (id ∙ f) ≡ f) ×
(∀ {X Y} {f : Hom X Y} → (f ∙ id) ≡ f) ×
(∀ {X Y Z U} {f : Hom X Y} {g : Hom Y Z} {h : Hom Z U} →
(f ∙ (g ∙ h)) ≡ ((f ∙ g) ∙ h))
record Precategory (ℓ₁ ℓ₂ : Level) : Set (lsuc (ℓ₁ ⊔ ℓ₂)) where
field
precategory : Precategory′ ℓ₁ ℓ₂
Obj : Set ℓ₁
Obj = proj₁ precategory
HOM : Obj → Obj → SET ℓ₂
HOM = proj₁ (proj₂ precategory)
Hom : Obj → Obj → Set ℓ₂
Hom X Y = proj₁ (HOM X Y)
Hom-is-set : ∀ {X Y} → Is-set (Hom X Y)
Hom-is-set = proj₂ (HOM _ _)
id : ∀ {X} → Hom X X
id = proj₁ (proj₂ (proj₂ precategory))
infixl 10 _∙_
_∙_ : ∀ {X Y Z} → Hom X Y → Hom Y Z → Hom X Z
_∙_ = proj₁ (proj₂ (proj₂ (proj₂ precategory)))
left-identity : ∀ {X Y} {f : Hom X Y} → id ∙ f ≡ f
left-identity = proj₁ (proj₂ (proj₂ (proj₂ (proj₂ precategory))))
right-identity : ∀ {X Y} {f : Hom X Y} → f ∙ id ≡ f
right-identity =
proj₁ (proj₂ (proj₂ (proj₂ (proj₂ (proj₂ precategory)))))
assoc : ∀ {X Y Z U} {f : Hom X Y} {g : Hom Y Z} {h : Hom Z U} →
f ∙ (g ∙ h) ≡ (f ∙ g) ∙ h
assoc =
proj₂ (proj₂ (proj₂ (proj₂ (proj₂ (proj₂ precategory)))))
Is-isomorphism : ∀ {X Y} → Hom X Y → Set ℓ₂
Is-isomorphism f = ∃ λ g → (f ∙ g ≡ id) × (g ∙ f ≡ id)
infix 4 _≅_
_≅_ : Obj → Obj → Set ℓ₂
X ≅ Y = ∃ λ (f : Hom X Y) → Is-isomorphism f
infix 15 _¹ _⁻¹ _¹⁻¹ _⁻¹¹
_¹ : ∀ {X Y} → X ≅ Y → Hom X Y
f ¹ = proj₁ f
_⁻¹ : ∀ {X Y} → X ≅ Y → Hom Y X
f ⁻¹ = proj₁ (proj₂ f)
_¹⁻¹ : ∀ {X Y} (f : X ≅ Y) → f ¹ ∙ f ⁻¹ ≡ id
f ¹⁻¹ = proj₁ (proj₂ (proj₂ f))
_⁻¹¹ : ∀ {X Y} (f : X ≅ Y) → f ⁻¹ ∙ f ¹ ≡ id
f ⁻¹¹ = proj₂ (proj₂ (proj₂ f))
abstract
Is-isomorphism-propositional :
∀ {X Y} (f : Hom X Y) →
Is-proposition (Is-isomorphism f)
Is-isomorphism-propositional f =
_⇔_.from propositional⇔irrelevant
λ { (g , fg , gf) (g′ , fg′ , g′f) →
Σ-≡,≡→≡ (g ≡⟨ sym left-identity ⟩
id ∙ g ≡⟨ cong (λ h → h ∙ g) $ sym g′f ⟩
(g′ ∙ f) ∙ g ≡⟨ sym assoc ⟩
g′ ∙ (f ∙ g) ≡⟨ cong (_∙_ g′) fg ⟩
g′ ∙ id ≡⟨ right-identity ⟩∎
g′ ∎)
(Σ-≡,≡→≡ (_⇔_.to set⇔UIP Hom-is-set _ _)
(_⇔_.to set⇔UIP Hom-is-set _ _)) }
≡≃≡¹ : ∀ {X Y} {f g : X ≅ Y} → (f ≡ g) ≃ (f ¹ ≡ g ¹)
≡≃≡¹ {f = f} {g} =
(f ≡ g) ↔⟨ inverse $ ignore-propositional-component $ Is-isomorphism-propositional _ ⟩□
(f ¹ ≡ g ¹) □
≅-set : ∀ {X Y} → Is-set (X ≅ Y)
≅-set = Σ-closure 2 Hom-is-set
(λ _ → mono₁ 1 $ Is-isomorphism-propositional _)
id≅ : ∀ {X} → X ≅ X
id≅ = id , id , left-identity , right-identity
infixl 10 _∙≅_
_∙≅_ : ∀ {X Y Z} → X ≅ Y → Y ≅ Z → X ≅ Z
f ∙≅ g = (f ¹ ∙ g ¹) , (g ⁻¹ ∙ f ⁻¹) , fg f g , gf f g
where
abstract
fg : ∀ {X Y Z} (f : X ≅ Y) (g : Y ≅ Z) →
(f ¹ ∙ g ¹) ∙ (g ⁻¹ ∙ f ⁻¹) ≡ id
fg f g =
(f ¹ ∙ g ¹) ∙ (g ⁻¹ ∙ f ⁻¹) ≡⟨ sym assoc ⟩
f ¹ ∙ (g ¹ ∙ (g ⁻¹ ∙ f ⁻¹)) ≡⟨ cong (_∙_ (f ¹)) assoc ⟩
f ¹ ∙ ((g ¹ ∙ g ⁻¹) ∙ f ⁻¹) ≡⟨ cong (λ h → f ¹ ∙ (h ∙ f ⁻¹)) $ g ¹⁻¹ ⟩
f ¹ ∙ (id ∙ f ⁻¹) ≡⟨ cong (_∙_ (f ¹)) left-identity ⟩
f ¹ ∙ f ⁻¹ ≡⟨ f ¹⁻¹ ⟩∎
id ∎
gf : ∀ {X Y Z} (f : X ≅ Y) (g : Y ≅ Z) →
(g ⁻¹ ∙ f ⁻¹) ∙ (f ¹ ∙ g ¹) ≡ id
gf f g =
(g ⁻¹ ∙ f ⁻¹) ∙ (f ¹ ∙ g ¹) ≡⟨ sym assoc ⟩
g ⁻¹ ∙ (f ⁻¹ ∙ (f ¹ ∙ g ¹)) ≡⟨ cong (_∙_ (g ⁻¹)) assoc ⟩
g ⁻¹ ∙ ((f ⁻¹ ∙ f ¹) ∙ g ¹) ≡⟨ cong (λ h → g ⁻¹ ∙ (h ∙ g ¹)) $ f ⁻¹¹ ⟩
g ⁻¹ ∙ (id ∙ g ¹) ≡⟨ cong (_∙_ (g ⁻¹)) left-identity ⟩
g ⁻¹ ∙ g ¹ ≡⟨ g ⁻¹¹ ⟩∎
id ∎
infix 15 _⁻¹≅
_⁻¹≅ : ∀ {X Y} → X ≅ Y → Y ≅ X
f ⁻¹≅ = f ⁻¹ , f ¹ , f ⁻¹¹ , f ¹⁻¹
precategory-≅ : Precategory ℓ₁ ℓ₂
precategory-≅ = record { precategory =
Obj ,
(λ X Y → (X ≅ Y) , ≅-set) ,
id≅ , _∙≅_ ,
_≃_.from ≡≃≡¹ left-identity ,
_≃_.from ≡≃≡¹ right-identity ,
_≃_.from ≡≃≡¹ assoc }
≡→≅ : ∀ {X Y} → X ≡ Y → X ≅ Y
≡→≅ = elim (λ {X Y} _ → X ≅ Y) (λ _ → id≅)
≡→≅-refl : ∀ {X} → ≡→≅ (refl X) ≡ id≅
≡→≅-refl = elim-refl (λ {X Y} _ → X ≅ Y) _
≡→≅-¹ :
∀ {X Y} (X≡Y : X ≡ Y) →
≡→≅ X≡Y ¹ ≡ elim (λ {X Y} _ → Hom X Y) (λ _ → id) X≡Y
≡→≅-¹ {X} = elim¹
(λ X≡Y → ≡→≅ X≡Y ¹ ≡
elim (λ {X Y} _ → Hom X Y) (λ _ → id) X≡Y)
(≡→≅ (refl X) ¹ ≡⟨ cong _¹ ≡→≅-refl ⟩
id≅ ¹ ≡⟨⟩
id ≡⟨ sym $ elim-refl (λ {X Y} _ → Hom X Y) _ ⟩∎
elim (λ {X Y} _ → Hom X Y) (λ _ → id) (refl X) ∎)
≡→≅-equivalence-lemma :
∀ {X} →
(≡≃≅ : ∀ {Y} → (X ≡ Y) ≃ (X ≅ Y)) →
_≃_.to ≡≃≅ (refl X) ≡ id≅ →
∀ {Y} → Is-equivalence (≡→≅ {X = X} {Y = Y})
≡→≅-equivalence-lemma {X} ≡≃≅ ≡≃≅-refl {Y} =
Eq.respects-extensional-equality
(elim¹ (λ X≡Y → _≃_.to ≡≃≅ X≡Y ≡ ≡→≅ X≡Y)
(_≃_.to ≡≃≅ (refl X) ≡⟨ ≡≃≅-refl ⟩
id≅ ≡⟨ sym ≡→≅-refl ⟩∎
≡→≅ (refl X) ∎))
(_≃_.is-equivalence ≡≃≅)
precategory-Set :
(ℓ : Level) →
Extensionality ℓ ℓ →
Precategory (lsuc ℓ) ℓ
precategory-Set ℓ ext = record { precategory =
SET ℓ ,
(λ { (A , A-set) (B , B-set) →
(A → B) , Π-closure ext 2 (λ _ → B-set) }) ,
P.id ,
(λ f g → g ∘ f) ,
refl _ , refl _ , refl _ }
≃≃≅-Set :
(ℓ : Level) (ext : Extensionality ℓ ℓ) →
let open Precategory (precategory-Set ℓ ext) in
(X Y : Obj) → (Type X ≃ Type Y) ≃ (X ≅ Y)
≃≃≅-Set ℓ ext X Y = Eq.↔⇒≃ record
{ surjection = record
{ logical-equivalence = record
{ to = λ X≃Y → _≃_.to X≃Y , _≃_.from X≃Y ,
ext (_≃_.left-inverse-of X≃Y) ,
ext (_≃_.right-inverse-of X≃Y)
; from = λ X≅Y → Eq.↔⇒≃ record
{ surjection = record
{ logical-equivalence = record
{ to = proj₁ X≅Y
; from = proj₁ (proj₂ X≅Y)
}
; right-inverse-of = λ x →
cong (λ f → f x) $ proj₂ (proj₂ (proj₂ X≅Y))
}
; left-inverse-of = λ x →
cong (λ f → f x) $ proj₁ (proj₂ (proj₂ X≅Y))
}
}
; right-inverse-of = λ X≅Y →
_≃_.from (≡≃≡¹ {X = X} {Y = Y}) (refl (proj₁ X≅Y))
}
; left-inverse-of = λ X≃Y →
Eq.lift-equality ext (refl (_≃_.to X≃Y))
}
where open Precategory (precategory-Set ℓ ext) using (≡≃≡¹)
Category′ : (ℓ₁ ℓ₂ : Level) → Set (lsuc (ℓ₁ ⊔ ℓ₂))
Category′ ℓ₁ ℓ₂ =
∃ λ (C : Precategory ℓ₁ ℓ₂) →
∀ {X Y} → Is-equivalence (Precategory.≡→≅ C {X = X} {Y = Y})
record Category (ℓ₁ ℓ₂ : Level) : Set (lsuc (ℓ₁ ⊔ ℓ₂)) where
field
category : Category′ ℓ₁ ℓ₂
precategory : Precategory ℓ₁ ℓ₂
precategory = proj₁ category
open Precategory precategory public hiding (precategory)
≡→≅-equivalence : ∀ {X Y} → Is-equivalence (≡→≅ {X = X} {Y = Y})
≡→≅-equivalence = proj₂ category
≡≃≅ : ∀ {X Y} → (X ≡ Y) ≃ (X ≅ Y)
≡≃≅ = ⟨ _ , ≡→≅-equivalence ⟩
≅→≡ : ∀ {X Y} → X ≅ Y → X ≡ Y
≅→≡ = _≃_.from ≡≃≅
Obj-3 : H-level 3 Obj
Obj-3 X Y =
respects-surjection
(_≃_.surjection (Eq.inverse ≡≃≅))
2 ≅-set
category-≅ : Category ℓ₁ ℓ₂
category-≅ = record { category = precategory-≅ , is-equiv }
where
module P≅ = Precategory precategory-≅
abstract
is-equiv : ∀ {X Y} → Is-equivalence (P≅.≡→≅ {X = X} {Y = Y})
is-equiv (X≅Y , X≅Y-iso) =
Σ-map (Σ-map
P.id
(λ {X≡Y} ≡→≅[X≡Y]≡X≅Y →
elim (λ {X Y} X≡Y →
(X≅Y : X ≅ Y) (X≅Y-iso : P≅.Is-isomorphism X≅Y) →
≡→≅ X≡Y ≡ X≅Y →
P≅.≡→≅ X≡Y ≡ (X≅Y , X≅Y-iso))
(λ X X≅X X≅X-iso ≡→≅[refl]≡X≅X →
P≅.≡→≅ (refl X) ≡⟨ P≅.≡→≅-refl ⟩
P≅.id≅ ≡⟨ Σ-≡,≡→≡ (id≅ ≡⟨ sym ≡→≅-refl ⟩
≡→≅ (refl X) ≡⟨ ≡→≅[refl]≡X≅X ⟩∎
X≅X ∎)
(_⇔_.to propositional⇔irrelevant (P≅.Is-isomorphism-propositional _) _ _) ⟩∎
(X≅X , X≅X-iso) ∎)
X≡Y X≅Y X≅Y-iso
≡→≅[X≡Y]≡X≅Y))
(λ { {X≡Y , _} ∀y→≡y → λ { (X≡Y′ , ≡→≅[X≡Y′]≡X≅Y) →
let lemma =
≡→≅ X≡Y′ ≡⟨ elim (λ X≡Y′ → ≡→≅ X≡Y′ ≡ proj₁ (P≅.≡→≅ X≡Y′))
(λ X → ≡→≅ (refl X) ≡⟨ ≡→≅-refl ⟩
id≅ ≡⟨ cong proj₁ $ sym P≅.≡→≅-refl ⟩∎
proj₁ (P≅.≡→≅ (refl X)) ∎)
X≡Y′ ⟩
proj₁ (P≅.≡→≅ X≡Y′) ≡⟨ cong proj₁ ≡→≅[X≡Y′]≡X≅Y ⟩∎
X≅Y ∎ in
(X≡Y , _) ≡⟨ Σ-≡,≡→≡ (cong proj₁ (∀y→≡y (X≡Y′ , lemma)))
(_⇔_.to set⇔UIP P≅.≅-set _ _) ⟩∎
(X≡Y′ , _) ∎ } })
(≡→≅-equivalence X≅Y)
Hom-, : ∀ {X X′ Y Y′} {f : Hom X Y}
(p : X ≡ X′) (q : Y ≡ Y′) →
subst (uncurry Hom) (cong₂ _,_ p q) f ≡ ≡→≅ p ⁻¹ ∙ f ∙ ≡→≅ q ¹
Hom-, p q = elim
(λ p → ∀ q → ∀ {f} → subst (uncurry Hom) (cong₂ _,_ p q) f ≡
≡→≅ p ⁻¹ ∙ f ∙ ≡→≅ q ¹)
(λ X q → elim
(λ q → ∀ {f} → subst (uncurry Hom) (cong₂ _,_ (refl X) q) f ≡
≡→≅ (refl X) ⁻¹ ∙ f ∙ ≡→≅ q ¹)
(λ Y {f} →
subst (uncurry Hom) (cong₂ _,_ (refl X) (refl Y)) f ≡⟨ cong (λ eq → subst (uncurry Hom) eq f) $ cong₂-refl _,_ ⟩
subst (uncurry Hom) (refl (X , Y)) f ≡⟨ subst-refl (uncurry Hom) _ ⟩
f ≡⟨ sym left-identity ⟩
id ∙ f ≡⟨ cong (λ g → g ⁻¹ ∙ f) $ sym ≡→≅-refl ⟩
≡→≅ (refl X) ⁻¹ ∙ f ≡⟨ sym right-identity ⟩
≡→≅ (refl X) ⁻¹ ∙ f ∙ id ≡⟨ cong (λ g → ≡→≅ (refl X) ⁻¹ ∙ f ∙ g ¹) $ sym ≡→≅-refl ⟩∎
≡→≅ (refl X) ⁻¹ ∙ f ∙ ≡→≅ (refl Y) ¹ ∎)
q)
p q
≡→≅-trans : ∀ {X Y Z} (p : X ≡ Y) (q : Y ≡ Z) →
≡→≅ (trans p q) ≡ ≡→≅ p ∙≅ ≡→≅ q
≡→≅-trans {X} = elim¹
(λ p → ∀ q → ≡→≅ (trans p q) ≡ ≡→≅ p ∙≅ ≡→≅ q)
(elim¹
(λ q → ≡→≅ (trans (refl X) q) ≡ ≡→≅ (refl X) ∙≅ ≡→≅ q)
(≡→≅ (trans (refl X) (refl X)) ≡⟨ cong ≡→≅ trans-refl-refl ⟩
≡→≅ (refl X) ≡⟨ ≡→≅-refl ⟩
id≅ ≡⟨ sym $ Precategory.left-identity precategory-≅ ⟩
id≅ ∙≅ id≅ ≡⟨ sym $ cong₂ _∙≅_ ≡→≅-refl ≡→≅-refl ⟩∎
≡→≅ (refl X) ∙≅ ≡→≅ (refl X) ∎))
precategory-to-category :
∀ {c₁ c₂}
(C : Precategory c₁ c₂) →
let open Precategory C in
(≡≃≅ : ∀ {X Y} → (X ≡ Y) ≃ (X ≅ Y)) →
(∀ {X} → _≃_.to ≡≃≅ (refl X) ≡ id≅) →
Category c₁ c₂
precategory-to-category C ≡≃≅ ≡≃≅-refl = record
{ category = C , Precategory.≡→≅-equivalence-lemma C ≡≃≅ ≡≃≅-refl
}
category-Set :
(ℓ : Level) →
Extensionality ℓ ℓ →
Univalence ℓ →
Category (lsuc ℓ) ℓ
category-Set ℓ ext univ =
precategory-to-category precategory ≡≃≅ ≡≃≅-refl-is-id≅
where
precategory = precategory-Set ℓ ext
open Precategory precategory hiding (precategory)
abstract
cong-Type : {X Y : Obj} → (X ≡ Y) ≃ (Type X ≡ Type Y)
cong-Type = Eq.↔⇒≃ $ inverse $
ignore-propositional-component (H-level-propositional ext 2)
≃≃≅ : (X Y : Obj) → (Type X ≃ Type Y) ≃ (X ≅ Y)
≃≃≅ = ≃≃≅-Set ℓ ext
≡≃≅ : ∀ {X Y} → (X ≡ Y) ≃ (X ≅ Y)
≡≃≅ {X} {Y} = ≃≃≅ X Y ⊚ ≡≃≃ univ ⊚ cong-Type
≡≃≅-refl-is-id≅ : ∀ {X} → _≃_.to ≡≃≅ (refl X) ≡ id≅ {X = X}
≡≃≅-refl-is-id≅ {X} =
_≃_.to (≃≃≅ X X) (≡⇒≃ (proj₁ (Σ-≡,≡←≡ (refl X)))) ≡⟨ cong (_≃_.to (≃≃≅ X X) ∘ ≡⇒≃ ∘ proj₁) Σ-≡,≡←≡-refl ⟩
_≃_.to (≃≃≅ X X) (≡⇒≃ (refl (Type X))) ≡⟨ cong (_≃_.to (≃≃≅ X X)) ≡⇒≃-refl ⟩
_≃_.to (≃≃≅ X X) Eq.id ≡⟨ _≃_.from (≡≃≡¹ {X = X} {Y = X}) (refl P.id) ⟩∎
id≅ {X = X} ∎
category-Set-≅ :
(ℓ : Level) →
Extensionality ℓ ℓ →
Univalence ℓ →
Category (lsuc ℓ) ℓ
category-Set-≅ ℓ ext univ =
Category.category-≅ (category-Set ℓ ext univ)
private
Obj-category-Set-≅ :
∀ ℓ (ext : Extensionality ℓ ℓ) (univ : Univalence ℓ) →
Category.Obj (category-Set-≅ ℓ ext univ) ≡ SET ℓ
Obj-category-Set-≅ _ _ _ = refl _
Hom-category-Set-≅ :
∀ ℓ (ext : Extensionality ℓ ℓ) (univ : Univalence ℓ) →
Category.Hom (category-Set-≅ ℓ ext univ) ≡
Category._≅_ (category-Set ℓ ext univ)
Hom-category-Set-≅ _ _ _ = refl _