-
Notifications
You must be signed in to change notification settings - Fork 69
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #452 from agda/limits-refactor
Factor (co)end (co)limits into their own modules
- Loading branch information
Showing
5 changed files
with
192 additions
and
151 deletions.
There are no files selected for viewing
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,55 @@ | ||
| {-# OPTIONS --without-K --safe #-} | ||
|
|
||
| module Categories.Diagram.Coend.Colimit where | ||
|
|
||
| open import Categories.Category.Equivalence as SE using (StrongEquivalence) | ||
| open import Categories.Category.Equivalence.Preserves using (pres-Initial) | ||
| open import Categories.Category.Core using (Category) | ||
| open import Categories.Functor using (Functor) | ||
| open import Categories.Functor.Bifunctor using (Bifunctor) | ||
| open import Categories.Functor.Instance.Twisted using (Twist′) | ||
| open import Categories.Diagram.Coend using (Coend) | ||
| open import Categories.Diagram.Coend.Properties using (Coend⇒Initial; Initial⇒Coend) | ||
| open import Categories.Diagram.Colimit using (Colimit) | ||
| open import Categories.Diagram.Cowedge using (module Cowedge-Morphism) | ||
| open import Categories.Diagram.Cowedge.Properties using (CoconesTwist≅Cowedges) | ||
|
|
||
| import Categories.Category.Construction.Cowedges as Cowedges | ||
| import Categories.Object.Initial as Initial | ||
| import Categories.Morphism as M | ||
|
|
||
| module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} | ||
| (F : Bifunctor (Category.op C) C D) where | ||
| private | ||
| Eq = CoconesTwist≅Cowedges F | ||
| module O = M D | ||
| open M (Cowedges.Cowedges F) | ||
| open Functor | ||
|
|
||
| open StrongEquivalence Eq renaming (F to F⇒) | ||
|
|
||
| Coend-yields-colimit : Coend F → Colimit (Twist′ C D F) | ||
| Coend-yields-colimit ef = record { initial = pres-Initial (SE.sym Eq) (Coend⇒Initial F ef) } | ||
|
|
||
| colimit-yields-Coend : Colimit (Twist′ C D F) → Coend F | ||
| colimit-yields-Coend l = Initial⇒Coend F (pres-Initial Eq (Colimit.initial l)) | ||
|
|
||
| -- Coends and Colimits are equivalent, in the category Cowedge F | ||
| Coend-as-Colimit : (coend : Coend F) → (cl : Colimit (Twist′ C D F)) → Coend.cowedge coend ≅ F₀ F⇒ (Colimit.initial.⊥ cl) | ||
| Coend-as-Colimit coend cl = Initial.up-to-iso (Cowedges.Cowedges F) (Coend⇒Initial F coend) (pres-Initial Eq initial) | ||
| where | ||
| open Colimit cl | ||
|
|
||
| -- Which then induces that the objects, in D, are also equivalent. | ||
| Coend-as-Colimit-on-Obj : (coend : Coend F) → (cl : Colimit (Twist′ C D F)) → Coend.E coend O.≅ Colimit.coapex cl | ||
| Coend-as-Colimit-on-Obj coend cl = record | ||
| { from = Cowedge-Morphism.u (M._≅_.from X≅Y) | ||
| ; to = Cowedge-Morphism.u (M._≅_.to X≅Y) | ||
| ; iso = record | ||
| { isoˡ = M._≅_.isoˡ X≅Y | ||
| ; isoʳ = M._≅_.isoʳ X≅Y | ||
| } | ||
| } | ||
| where | ||
| X≅Y = Coend-as-Colimit coend cl | ||
| open Category D |
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,115 @@ | ||
| {-# OPTIONS --without-K --safe #-} | ||
|
|
||
| module Categories.Diagram.End.Limit where | ||
|
|
||
| open import Level | ||
|
|
||
| open import Categories.Category using (Category) | ||
| open import Categories.Category.Construction.TwistedArrow using (Codomain) | ||
| open import Categories.Category.Equivalence as SE using (StrongEquivalence) | ||
| open import Categories.Category.Equivalence.Preserves using (pres-Terminal) | ||
| open import Categories.Diagram.End using () renaming (End to ∫) | ||
| open import Categories.Diagram.End.Properties using (End⇒Terminal; Terminal⇒End; end-η; end-unique; end-identity; end-η-resp-≈; end-η-resp-∘) | ||
| open import Categories.Diagram.Limit using (Limit) | ||
| open import Categories.Diagram.Limit.Properties using (≃-resp-lim) | ||
| open import Categories.Diagram.Wedge using (module Wedge-Morphism) | ||
| open import Categories.Diagram.Wedge.Properties using (ConesTwist≅Wedges) | ||
| open import Categories.Functor using (Functor; _∘F_) | ||
| open import Categories.Functor.Instance.Twisted using (Twist; Twistⁿⁱ) | ||
| open import Categories.Functor.Limits using (Continuous) | ||
| open import Categories.Functor.Bifunctor using (Bifunctor) | ||
| open import Categories.NaturalTransformation using (NaturalTransformation; _∘ᵥ_) renaming (id to idN) | ||
| open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; sym-associator) renaming (_≃_ to _≃ⁱ_) | ||
| open import Categories.Object.Terminal as Terminal | ||
|
|
||
| import Categories.Category.Construction.Wedges as Wedges | ||
| import Categories.Morphism as M | ||
|
|
||
| private | ||
| variable | ||
| o ℓ e : Level | ||
| C D E : Category o ℓ e | ||
|
|
||
| -- The real start of the End Calculus. Maybe need to move such properties elsewhere? | ||
| -- This is an unpacking of the lhs of Eq. (25) of Loregian's book. | ||
| module _ (F : Bifunctor (Category.op C) C D) where | ||
| private | ||
| Eq = ConesTwist≅Wedges F | ||
| module O = M D | ||
| open M (Wedges.Wedges F) | ||
| open Functor | ||
|
|
||
| open StrongEquivalence Eq renaming (F to F⇒; G to F⇐) | ||
|
|
||
| End-yields-limit : ∫ F → Limit (Twist C D F) | ||
| End-yields-limit ef = record { terminal = pres-Terminal (SE.sym Eq) (End⇒Terminal F ef) } | ||
|
|
||
| limit-yields-End : Limit (Twist C D F) → ∫ F | ||
| limit-yields-End l = Terminal⇒End F (pres-Terminal Eq (Limit.terminal l)) | ||
|
|
||
| -- Ends and Limits are equivalent, in the category Wedge F | ||
| End-as-Limit : (end : ∫ F) → (l : Limit (Twist C D F)) → ∫.wedge end ≅ F₀ F⇒ (Limit.terminal.⊤ l) | ||
| End-as-Limit end l = Terminal.up-to-iso (Wedges.Wedges F) (End⇒Terminal F end) (pres-Terminal Eq terminal) | ||
| where | ||
| open Limit l | ||
|
|
||
| -- Which then induces that the objects, in D, are also equivalent. | ||
| End-as-Limit-on-Obj : (end : ∫ F) → (l : Limit (Twist C D F)) → ∫.E end O.≅ Limit.apex l | ||
| End-as-Limit-on-Obj end l = record | ||
| { from = Wedge-Morphism.u (M._≅_.from X≅Y) | ||
| ; to = Wedge-Morphism.u (M._≅_.to X≅Y) | ||
| ; iso = record | ||
| { isoˡ = M._≅_.isoˡ X≅Y | ||
| ; isoʳ = M._≅_.isoʳ X≅Y | ||
| } | ||
| } | ||
| where | ||
| X≅Y = End-as-Limit end l | ||
| open Category D | ||
|
|
||
| -- A stronger form of Categories.Diagram.End.Properties.end-resp-≅ | ||
| module _ {F G : Bifunctor (Category.op C) C D} (F≃G : F ≃ⁱ G) where | ||
| ≅-yields-end : ∫ F → ∫ G | ||
| ≅-yields-end ef = limit-yields-End G (≃-resp-lim (Twistⁿⁱ C D F≃G) (End-yields-limit F ef)) | ||
|
|
||
| -- continuous functors preserve ends | ||
| module _ {C : Category o ℓ e} | ||
| (J : Bifunctor (Category.op C) C D) (F : Functor D E) | ||
| {cont : Continuous (o ⊔ ℓ) (ℓ ⊔ e) e F} where | ||
| open Category E | ||
| open M E | ||
| open _≅_ | ||
| open Iso | ||
| open ∫ hiding (E) | ||
| private | ||
| module F = Functor F | ||
| module J = Bifunctor J | ||
| module E = Category E | ||
| -- i don't have a better name for this | ||
| -- the converse follows only if J reflects limits | ||
| open import Categories.Diagram.Cone.Properties | ||
| open import Categories.Diagram.Limit.Properties | ||
|
|
||
| module _ (ej : ∫ J) where | ||
| private | ||
| module ej = ∫ ej | ||
| j-limit : Limit (Twist C D J) | ||
| j-limit = End-yields-limit J ej | ||
| --new-limit | ||
| f-limit : Limit (F ∘F (J ∘F Codomain C)) | ||
| f-limit .Limit.terminal = record | ||
| { ⊤ = F-map-Coneˡ F (Limit.limit j-limit) | ||
| ; ⊤-is-terminal = cont j-limit | ||
| } | ||
| -- for this we merely need to transport across the associator | ||
| f-limit′ : Limit (Twist C E (F ∘F J)) | ||
| f-limit′ = ≃-resp-lim (sym-associator (Codomain C) J F) f-limit | ||
|
|
||
| -- really we want IsEnd `F.₀ (∫.E ej)` (F ∘F J) | ||
| contF-as-end : ∫ (F ∘F J) | ||
| contF-as-end = limit-yields-End (F ∘F J) f-limit′ | ||
| _ : F.₀ (∫.E ej) ≅ (∫.E contF-as-end) | ||
| _ = ≅.refl | ||
|
|
||
| Continuous-pres-End : {ej : ∫ J} {ef : ∫ (F ∘F J)} → F.₀ (∫.E ej) ≅ ∫.E ef | ||
| Continuous-pres-End {ej} {ef} = end-unique (contF-as-end ej) ef |
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
Oops, something went wrong.