|
| 1 | +{-# OPTIONS --without-K --safe #-} |
| 2 | + |
| 3 | +module Categories.Diagram.End.Limit where |
| 4 | + |
| 5 | +open import Level |
| 6 | + |
| 7 | +open import Categories.Category using (Category) |
| 8 | +open import Categories.Category.Construction.TwistedArrow using (Codomain) |
| 9 | +open import Categories.Category.Equivalence as SE using (StrongEquivalence) |
| 10 | +open import Categories.Category.Equivalence.Preserves using (pres-Terminal) |
| 11 | +open import Categories.Diagram.End using () renaming (End to ∫) |
| 12 | +open import Categories.Diagram.End.Properties using (End⇒Terminal; Terminal⇒End; end-η; end-unique; end-identity; end-η-resp-≈; end-η-resp-∘) |
| 13 | +open import Categories.Diagram.Limit using (Limit) |
| 14 | +open import Categories.Diagram.Limit.Properties using (≃-resp-lim) |
| 15 | +open import Categories.Diagram.Wedge using (module Wedge-Morphism) |
| 16 | +open import Categories.Diagram.Wedge.Properties using (ConesTwist≅Wedges) |
| 17 | +open import Categories.Functor using (Functor; _∘F_) |
| 18 | +open import Categories.Functor.Instance.Twisted using (Twist; Twistⁿⁱ) |
| 19 | +open import Categories.Functor.Limits using (Continuous) |
| 20 | +open import Categories.Functor.Bifunctor using (Bifunctor) |
| 21 | +open import Categories.NaturalTransformation using (NaturalTransformation; _∘ᵥ_) renaming (id to idN) |
| 22 | +open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; sym-associator) renaming (_≃_ to _≃ⁱ_) |
| 23 | +open import Categories.Object.Terminal as Terminal |
| 24 | + |
| 25 | +import Categories.Category.Construction.Wedges as Wedges |
| 26 | +import Categories.Morphism as M |
| 27 | + |
| 28 | +private |
| 29 | + variable |
| 30 | + o ℓ e : Level |
| 31 | + C D E : Category o ℓ e |
| 32 | + |
| 33 | +-- The real start of the End Calculus. Maybe need to move such properties elsewhere? |
| 34 | +-- This is an unpacking of the lhs of Eq. (25) of Loregian's book. |
| 35 | +module _ (F : Bifunctor (Category.op C) C D) where |
| 36 | + private |
| 37 | + Eq = ConesTwist≅Wedges F |
| 38 | + module O = M D |
| 39 | + open M (Wedges.Wedges F) |
| 40 | + open Functor |
| 41 | + |
| 42 | + open StrongEquivalence Eq renaming (F to F⇒; G to F⇐) |
| 43 | + |
| 44 | + End-yields-limit : ∫ F → Limit (Twist C D F) |
| 45 | + End-yields-limit ef = record { terminal = pres-Terminal (SE.sym Eq) (End⇒Terminal F ef) } |
| 46 | + |
| 47 | + limit-yields-End : Limit (Twist C D F) → ∫ F |
| 48 | + limit-yields-End l = Terminal⇒End F (pres-Terminal Eq (Limit.terminal l)) |
| 49 | + |
| 50 | + -- Ends and Limits are equivalent, in the category Wedge F |
| 51 | + End-as-Limit : (end : ∫ F) → (l : Limit (Twist C D F)) → ∫.wedge end ≅ F₀ F⇒ (Limit.terminal.⊤ l) |
| 52 | + End-as-Limit end l = Terminal.up-to-iso (Wedges.Wedges F) (End⇒Terminal F end) (pres-Terminal Eq terminal) |
| 53 | + where |
| 54 | + open Limit l |
| 55 | + |
| 56 | + -- Which then induces that the objects, in D, are also equivalent. |
| 57 | + End-as-Limit-on-Obj : (end : ∫ F) → (l : Limit (Twist C D F)) → ∫.E end O.≅ Limit.apex l |
| 58 | + End-as-Limit-on-Obj end l = record |
| 59 | + { from = Wedge-Morphism.u (M._≅_.from X≅Y) |
| 60 | + ; to = Wedge-Morphism.u (M._≅_.to X≅Y) |
| 61 | + ; iso = record |
| 62 | + { isoˡ = M._≅_.isoˡ X≅Y |
| 63 | + ; isoʳ = M._≅_.isoʳ X≅Y |
| 64 | + } |
| 65 | + } |
| 66 | + where |
| 67 | + X≅Y = End-as-Limit end l |
| 68 | + open Category D |
| 69 | + |
| 70 | +-- A stronger form of Categories.Diagram.End.Properties.end-resp-≅ |
| 71 | +module _ {F G : Bifunctor (Category.op C) C D} (F≃G : F ≃ⁱ G) where |
| 72 | + ≅-yields-end : ∫ F → ∫ G |
| 73 | + ≅-yields-end ef = limit-yields-End G (≃-resp-lim (Twistⁿⁱ C D F≃G) (End-yields-limit F ef)) |
| 74 | + |
| 75 | +-- continuous functors preserve ends |
| 76 | +module _ {C : Category o ℓ e} |
| 77 | + (J : Bifunctor (Category.op C) C D) (F : Functor D E) |
| 78 | + {cont : Continuous (o ⊔ ℓ) (ℓ ⊔ e) e F} where |
| 79 | + open Category E |
| 80 | + open M E |
| 81 | + open _≅_ |
| 82 | + open Iso |
| 83 | + open ∫ hiding (E) |
| 84 | + private |
| 85 | + module F = Functor F |
| 86 | + module J = Bifunctor J |
| 87 | + module E = Category E |
| 88 | + -- i don't have a better name for this |
| 89 | + -- the converse follows only if J reflects limits |
| 90 | + open import Categories.Diagram.Cone.Properties |
| 91 | + open import Categories.Diagram.Limit.Properties |
| 92 | + |
| 93 | + module _ (ej : ∫ J) where |
| 94 | + private |
| 95 | + module ej = ∫ ej |
| 96 | + j-limit : Limit (Twist C D J) |
| 97 | + j-limit = End-yields-limit J ej |
| 98 | + --new-limit |
| 99 | + f-limit : Limit (F ∘F (J ∘F Codomain C)) |
| 100 | + f-limit .Limit.terminal = record |
| 101 | + { ⊤ = F-map-Coneˡ F (Limit.limit j-limit) |
| 102 | + ; ⊤-is-terminal = cont j-limit |
| 103 | + } |
| 104 | + -- for this we merely need to transport across the associator |
| 105 | + f-limit′ : Limit (Twist C E (F ∘F J)) |
| 106 | + f-limit′ = ≃-resp-lim (sym-associator (Codomain C) J F) f-limit |
| 107 | + |
| 108 | + -- really we want IsEnd `F.₀ (∫.E ej)` (F ∘F J) |
| 109 | + contF-as-end : ∫ (F ∘F J) |
| 110 | + contF-as-end = limit-yields-End (F ∘F J) f-limit′ |
| 111 | + _ : F.₀ (∫.E ej) ≅ (∫.E contF-as-end) |
| 112 | + _ = ≅.refl |
| 113 | + |
| 114 | + Continuous-pres-End : {ej : ∫ J} {ef : ∫ (F ∘F J)} → F.₀ (∫.E ej) ≅ ∫.E ef |
| 115 | + Continuous-pres-End {ej} {ef} = end-unique (contF-as-end ej) ef |
0 commit comments