Created
September 10, 2018 19:22
-
-
Save Taneb/6bca8c7d5fd47b12db32b3884cab097e to your computer and use it in GitHub Desktop.
Category theory in Agda!
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module Cat where | |
| open import Relation.Binary | |
| open import Relation.Binary.PropositionalEquality | |
| open import Level | |
| record Category (o a ℓ : Level) : Set (suc (o ⊔ a ⊔ ℓ)) where | |
| infix 4 _≈_ | |
| infixr 9 _∘_ | |
| field | |
| Ob : Set o | |
| Mor′ : Ob → Ob → Setoid a ℓ | |
| Mor : Ob → Ob → Set a | |
| Mor α β = Setoid.Carrier (Mor′ α β) | |
| _≈_ : {α β : Ob} → Rel (Mor α β) ℓ | |
| _≈_ {α} {β} = Setoid._≈_ (Mor′ α β) | |
| field | |
| ι : (α : Ob) → Mor α α | |
| _∘_ : {α β γ : Ob} (f : Mor β γ) (g : Mor α β) → Mor α γ | |
| ∘-ι : ∀ {α β : Ob} → (f : Mor α β) → f ∘ ι α ≈ f | |
| ι-∘ : ∀ {α β : Ob} → (f : Mor α β) → ι β ∘ f ≈ f | |
| ∘-∘ : ∀ {α β γ δ} (f : Mor γ δ) (g : Mor β γ) (h : Mor α β) → f ∘ (g ∘ h) ≈ (f ∘ g) ∘ h | |
| ∘-cong : {α β γ : Ob} {f f′ : Mor β γ} {g g′ : Mor α β} → f ≈ f′ → g ≈ g′ → f ∘ g ≈ f′ ∘ g′ | |
| Set′ : (ℓ : Level) → Category (suc ℓ) _ _ | |
| Set′ ℓ = record { | |
| Ob = Set ℓ; | |
| Mor′ = _→-setoid_; | |
| ι = λ _ x → x; | |
| _∘_ = λ f g x → f (g x); | |
| ∘-ι = λ f x → refl; | |
| ι-∘ = λ f x → refl; | |
| ∘-∘ = λ f g h x → refl; | |
| ∘-cong = λ {_} {_} {_} {_} {f′} {g} {_} p q x → Setoid.trans (setoid _) (p (g x)) (cong f′ (q x)) | |
| } | |
| where | |
| open import Relation.Binary.PropositionalEquality | |
| open Category using (Ob; Mor; ι) | |
| record IsProduct {o a ℓ : Level} (𝒞 : Category o a ℓ) (α β α×β : Ob 𝒞) : Set (o ⊔ a ⊔ ℓ) where | |
| open Category 𝒞 using (_∘_; _≈_) | |
| field | |
| π₁ : Mor 𝒞 α×β α | |
| π₂ : Mor 𝒞 α×β β | |
| <_,_> : {γ : Ob 𝒞} (f : Mor 𝒞 γ α) (g : Mor 𝒞 γ β) → Mor 𝒞 γ α×β | |
| π₁-× : {γ : Ob 𝒞} (f : Mor 𝒞 γ α) (g : Mor 𝒞 γ β) → π₁ ∘ < f , g > ≈ f | |
| π₂-× : {γ : Ob 𝒞} (f : Mor 𝒞 γ α) (g : Mor 𝒞 γ β) → π₂ ∘ < f , g > ≈ g | |
| ×-unique : {γ : Ob 𝒞} (g : Mor 𝒞 γ α×β) → < π₁ ∘ g , π₂ ∘ g > ≈ g | |
| record HasProducts {o a ℓ : Level} (𝒞 : Category o a ℓ) : Set (o ⊔ a ⊔ ℓ) where | |
| open Category 𝒞 using (_∘_; _≈_) | |
| field | |
| _×_ : Ob 𝒞 → Ob 𝒞 → Ob 𝒞 | |
| π₁ : {α β : Ob 𝒞} → Mor 𝒞 (α × β) α | |
| π₂ : {α β : Ob 𝒞} → Mor 𝒞 (α × β) β | |
| <_,_> : {α β γ : Ob 𝒞} (f : Mor 𝒞 α β) (g : Mor 𝒞 α γ) → Mor 𝒞 α (β × γ) | |
| π₁-× : {α β γ : Ob 𝒞} (f : Mor 𝒞 α β) (g : Mor 𝒞 α γ) → π₁ ∘ < f , g > ≈ f | |
| π₂-× : {α β γ : Ob 𝒞} (f : Mor 𝒞 α β) (g : Mor 𝒞 α γ) → π₂ ∘ < f , g > ≈ g | |
| ×-unique : {α β γ : Ob 𝒞} (g : Mor 𝒞 α (β × γ)) → < π₁ ∘ g , π₂ ∘ g > ≈ g | |
| isProduct : ∀ α β → IsProduct 𝒞 α β (α × β) | |
| isProduct α β = record { | |
| π₁ = π₁; | |
| π₂ = π₂; | |
| <_,_> = <_,_>; | |
| π₁-× = π₁-×; | |
| π₂-× = π₂-×; | |
| ×-unique = ×-unique | |
| } | |
| _××_ : {α β γ δ : Ob 𝒞} (f : Mor 𝒞 α β) (g : Mor 𝒞 γ δ) → Mor 𝒞 (α × γ) (β × δ) | |
| f ×× g = < f ∘ π₁ , g ∘ π₂ > | |
| SetHasProducts : ∀ {ℓ} → HasProducts (Set′ ℓ) | |
| SetHasProducts = record { | |
| _×_ = _×_; | |
| π₁ = proj₁; | |
| π₂ = proj₂; | |
| <_,_> = <_,_>; | |
| π₁-× = λ f g x → refl; | |
| π₂-× = λ f g x → refl; | |
| ×-unique = λ g x → refl | |
| } | |
| where | |
| open import Data.Product | |
| _ᵒᵖ : {o a ℓ : Level} → Category o a ℓ → Category o a ℓ | |
| 𝒞 ᵒᵖ = record { | |
| Ob = Ob 𝒞; | |
| Mor′ = λ α β → Mor′ β α; | |
| ι = ι 𝒞; | |
| _∘_ = λ f g → g ∘ f; | |
| ∘-ι = ι-∘; | |
| ι-∘ = ∘-ι; | |
| ∘-∘ = λ f g h → Setoid.sym (Mor′ _ _) (∘-∘ h g f); | |
| ∘-cong = λ p q → ∘-cong q p | |
| } | |
| where | |
| open Category 𝒞 | |
| HasCoproducts : {o a ℓ : Level} (𝒞 : Category o a ℓ) → Set (o ⊔ a ⊔ ℓ) | |
| HasCoproducts 𝒞 = HasProducts (𝒞 ᵒᵖ) | |
| SetHasCoproducts : ∀ {ℓ} → HasCoproducts (Set′ ℓ) | |
| SetHasCoproducts = record { | |
| _×_ = _⊎_; | |
| π₁ = inj₁; | |
| π₂ = inj₂; | |
| <_,_> = [_,_]; | |
| π₁-× = λ f g x → refl; | |
| π₂-× = λ f g x → refl; | |
| ×-unique = λ g → λ { (inj₁ x) → refl ; (inj₂ y) → refl} | |
| } | |
| where | |
| open import Data.Sum | |
| record HasTerminal {o a ℓ : Level} (𝒞 : Category o a ℓ) : Set (o ⊔ a ⊔ ℓ) where | |
| open Category 𝒞 using (_≈_) | |
| field | |
| ⊤ : Ob 𝒞 | |
| terminate : (α : Ob 𝒞) → Mor 𝒞 α ⊤ | |
| terminal : {α : Ob 𝒞} (f : Mor 𝒞 α ⊤) → f ≈ terminate α | |
| SetHasTerminal : ∀ {ℓ} → HasTerminal (Set′ ℓ) | |
| SetHasTerminal = record { | |
| ⊤ = Lift ⊤; | |
| terminate = λ α x → lift tt; | |
| terminal = λ f x → refl | |
| } | |
| where | |
| open import Data.Unit | |
| HasInitial : {o a ℓ : Level} (𝒞 : Category o a ℓ) → Set (o ⊔ a ⊔ ℓ) | |
| HasInitial 𝒞 = HasTerminal (𝒞 ᵒᵖ) | |
| SetHasinitial : ∀ {ℓ} → HasInitial (Set′ ℓ) | |
| SetHasinitial = record { | |
| ⊤ = Lift ⊥; | |
| terminate = λ α (); | |
| terminal = λ f () | |
| } | |
| where | |
| open import Data.Empty | |
| record HasExponential {o a ℓ : Level} {𝒞 : Category o a ℓ} (Π : HasProducts 𝒞) : Set (o ⊔ a ⊔ ℓ) where | |
| open Category 𝒞 using (_∘_; _≈_) | |
| open HasProducts Π using (_×_; _××_) | |
| field | |
| _^_ : Ob 𝒞 → Ob 𝒞 → Ob 𝒞 | |
| eval : {α β : Ob 𝒞} → Mor 𝒞 ((β ^ α) × α) β | |
| transpose : {α β γ : Ob 𝒞} (g : Mor 𝒞 (α × β) γ) → Mor 𝒞 α (γ ^ β) | |
| evaluates : {α β γ : Ob 𝒞} (g : Mor 𝒞 (α × β) γ) → eval ∘ (transpose g ×× ι 𝒞 _) ≈ g | |
| transposes : {α β γ : Ob 𝒞} (h : Mor 𝒞 α (γ ^ β)) → transpose (eval ∘ (h ×× ι 𝒞 _)) ≈ h | |
| open import Relation.Binary.PropositionalEquality | |
| SetHasExponential : ∀ {ℓ} → Extensionality ℓ ℓ → HasExponential (SetHasProducts) | |
| SetHasExponential extensionality = record { | |
| _^_ = λ α β → β → α; | |
| eval = λ { (f , x) → f x}; | |
| transpose = λ g x y → g (x , y); | |
| evaluates = λ g x → refl; | |
| transposes = λ h x → extensionality λ y → refl | |
| } | |
| where | |
| open import Data.Product | |
| record Functor {oₛ aₛ ℓₛ oₜ aₜ ℓₜ} (𝒮 : Category oₛ aₛ ℓₛ) (𝒯 : Category oₜ aₜ ℓₜ) : Set (oₛ ⊔ aₛ ⊔ oₜ ⊔ aₜ ⊔ ℓₛ ⊔ ℓₜ) where | |
| open Category 𝒮 using () renaming (_≈_ to _∼_; _∘_ to _∙_) | |
| open Category 𝒯 using (_≈_; _∘_) | |
| field | |
| ⟨_⟩ : Ob 𝒮 → Ob 𝒯 | |
| map : {α β : Ob 𝒮} → Mor 𝒮 α β → Mor 𝒯 ⟨ α ⟩ ⟨ β ⟩ | |
| map-ι : (α : Ob 𝒮) → map (ι 𝒮 α) ≈ ι 𝒯 ⟨ α ⟩ | |
| map-∘ : {α β γ : Ob 𝒮} (f : Mor 𝒮 β γ) (g : Mor 𝒮 α β) → map (f ∙ g) ≈ map f ∘ map g | |
| map-≈ : {α β : Ob 𝒮} {f f′ : Mor 𝒮 α β} → f ∼ f′ → map f ≈ map f′ | |
| record NaturalTransformation {oₛ aₛ ℓₛ oₜ aₜ ℓₜ : Level} {𝒮 : Category oₛ aₛ ℓₛ} {𝒯 : Category oₜ aₜ ℓₜ} (F G : Functor 𝒮 𝒯) : Set (oₛ ⊔ aₛ ⊔ aₜ ⊔ ℓₜ) where | |
| open Functor F using (⟨_⟩) renaming (map to Fmap) | |
| open Functor G using () renaming (⟨_⟩ to ⟪_⟫; map to Gmap) | |
| open Category 𝒯 using (_∘_; _≈_) | |
| field | |
| component : (α : Ob 𝒮) → Mor 𝒯 ⟨ α ⟩ ⟪ α ⟫ | |
| natural : {α β : Ob 𝒮} (f : Mor 𝒮 α β) → component β ∘ Fmap f ≈ Gmap f ∘ component α | |
| record IsIsomorphism {o a ℓ : Level} (𝒞 : Category o a ℓ) {α β : Ob 𝒞} (f : Mor 𝒞 α β) : Set (a ⊔ ℓ) where | |
| open Category 𝒞 using (_∘_; _≈_) | |
| field | |
| inverse : Mor 𝒞 β α | |
| retract : f ∘ inverse ≈ ι 𝒞 β | |
| section : inverse ∘ f ≈ ι 𝒞 α | |
| record Isomorphism {o a ℓ : Level} (𝒞 : Category o a ℓ) (α β : Ob 𝒞) : Set (a ⊔ ℓ) where | |
| field | |
| iso : Mor 𝒞 α β | |
| isIsomorphism : IsIsomorphism 𝒞 iso | |
| open IsIsomorphism isIsomorphism public | |
| IsomorphismSetoid : {o a ℓ : Level} (𝒞 : Category o a ℓ) → Setoid o (a ⊔ ℓ) | |
| IsomorphismSetoid 𝒞 = record { | |
| Carrier = Ob 𝒞; | |
| _≈_ = Isomorphism 𝒞; | |
| isEquivalence = record { | |
| refl = record { | |
| iso = ι 𝒞 _; | |
| isIsomorphism = record { | |
| inverse = ι 𝒞 _; | |
| retract = ι-∘ _; | |
| section = ∘-ι _ | |
| } | |
| }; | |
| sym = λ p → record { | |
| iso = Isomorphism.inverse p; | |
| isIsomorphism = record { | |
| inverse = Isomorphism.iso p; | |
| retract = Isomorphism.section p; | |
| section = Isomorphism.retract p | |
| } | |
| }; | |
| trans = λ p q → record { | |
| iso = Isomorphism.iso q ∘ Isomorphism.iso p; | |
| isIsomorphism = record { | |
| inverse = Isomorphism.inverse p ∘ Isomorphism.inverse q; | |
| retract = begin⟨ Mor′ _ _ ⟩ | |
| (Isomorphism.iso q ∘ Isomorphism.iso p) ∘ (Isomorphism.inverse p ∘ Isomorphism.inverse q) | |
| ≈⟨ Setoid.sym (Mor′ _ _) (∘-∘ _ _ _) ⟩ | |
| Isomorphism.iso q ∘ (Isomorphism.iso p ∘ (Isomorphism.inverse p ∘ Isomorphism.inverse q)) | |
| ≈⟨ ∘-cong (Setoid.refl (Mor′ _ _)) (∘-∘ _ _ _) ⟩ | |
| Isomorphism.iso q ∘ ((Isomorphism.iso p ∘ Isomorphism.inverse p) ∘ Isomorphism.inverse q) | |
| ≈⟨ ∘-cong (Setoid.refl (Mor′ _ _)) (∘-cong (Isomorphism.retract p) (Setoid.refl (Mor′ _ _))) ⟩ | |
| Isomorphism.iso q ∘ (ι 𝒞 _ ∘ Isomorphism.inverse q) | |
| ≈⟨ ∘-cong (Setoid.refl (Mor′ _ _)) (ι-∘ _) ⟩ | |
| Isomorphism.iso q ∘ Isomorphism.inverse q | |
| ≈⟨ Isomorphism.retract q ⟩ | |
| ι 𝒞 _ | |
| ∎; | |
| section = begin⟨ Mor′ _ _ ⟩ | |
| (Isomorphism.inverse p ∘ Isomorphism.inverse q) ∘ (Isomorphism.iso q ∘ Isomorphism.iso p) | |
| ≈⟨ Setoid.sym (Mor′ _ _) (∘-∘ _ _ _) ⟩ | |
| Isomorphism.inverse p ∘ (Isomorphism.inverse q ∘ (Isomorphism.iso q ∘ Isomorphism.iso p)) | |
| ≈⟨ ∘-cong (Setoid.refl (Mor′ _ _)) (∘-∘ _ _ _) ⟩ | |
| Isomorphism.inverse p ∘ ((Isomorphism.inverse q ∘ Isomorphism.iso q) ∘ Isomorphism.iso p) | |
| ≈⟨ ∘-cong (Setoid.refl (Mor′ _ _)) (∘-cong (Isomorphism.section q) (Setoid.refl (Mor′ _ _))) ⟩ | |
| Isomorphism.inverse p ∘ (ι 𝒞 _ ∘ Isomorphism.iso p) | |
| ≈⟨ ∘-cong (Setoid.refl (Mor′ _ _)) (ι-∘ _) ⟩ | |
| Isomorphism.inverse p ∘ Isomorphism.iso p | |
| ≈⟨ Isomorphism.section p ⟩ | |
| ι 𝒞 _ | |
| ∎ | |
| } | |
| } | |
| } | |
| } | |
| where | |
| open Category 𝒞 using (Mor′; _∘_; ι-∘; ∘-ι; ∘-∘; ∘-cong) | |
| open import Relation.Binary.SetoidReasoning | |
| [_,_] : {oₛ aₛ ℓₛ oₜ aₜ ℓₜ : Level} (𝒮 : Category oₛ aₛ ℓₛ) (𝒯 : Category oₜ aₜ ℓₜ) → Category _ _ _ | |
| [ 𝒮 , 𝒯 ] = record { | |
| Ob = Functor 𝒮 𝒯; | |
| Mor′ = λ F G → record { | |
| Carrier = NaturalTransformation F G; | |
| _≈_ = λ ℵ ℶ → (α : Ob 𝒮) → NaturalTransformation.component ℵ α ≈ NaturalTransformation.component ℶ α; | |
| isEquivalence = record { | |
| refl = λ _ → Setoid.refl (Mor′ _ _); | |
| sym = λ p α → Setoid.sym (Mor′ _ _) (p α); | |
| trans = λ p q → λ α → Setoid.trans (Mor′ _ _) (p α) (q α) | |
| } | |
| }; | |
| _∘_ = λ {F} {G} {H} ℵ ℶ → record { | |
| component = λ α → NaturalTransformation.component ℵ α ∘ NaturalTransformation.component ℶ α; | |
| natural = λ f → begin⟨ Mor′ _ _ ⟩ | |
| (NaturalTransformation.component ℵ _ ∘ NaturalTransformation.component ℶ _) ∘ Functor.map F f | |
| ≈⟨ Setoid.sym (Mor′ _ _) (∘-∘ _ _ _) ⟩ | |
| NaturalTransformation.component ℵ _ ∘ (NaturalTransformation.component ℶ _ ∘ Functor.map F f) | |
| ≈⟨ ∘-cong (Setoid.refl (Mor′ _ _)) (NaturalTransformation.natural ℶ _) ⟩ | |
| NaturalTransformation.component ℵ _ ∘ (Functor.map G f ∘ NaturalTransformation.component ℶ _) | |
| ≈⟨ ∘-∘ _ _ _ ⟩ | |
| (NaturalTransformation.component ℵ _ ∘ Functor.map G f) ∘ NaturalTransformation.component ℶ _ | |
| ≈⟨ ∘-cong (NaturalTransformation.natural ℵ _) (Setoid.refl (Mor′ _ _)) ⟩ | |
| (Functor.map H f ∘ NaturalTransformation.component ℵ _) ∘ NaturalTransformation.component ℶ _ | |
| ≈⟨ Setoid.sym (Mor′ _ _) (∘-∘ _ _ _) ⟩ | |
| Functor.map H f ∘ (NaturalTransformation.component ℵ _ ∘ NaturalTransformation.component ℶ _) | |
| ∎ | |
| }; | |
| ι = λ F → record { | |
| component = λ α → ι 𝒯 (Functor.⟨_⟩ F α); | |
| natural = λ f → begin⟨ Mor′ _ _ ⟩ | |
| ι 𝒯 (Functor.⟨_⟩ F _) ∘ Functor.map F f | |
| ≈⟨ ι-∘ _ ⟩ | |
| Functor.map F f | |
| ≈⟨ Setoid.sym (Mor′ _ _) (∘-ι _) ⟩ | |
| Functor.map F f ∘ ι 𝒯 (Functor.⟨_⟩ F _) | |
| ∎ | |
| }; | |
| ι-∘ = λ ℵ α → ι-∘ _; | |
| ∘-ι = λ ℵ α → ∘-ι _; | |
| ∘-∘ = λ ℵ ℶ ℷ α → ∘-∘ _ _ _; | |
| ∘-cong = λ p q α → ∘-cong (p α) (q α) | |
| } | |
| where | |
| open Category 𝒯 using (_∘_; _≈_; Mor′; ι-∘; ∘-ι; ∘-∘; ∘-cong) | |
| open import Relation.Binary.SetoidReasoning | |
| Cat : (o a ℓ : Level) → Category _ _ _ | |
| Cat o a ℓ = record { | |
| Ob = Category o a ℓ; | |
| Mor′ = λ 𝒞 𝒟 → IsomorphismSetoid [ 𝒞 , 𝒟 ]; | |
| _∘_ = λ {𝒞} {𝒟} {ℰ} F G → record { | |
| ⟨_⟩ = λ α → Functor.⟨_⟩ F (Functor.⟨_⟩ G α); | |
| map = λ f → Functor.map F (Functor.map G f); | |
| map-ι = λ α → Setoid.trans (Category.Mor′ ℰ _ _) (Functor.map-≈ F (Functor.map-ι G α)) (Functor.map-ι F _); | |
| map-∘ = λ f g → Setoid.trans (Category.Mor′ ℰ _ _) (Functor.map-≈ F (Functor.map-∘ G f g)) (Functor.map-∘ F _ _); | |
| map-≈ = λ p → Functor.map-≈ F (Functor.map-≈ G p) | |
| }; | |
| ι = λ 𝒞 → record { | |
| ⟨_⟩ = λ α → α; | |
| map = λ f → f; | |
| map-ι = λ α → Setoid.refl (Category.Mor′ 𝒞 _ _); | |
| map-∘ = λ f g → Setoid.refl (Category.Mor′ 𝒞 _ _); | |
| map-≈ = λ p → p | |
| }; | |
| ι-∘ = λ {𝒞} {𝒟} F → let open Category 𝒟 using (_∘_) in record { | |
| iso = record { | |
| component = λ α → ι 𝒟 _; | |
| natural = λ f → begin⟨ Category.Mor′ 𝒟 _ _ ⟩ | |
| ι 𝒟 _ ∘ Functor.map F f | |
| ≈⟨ Category.ι-∘ 𝒟 _ ⟩ | |
| Functor.map F f | |
| ≈⟨ Setoid.sym (Category.Mor′ 𝒟 _ _) (Category.∘-ι 𝒟 _) ⟩ | |
| Functor.map F f ∘ ι 𝒟 _ | |
| ∎ | |
| }; | |
| isIsomorphism = record { | |
| inverse = record { | |
| component = λ α → ι 𝒟 _; | |
| natural = λ f → begin⟨ Category.Mor′ 𝒟 _ _ ⟩ | |
| ι 𝒟 _ ∘ Functor.map F f | |
| ≈⟨ Category.ι-∘ 𝒟 _ ⟩ | |
| Functor.map F f | |
| ≈⟨ Setoid.sym (Category.Mor′ 𝒟 _ _) (Category.∘-ι 𝒟 _) ⟩ | |
| Functor.map F f ∘ ι 𝒟 _ | |
| ∎ | |
| }; | |
| section = λ α → Category.ι-∘ 𝒟 _; | |
| retract = λ α → Category.∘-ι 𝒟 _ | |
| } | |
| }; | |
| ∘-ι = λ {𝒞} {𝒟} F → let open Category 𝒟 using (_∘_) in record { | |
| iso = record { | |
| component = λ α → ι 𝒟 _; | |
| natural = λ f → begin⟨ Category.Mor′ 𝒟 _ _ ⟩ | |
| ι 𝒟 _ ∘ Functor.map F f | |
| ≈⟨ Category.ι-∘ 𝒟 _ ⟩ | |
| Functor.map F f | |
| ≈⟨ Setoid.sym (Category.Mor′ 𝒟 _ _) (Category.∘-ι 𝒟 _) ⟩ | |
| Functor.map F f ∘ ι 𝒟 _ | |
| ∎ | |
| }; | |
| isIsomorphism = record { | |
| inverse = record { | |
| component = λ α → ι 𝒟 _; | |
| natural = λ f → begin⟨ Category.Mor′ 𝒟 _ _ ⟩ | |
| ι 𝒟 _ ∘ Functor.map F f | |
| ≈⟨ Category.ι-∘ 𝒟 _ ⟩ | |
| Functor.map F f | |
| ≈⟨ Setoid.sym (Category.Mor′ 𝒟 _ _) (Category.∘-ι 𝒟 _)⟩ | |
| Functor.map F f ∘ ι 𝒟 _ | |
| ∎ | |
| }; | |
| section = λ α → Category.ι-∘ 𝒟 _; | |
| retract = λ α → Category.∘-ι 𝒟 _ | |
| } | |
| }; | |
| ∘-∘ = λ {𝒞} {𝒟} {ℰ} {ℱ} F G H → let open Category ℱ using (_∘_) in record { | |
| iso = record { | |
| component = λ α → ι ℱ _; | |
| natural = λ f → begin⟨ Category.Mor′ ℱ _ _ ⟩ | |
| ι ℱ _ ∘ Functor.map F (Functor.map G (Functor.map H f)) | |
| ≈⟨ Category.ι-∘ ℱ _ ⟩ | |
| Functor.map F (Functor.map G (Functor.map H f)) | |
| ≈⟨ Setoid.sym (Category.Mor′ ℱ _ _) (Category.∘-ι ℱ _) ⟩ | |
| Functor.map F (Functor.map G (Functor.map H f)) ∘ ι ℱ _ | |
| ∎ | |
| }; | |
| isIsomorphism = record { | |
| inverse = record { | |
| component = λ α → ι ℱ _; | |
| natural = λ f → begin⟨ Category.Mor′ ℱ _ _ ⟩ | |
| ι ℱ _ ∘ Functor.map F (Functor.map G (Functor.map H f)) | |
| ≈⟨ Category.ι-∘ ℱ _ ⟩ | |
| Functor.map F (Functor.map G (Functor.map H f)) | |
| ≈⟨ Setoid.sym (Category.Mor′ ℱ _ _) (Category.∘-ι ℱ _) ⟩ | |
| Functor.map F (Functor.map G (Functor.map H f)) ∘ ι ℱ _ | |
| ∎ | |
| }; | |
| section = λ α → Category.ι-∘ ℱ _; | |
| retract = λ α → Category.∘-ι ℱ _ | |
| } | |
| }; | |
| ∘-cong = λ {𝒞} {𝒟} {ℰ} {F} {F′} {G} {G′} p q → | |
| let | |
| open Category 𝒟 using () renaming (_∘_ to _∙_) | |
| open Category ℰ using (_∘_) | |
| in record { | |
| iso = record { | |
| component = λ α → Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) α) ∘ NaturalTransformation.component (Isomorphism.iso p) _; | |
| natural = λ f → begin⟨ Category.Mor′ ℰ _ _ ⟩ | |
| (Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _) ∘ NaturalTransformation.component (Isomorphism.iso p) _) ∘ Functor.map F (Functor.map G f) | |
| ≈⟨ Setoid.sym (Category.Mor′ ℰ _ _) (Category.∘-∘ ℰ _ _ _) ⟩ | |
| Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _) ∘ (NaturalTransformation.component (Isomorphism.iso p) _ ∘ Functor.map F (Functor.map G f)) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (NaturalTransformation.natural (Isomorphism.iso p) _) ⟩ | |
| Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _) ∘ (Functor.map F′ (Functor.map G f) ∘ NaturalTransformation.component (Isomorphism.iso p) _) | |
| ≈⟨ Category.∘-∘ ℰ _ _ _ ⟩ | |
| (Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _ ) ∘ Functor.map F′ (Functor.map G f)) ∘ NaturalTransformation.component (Isomorphism.iso p) _ | |
| ≈⟨ Category.∘-cong ℰ (Setoid.sym (Category.Mor′ ℰ _ _) (Functor.map-∘ F′ _ _)) (Setoid.refl (Category.Mor′ ℰ _ _)) ⟩ | |
| (Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _ ∙ Functor.map G f)) ∘ NaturalTransformation.component (Isomorphism.iso p) _ | |
| ≈⟨ Category.∘-cong ℰ (Functor.map-≈ F′ (NaturalTransformation.natural (Isomorphism.iso q) _)) (Setoid.refl (Category.Mor′ ℰ _ _)) ⟩ | |
| (Functor.map F′ (Functor.map G′ f ∙ NaturalTransformation.component (Isomorphism.iso q) _)) ∘ NaturalTransformation.component (Isomorphism.iso p) _ | |
| ≈⟨ Category.∘-cong ℰ (Functor.map-∘ F′ _ _) (Setoid.refl (Category.Mor′ ℰ _ _)) ⟩ | |
| (Functor.map F′ (Functor.map G′ f) ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _)) ∘ NaturalTransformation.component (Isomorphism.iso p) _ | |
| ≈⟨ Setoid.sym (Category.Mor′ ℰ _ _) (Category.∘-∘ ℰ _ _ _) ⟩ | |
| Functor.map F′ (Functor.map G′ f) ∘ (Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _) ∘ NaturalTransformation.component (Isomorphism.iso p) _) | |
| ∎ | |
| }; | |
| isIsomorphism = record { | |
| inverse = record { | |
| component = λ α → NaturalTransformation.component (Isomorphism.inverse p) _ ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _); | |
| natural = λ f → begin⟨ Category.Mor′ ℰ _ _ ⟩ | |
| (NaturalTransformation.component (Isomorphism.inverse p) _ ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _)) ∘ Functor.map F′ (Functor.map G′ f) | |
| ≈⟨ Setoid.sym (Category.Mor′ ℰ _ _) (Category.∘-∘ ℰ _ _ _) ⟩ | |
| NaturalTransformation.component (Isomorphism.inverse p) _ ∘ (Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _) ∘ Functor.map F′ (Functor.map G′ f)) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (Setoid.sym (Category.Mor′ ℰ _ _) (Functor.map-∘ F′ _ _)) ⟩ | |
| NaturalTransformation.component (Isomorphism.inverse p) _ ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _ ∙ Functor.map G′ f) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (Functor.map-≈ F′ (NaturalTransformation.natural (Isomorphism.inverse q) _)) ⟩ | |
| NaturalTransformation.component (Isomorphism.inverse p) _ ∘ Functor.map F′ (Functor.map G f ∙ NaturalTransformation.component (Isomorphism.inverse q) _) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (Functor.map-∘ F′ _ _) ⟩ | |
| NaturalTransformation.component (Isomorphism.inverse p) _ ∘ (Functor.map F′ (Functor.map G f) ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _)) | |
| ≈⟨ Category.∘-∘ ℰ _ _ _ ⟩ | |
| (NaturalTransformation.component (Isomorphism.inverse p) _ ∘ Functor.map F′ (Functor.map G f)) ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _) | |
| ≈⟨ Category.∘-cong ℰ (NaturalTransformation.natural (Isomorphism.inverse p) _) (Setoid.refl (Category.Mor′ ℰ _ _)) ⟩ | |
| (Functor.map F (Functor.map G f) ∘ NaturalTransformation.component (Isomorphism.inverse p) _) ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _) | |
| ≈⟨ Setoid.sym (Category.Mor′ ℰ _ _) (Category.∘-∘ ℰ _ _ _) ⟩ | |
| Functor.map F (Functor.map G f) ∘ (NaturalTransformation.component (Isomorphism.inverse p) _ ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _)) | |
| ∎ | |
| }; | |
| section = λ α → begin⟨ Category.Mor′ ℰ _ _ ⟩ | |
| (NaturalTransformation.component (Isomorphism.inverse p) _ ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _)) ∘ (Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _) ∘ NaturalTransformation.component (Isomorphism.iso p) _) | |
| ≈⟨ Setoid.sym (Category.Mor′ ℰ _ _) (Category.∘-∘ ℰ _ _ _) ⟩ | |
| NaturalTransformation.component (Isomorphism.inverse p) _ ∘ (Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _) ∘ (Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _) ∘ NaturalTransformation.component (Isomorphism.iso p) _)) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (Category.∘-∘ ℰ _ _ _) ⟩ | |
| NaturalTransformation.component (Isomorphism.inverse p) _ ∘ ((Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _) ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _)) ∘ NaturalTransformation.component (Isomorphism.iso p) _) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (Category.∘-cong ℰ (Setoid.sym (Category.Mor′ ℰ _ _) (Functor.map-∘ F′ _ _)) (Setoid.refl (Category.Mor′ ℰ _ _))) ⟩ | |
| NaturalTransformation.component (Isomorphism.inverse p) _ ∘ (Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _ ∙ NaturalTransformation.component (Isomorphism.iso q) _) ∘ NaturalTransformation.component (Isomorphism.iso p) _) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (Category.∘-cong ℰ (Functor.map-≈ F′ (Isomorphism.section q _)) (Setoid.refl (Category.Mor′ ℰ _ _))) ⟩ | |
| NaturalTransformation.component (Isomorphism.inverse p) _ ∘ (Functor.map F′ (ι 𝒟 _) ∘ NaturalTransformation.component (Isomorphism.iso p) _) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (Category.∘-cong ℰ (Functor.map-ι F′ _) (Setoid.refl (Category.Mor′ ℰ _ _))) ⟩ | |
| NaturalTransformation.component (Isomorphism.inverse p) _ ∘ (ι ℰ _ ∘ NaturalTransformation.component (Isomorphism.iso p) _) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (Category.ι-∘ ℰ _) ⟩ | |
| NaturalTransformation.component (Isomorphism.inverse p) _ ∘ NaturalTransformation.component (Isomorphism.iso p) _ | |
| ≈⟨ Isomorphism.section p _ ⟩ | |
| ι ℰ _ | |
| ∎; | |
| retract = λ α → begin⟨ Category.Mor′ ℰ _ _ ⟩ | |
| (Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _) ∘ NaturalTransformation.component (Isomorphism.iso p) _) ∘ (NaturalTransformation.component (Isomorphism.inverse p) _ ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _)) | |
| ≈⟨ Setoid.sym (Category.Mor′ ℰ _ _) (Category.∘-∘ ℰ _ _ _) ⟩ | |
| Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _) ∘ (NaturalTransformation.component (Isomorphism.iso p) _ ∘ (NaturalTransformation.component (Isomorphism.inverse p) _ ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _))) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (Category.∘-∘ ℰ _ _ _) ⟩ | |
| Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _) ∘ ((NaturalTransformation.component (Isomorphism.iso p) _ ∘ NaturalTransformation.component (Isomorphism.inverse p) _) ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _)) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (Category.∘-cong ℰ (Isomorphism.retract p _) (Setoid.refl (Category.Mor′ ℰ _ _))) ⟩ | |
| Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _) ∘ (ι ℰ _ ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _)) | |
| ≈⟨ Category.∘-cong ℰ (Setoid.refl (Category.Mor′ ℰ _ _)) (Category.ι-∘ ℰ _) ⟩ | |
| Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _) ∘ Functor.map F′ (NaturalTransformation.component (Isomorphism.inverse q) _) | |
| ≈⟨ Setoid.sym (Category.Mor′ ℰ _ _) (Functor.map-∘ F′ _ _) ⟩ | |
| Functor.map F′ (NaturalTransformation.component (Isomorphism.iso q) _ ∙ NaturalTransformation.component (Isomorphism.inverse q) _) | |
| ≈⟨ Functor.map-≈ F′ (Isomorphism.retract q _) ⟩ | |
| Functor.map F′ (ι 𝒟 _) | |
| ≈⟨ Functor.map-ι F′ _ ⟩ | |
| ι ℰ _ | |
| ∎ | |
| } | |
| } | |
| } | |
| where | |
| open import Relation.Binary.SetoidReasoning |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment