From 36fab80b4d0c3314651b50b9e33217d19c2e7745 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 1 Aug 2024 20:40:18 -0500 Subject: [PATCH 1/5] Move IsPullback unique field to bottom --- .../Category/CartesianClosed/Locally.agda | 2 +- .../Category/Construction/Elements.agda | 4 +- .../Extensive/Properties/Distributive.agda | 10 ++--- .../Instance/Properties/Setoids/Exact.agda | 4 +- .../Properties/Setoids/Extensive.agda | 2 +- .../Properties/Setoids/Limits/Canonical.agda | 2 +- src/Categories/Category/Slice/Properties.agda | 2 +- src/Categories/Diagram/Duality.agda | 2 +- src/Categories/Diagram/Pullback.agda | 37 +++++++++---------- src/Categories/Diagram/Pullback/Limit.agda | 2 +- .../Diagram/Pullback/Properties.agda | 6 +-- src/Categories/Object/Kernel/Properties.agda | 4 +- 12 files changed, 38 insertions(+), 39 deletions(-) diff --git a/src/Categories/Category/CartesianClosed/Locally.agda b/src/Categories/Category/CartesianClosed/Locally.agda index a36f0d368..72c887df0 100644 --- a/src/Categories/Category/CartesianClosed/Locally.agda +++ b/src/Categories/Category/CartesianClosed/Locally.agda @@ -44,9 +44,9 @@ record Locally : Set (levelOfTerm C) where ; isPullback = record { commute = p.commute ; universal = λ {Z} {h i} eq → slicearr {h = p.universal eq} (pullʳ p.p₁∘universal≈h₁ ○ Slice⇒.△ h) - ; unique = λ eq₁ eq₂ → p.unique eq₁ eq₂ ; p₁∘universal≈h₁ = p.p₁∘universal≈h₁ ; p₂∘universal≈h₂ = p.p₂∘universal≈h₂ + ; unique = λ eq₁ eq₂ → p.unique eq₁ eq₂ } } where open HomReasoning diff --git a/src/Categories/Category/Construction/Elements.agda b/src/Categories/Category/Construction/Elements.agda index 67820da8b..fccc645a7 100644 --- a/src/Categories/Category/Construction/Elements.agda +++ b/src/Categories/Category/Construction/Elements.agda @@ -140,13 +140,13 @@ module Alternate-Pullback {C : Category (suc o) o o} (F : Functor C (Sets o)) wh ; homomorphism = Functor.homomorphism h₁ ; F-resp-≈ = Functor.F-resp-≈ h₁ } + ; p₁∘universal≈h₁ = {!!} + ; p₂∘universal≈h₂ = {!!} ; unique = λ πˡ∘i≃h₁ map∘i≃h₂ → record { F⇒G = record { η = λ X → {!!} ; commute = {!!} } ; F⇐G = record { η = {!!} ; commute = {!!} } ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} } } - ; p₁∘universal≈h₁ = {!!} - ; p₂∘universal≈h₂ = {!!} } where open NaturalTransformation diff --git a/src/Categories/Category/Extensive/Properties/Distributive.agda b/src/Categories/Category/Extensive/Properties/Distributive.agda index 4653ff081..a07bb4309 100644 --- a/src/Categories/Category/Extensive/Properties/Distributive.agda +++ b/src/Categories/Category/Extensive/Properties/Distributive.agda @@ -56,11 +56,6 @@ module Categories.Category.Extensive.Properties.Distributive {o ℓ e} (𝒞 : C pb g = record { p₁ = id ⁂ g ; p₂ = π₂ ; isPullback = record { commute = π₂∘⁂ ; universal = λ {_} {h₁} {h₂} H → ⟨ π₁ ∘ h₁ , h₂ ⟩ - ; unique = λ {X} {h₁} {h₂} {i} {eq} H1 H2 → sym (BP.unique (begin - π₁ ∘ i ≈˘⟨ identityˡ ⟩∘⟨refl ⟩ - ((id ∘ π₁) ∘ i) ≈˘⟨ pullˡ π₁∘⁂ ⟩ - (π₁ ∘ (id ⁂ g) ∘ i) ≈⟨ refl⟩∘⟨ H1 ⟩ - π₁ ∘ h₁ ∎) H2) ; p₁∘universal≈h₁ = λ {X} {h₁} {h₂} {eq} → begin (id ⁂ g) ∘ ⟨ π₁ ∘ h₁ , h₂ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩ ⟨ id ∘ π₁ ∘ h₁ , g ∘ h₂ ⟩ ≈⟨ ⟨⟩-congʳ identityˡ ⟩ @@ -68,6 +63,11 @@ module Categories.Category.Extensive.Properties.Distributive {o ℓ e} (𝒞 : C ⟨ π₁ ∘ h₁ , π₂ ∘ h₁ ⟩ ≈⟨ g-η ⟩ h₁ ∎ ; p₂∘universal≈h₂ = project₂ + ; unique = λ {X} {h₁} {h₂} {i} {eq} H1 H2 → sym (BP.unique (begin + π₁ ∘ i ≈˘⟨ identityˡ ⟩∘⟨refl ⟩ + ((id ∘ π₁) ∘ i) ≈˘⟨ pullˡ π₁∘⁂ ⟩ + (π₁ ∘ (id ⁂ g) ∘ i) ≈⟨ refl⟩∘⟨ H1 ⟩ + π₁ ∘ h₁ ∎) H2) } } -- by the diagram we get the canonical distributivity (iso-)morphism diff --git a/src/Categories/Category/Instance/Properties/Setoids/Exact.agda b/src/Categories/Category/Instance/Properties/Setoids/Exact.agda index f9d5a7dc8..365b9db48 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Exact.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Exact.agda @@ -282,12 +282,12 @@ module _ ℓ where ; effective = λ {X} E → record { commute = eqn _ (refl X) (refl X) ; universal = λ { {Z}{h₁}{h₂} → universal E h₁ h₂ } + ; p₁∘universal≈h₁ = λ { {eq = eq} → x₁≈ eq} + ; p₂∘universal≈h₂ = λ { {eq = eq} → ≈x₂ eq} ; unique = λ {Z}{h₁}{h₂}{u}{eq} eq₁ eq₂ {x} → Relation.relation (R E) u (universal E h₁ h₂ eq) λ { zero {x} → trans X eq₁ (sym X (x₁≈ eq)) ; (nzero _) {x} → trans X eq₂ (sym X (≈x₂ eq)) } - ; p₁∘universal≈h₁ = λ { {eq = eq} → x₁≈ eq} - ; p₂∘universal≈h₂ = λ { {eq = eq} → ≈x₂ eq} } } where diff --git a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda b/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda index b4f21707c..b6eb89ae9 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda @@ -46,9 +46,9 @@ Setoids-Extensive ℓ = record { to = λ z → conflict A B (eq {z}) ; cong = λ {x} _ → conflict A B (eq {x}) } - ; unique = λ {_} {_} {_} {_} {eq} _ _ {x} → conflict A B (eq {x}) ; p₁∘universal≈h₁ = λ {_ _ _ eq x} → conflict A B (eq {x}) ; p₂∘universal≈h₂ = λ {_ _ _ eq y} → conflict A B (eq {y}) + ; unique = λ {_} {_} {_} {_} {eq} _ _ {x} → conflict A B (eq {x}) } } where diff --git a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda index 381eb039f..e350220e1 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda @@ -58,9 +58,9 @@ pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record } ; cong = < cong h₁ , cong h₂ > } - ; unique = λ eq₁ eq₂ → eq₁ , eq₂ ; p₁∘universal≈h₁ = X.refl ; p₂∘universal≈h₂ = Y.refl + ; unique = λ eq₁ eq₂ → eq₁ , eq₂ } } where diff --git a/src/Categories/Category/Slice/Properties.agda b/src/Categories/Category/Slice/Properties.agda index e3e2a3183..eac35e79c 100644 --- a/src/Categories/Category/Slice/Properties.agda +++ b/src/Categories/Category/Slice/Properties.agda @@ -33,9 +33,9 @@ module _ {A : C.Obj} where ; isPullback = record { commute = △ π₁ ○ ⟺ (△ π₂) ; universal = λ eq → h ⟨ slicearr eq , slicearr refl ⟩ - ; unique = λ {_ _ _ _ eq} eq′ eq″ → ⟺ (unique {h = slicearr (pushˡ (⟺ (△ π₁)) ○ C.∘-resp-≈ʳ eq′ ○ eq)} eq′ eq″) ; p₁∘universal≈h₁ = project₁ ; p₂∘universal≈h₂ = project₂ + ; unique = λ {_ _ _ _ eq} eq′ eq″ → ⟺ (unique {h = slicearr (pushˡ (⟺ (△ π₁)) ○ C.∘-resp-≈ʳ eq′ ○ eq)} eq′ eq″) } } where open Product (Slice A) p diff --git a/src/Categories/Diagram/Duality.agda b/src/Categories/Diagram/Duality.agda index f90945272..5fdd4dd5b 100644 --- a/src/Categories/Diagram/Duality.agda +++ b/src/Categories/Diagram/Duality.agda @@ -93,9 +93,9 @@ Pushout⇒coPullback p = record ; isPullback = record { commute = commute ; universal = universal - ; unique = unique ; p₁∘universal≈h₁ = universal∘i₁≈h₁ ; p₂∘universal≈h₂ = universal∘i₂≈h₂ + ; unique = unique } } where open Pushout p diff --git a/src/Categories/Diagram/Pullback.agda b/src/Categories/Diagram/Pullback.agda index d5e3abb3f..358968e78 100644 --- a/src/Categories/Diagram/Pullback.agda +++ b/src/Categories/Diagram/Pullback.agda @@ -24,16 +24,15 @@ private -- Proof that a given square is a pullback record IsPullback {P : Obj} (p₁ : P ⇒ X) (p₂ : P ⇒ Y) (f : X ⇒ Z) (g : Y ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where field - commute : f ∘ p₁ ≈ g ∘ p₂ - universal : ∀ {h₁ : A ⇒ X} {h₂ : A ⇒ Y} → f ∘ h₁ ≈ g ∘ h₂ → A ⇒ P - unique : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} → - p₁ ∘ i ≈ h₁ → p₂ ∘ i ≈ h₂ → - i ≈ universal eq - - p₁∘universal≈h₁ : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} → - p₁ ∘ universal eq ≈ h₁ - p₂∘universal≈h₂ : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} → - p₂ ∘ universal eq ≈ h₂ + commute : f ∘ p₁ ≈ g ∘ p₂ + universal : ∀ {h₁ : A ⇒ X} {h₂ : A ⇒ Y} → f ∘ h₁ ≈ g ∘ h₂ → A ⇒ P + p₁∘universal≈h₁ : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} → + p₁ ∘ universal eq ≈ h₁ + p₂∘universal≈h₂ : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} → + p₂ ∘ universal eq ≈ h₂ + unique : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} → + p₁ ∘ i ≈ h₁ → p₂ ∘ i ≈ h₂ → + i ≈ universal eq unique′ : (eq eq′ : f ∘ h₁ ≈ g ∘ h₂) → universal eq ≈ universal eq′ unique′ eq eq′ = unique p₁∘universal≈h₁ p₂∘universal≈h₂ @@ -95,9 +94,9 @@ swap p = record ; isPullback = record { commute = ⟺ commute ; universal = universal ● ⟺ - ; unique = flip unique ; p₁∘universal≈h₁ = p₂∘universal≈h₂ ; p₂∘universal≈h₂ = p₁∘universal≈h₁ + ; unique = flip unique } } where open Pullback p @@ -109,14 +108,14 @@ glue {h = h} p q = record ; isPullback = record { commute = glue-square p.commute q.commute ; universal = λ eq → q.universal (⟺ (p.p₁∘universal≈h₁ {eq = sym-assoc ○ eq})) + ; p₁∘universal≈h₁ = q.p₁∘universal≈h₁ + ; p₂∘universal≈h₂ = assoc ○ ∘-resp-≈ʳ q.p₂∘universal≈h₂ ○ p.p₂∘universal≈h₂ ; unique = λ {_ h₁ h₂ i} eq eq′ → q.unique eq (p.unique (begin p.p₁ ∘ q.p₂ ∘ i ≈˘⟨ extendʳ q.commute ⟩ h ∘ q.p₁ ∘ i ≈⟨ refl⟩∘⟨ eq ⟩ h ∘ h₁ ∎) (sym-assoc ○ eq′)) - ; p₁∘universal≈h₁ = q.p₁∘universal≈h₁ - ; p₂∘universal≈h₂ = assoc ○ ∘-resp-≈ʳ q.p₂∘universal≈h₂ ○ p.p₂∘universal≈h₂ } } where module p = Pullback p @@ -132,14 +131,14 @@ unglue {f = f} {g = g} {h = h} p q = record (f ∘ h) ∘ h₁ ≈⟨ pullʳ eq ⟩ f ∘ p.p₁ ∘ h₂ ≈⟨ extendʳ p.commute ⟩ g ∘ p.p₂ ∘ h₂ ∎ - ; unique = λ {_ h₁ h₂ i} eq eq′ → q.unique eq $ begin - q.p₂ ∘ i ≈⟨ pushˡ (⟺ p.p₂∘universal≈h₂) ⟩ - p.p₂ ∘ p₂′ ∘ i ≈⟨ refl⟩∘⟨ eq′ ⟩ - p.p₂ ∘ h₂ ∎ ; p₁∘universal≈h₁ = q.p₁∘universal≈h₁ ; p₂∘universal≈h₂ = λ {_ _ _ eq} → p.unique-diagram ((pullˡ p.p₁∘universal≈h₁) ○ pullʳ q.p₁∘universal≈h₁ ○ eq) (pullˡ p.p₂∘universal≈h₂ ○ q.p₂∘universal≈h₂) + ; unique = λ {_ h₁ h₂ i} eq eq′ → q.unique eq $ begin + q.p₂ ∘ i ≈⟨ pushˡ (⟺ p.p₂∘universal≈h₂) ⟩ + p.p₂ ∘ p₂′ ∘ i ≈⟨ refl⟩∘⟨ eq′ ⟩ + p.p₂ ∘ h₂ ∎ } } where module p = Pullback p @@ -159,9 +158,9 @@ Product×Equalizer⇒Pullback {f = f} {g = g} p e = record f ∘ h₁ ≈⟨ eq ⟩ g ∘ h₂ ≈˘⟨ pullʳ project₂ ⟩ (g ∘ π₂) ∘ ⟨ h₁ , h₂ ⟩ ∎ - ; unique = λ eq eq′ → e.unique (p.unique (sym-assoc ○ eq) (sym-assoc ○ eq′)) ; p₁∘universal≈h₁ = pullʳ (⟺ e.universal) ○ project₁ ; p₂∘universal≈h₂ = pullʳ (⟺ e.universal) ○ project₂ + ; unique = λ eq eq′ → e.unique (p.unique (sym-assoc ○ eq) (sym-assoc ○ eq′)) } } where module p = Product p @@ -203,9 +202,9 @@ module _ (p : Pullback f g) where ; isPullback = record { commute = ∘-resp-≈ˡ eq ○ commute ○ ⟺ (∘-resp-≈ˡ eq′) ; universal = λ eq″ → universal (∘-resp-≈ˡ (⟺ eq) ○ eq″ ○ ∘-resp-≈ˡ eq′) - ; unique = unique ; p₁∘universal≈h₁ = p₁∘universal≈h₁ ; p₂∘universal≈h₂ = p₂∘universal≈h₂ + ; unique = unique } } diff --git a/src/Categories/Diagram/Pullback/Limit.agda b/src/Categories/Diagram/Pullback/Limit.agda index b32c87637..eff94b13f 100644 --- a/src/Categories/Diagram/Pullback/Limit.agda +++ b/src/Categories/Diagram/Pullback/Limit.agda @@ -51,9 +51,9 @@ module _ {F : Functor Span.op C} where ; isPullback = record { commute = trans (limit-commute span-arrˡ) (sym (limit-commute span-arrʳ)) ; universal = universal - ; unique = commute′ ; p₁∘universal≈h₁ = commute ; p₂∘universal≈h₂ = commute + ; unique = commute′ } } where open Limit lim diff --git a/src/Categories/Diagram/Pullback/Properties.agda b/src/Categories/Diagram/Pullback/Properties.agda index 6af5d0e80..4973d9d0f 100644 --- a/src/Categories/Diagram/Pullback/Properties.agda +++ b/src/Categories/Diagram/Pullback/Properties.agda @@ -30,9 +30,9 @@ pullback-self-mono : Mono f → IsPullback id id f f pullback-self-mono mono = record { commute = refl ; universal = λ {X} {h₁} {h₂} eq → h₁ - ; unique = λ id∘i≈h₁ _ → ⟺ identityˡ ○ id∘i≈h₁ ; p₁∘universal≈h₁ = identityˡ ; p₂∘universal≈h₂ = λ {X} {h₁} {h₂} {eq} → identityˡ ○ mono h₁ h₂ eq + ; unique = λ id∘i≈h₁ _ → ⟺ identityˡ ○ id∘i≈h₁ } -- pullback from a terminal object is the same as a product @@ -58,9 +58,9 @@ module _ (t : Terminal) where ; isPullback = record { commute = !-unique₂ ; universal = λ {_ f g} _ → ⟨ f , g ⟩ - ; unique = λ eq eq′ → ⟺ (unique eq eq′) ; p₁∘universal≈h₁ = project₁ ; p₂∘universal≈h₂ = project₂ + ; unique = λ eq eq′ → ⟺ (unique eq eq′) } } where open Product p @@ -76,9 +76,9 @@ module _ (p : Pullback f g) where ; isPullback = record { commute = ∘-resp-≈ˡ (⟺ eq) ○ commute ○ ∘-resp-≈ˡ eq′ ; universal = λ eq″ → universal (∘-resp-≈ˡ eq ○ eq″ ○ ∘-resp-≈ˡ (⟺ eq′)) - ; unique = unique ; p₁∘universal≈h₁ = p₁∘universal≈h₁ ; p₂∘universal≈h₂ = p₂∘universal≈h₂ + ; unique = unique } } diff --git a/src/Categories/Object/Kernel/Properties.agda b/src/Categories/Object/Kernel/Properties.agda index 571132d01..92c05c7a4 100644 --- a/src/Categories/Object/Kernel/Properties.agda +++ b/src/Categories/Object/Kernel/Properties.agda @@ -38,11 +38,11 @@ Kernel⇒Pullback {f = f} kernel = record f ∘ h₁ ≈⟨ eq ⟩ ¡ ∘ h₂ ≈˘⟨ refl⟩∘⟨ !-unique h₂ ⟩ zero⇒ ∎ + ; p₁∘universal≈h₁ = ⟺ factors + ; p₂∘universal≈h₂ = !-unique₂ ; unique = λ {C} {h₁} {h₂} {i} k-eq h-eq → unique $ begin h₁ ≈˘⟨ k-eq ⟩ kernel⇒ ∘ i ∎ - ; p₁∘universal≈h₁ = ⟺ factors - ; p₂∘universal≈h₂ = !-unique₂ } } where From 111698a501a84e076c689fa3da886968c6eeb2d1 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 1 Aug 2024 21:03:25 -0500 Subject: [PATCH 2/5] Move Pushout unique field to bottom --- src/Categories/Diagram/Duality.agda | 2 +- src/Categories/Diagram/Pushout.agda | 15 +++++++-------- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/src/Categories/Diagram/Duality.agda b/src/Categories/Diagram/Duality.agda index 5fdd4dd5b..821f3d348 100644 --- a/src/Categories/Diagram/Duality.agda +++ b/src/Categories/Diagram/Duality.agda @@ -80,9 +80,9 @@ coPullback⇒Pushout p = record ; i₂ = p₂ ; commute = commute ; universal = universal - ; unique = unique ; universal∘i₁≈h₁ = p₁∘universal≈h₁ ; universal∘i₂≈h₂ = p₂∘universal≈h₂ + ; unique = unique } where open Pullback p diff --git a/src/Categories/Diagram/Pushout.agda b/src/Categories/Diagram/Pushout.agda index 0efd95bea..f49797608 100644 --- a/src/Categories/Diagram/Pushout.agda +++ b/src/Categories/Diagram/Pushout.agda @@ -25,16 +25,15 @@ record Pushout (f : X ⇒ Y) (g : X ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where i₂ : Z ⇒ Q field - commute : i₁ ∘ f ≈ i₂ ∘ g - universal : {h₁ : Y ⇒ B} {h₂ : Z ⇒ B} → h₁ ∘ f ≈ h₂ ∘ g → Q ⇒ B - unique : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {j : Q ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} → - j ∘ i₁ ≈ h₁ → j ∘ i₂ ≈ h₂ → - j ≈ universal eq - - universal∘i₁≈h₁ : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} → + commute : i₁ ∘ f ≈ i₂ ∘ g + universal : {h₁ : Y ⇒ B} {h₂ : Z ⇒ B} → h₁ ∘ f ≈ h₂ ∘ g → Q ⇒ B + universal∘i₁≈h₁ : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} → universal eq ∘ i₁ ≈ h₁ - universal∘i₂≈h₂ : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} → + universal∘i₂≈h₂ : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} → universal eq ∘ i₂ ≈ h₂ + unique : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {j : Q ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} → + j ∘ i₁ ≈ h₁ → j ∘ i₂ ≈ h₂ → + j ≈ universal eq unique-diagram : h ∘ i₁ ≈ j ∘ i₁ → h ∘ i₂ ≈ j ∘ i₂ → From 09c5304cb43d61f48b88befcf567770279e24c4c Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 6 Aug 2024 13:28:13 -0500 Subject: [PATCH 3/5] Replace unique field with unique-diagram Switched the places of unique and unique-diagram for both pullbacks and pushouts; unique is now derived from unique-diagram. --- .../Category/CartesianClosed/Locally.agda | 4 +- .../Extensive/Properties/Distributive.agda | 12 +-- .../Instance/Properties/Setoids/Exact.agda | 14 ++-- .../Properties/Setoids/Extensive.agda | 6 +- .../Properties/Setoids/Limits/Canonical.agda | 2 +- src/Categories/Category/Slice/Properties.agda | 17 ++++- src/Categories/Diagram/Duality.agda | 4 +- src/Categories/Diagram/Pullback.agda | 59 ++++++++------- src/Categories/Diagram/Pullback/Limit.agda | 74 +++++++++++++------ .../Diagram/Pullback/Properties.agda | 6 +- src/Categories/Diagram/Pushout.agda | 24 +++--- src/Categories/Object/Kernel.agda | 12 +++ src/Categories/Object/Kernel/Properties.agda | 4 +- 13 files changed, 147 insertions(+), 91 deletions(-) diff --git a/src/Categories/Category/CartesianClosed/Locally.agda b/src/Categories/Category/CartesianClosed/Locally.agda index 72c887df0..d5373add5 100644 --- a/src/Categories/Category/CartesianClosed/Locally.agda +++ b/src/Categories/Category/CartesianClosed/Locally.agda @@ -46,7 +46,7 @@ record Locally : Set (levelOfTerm C) where ; universal = λ {Z} {h i} eq → slicearr {h = p.universal eq} (pullʳ p.p₁∘universal≈h₁ ○ Slice⇒.△ h) ; p₁∘universal≈h₁ = p.p₁∘universal≈h₁ ; p₂∘universal≈h₂ = p.p₂∘universal≈h₂ - ; unique = λ eq₁ eq₂ → p.unique eq₁ eq₂ + ; unique-diagram = p.unique-diagram } } where open HomReasoning @@ -57,7 +57,7 @@ record Locally : Set (levelOfTerm C) where module f = Slice⇒ f module g = Slice⇒ g module p = P.Pullback (pullbacks f.h g.h) using (p₁; p₂; commute; universal; - p₁∘universal≈h₁; p₂∘universal≈h₂; unique) + p₁∘universal≈h₁; p₂∘universal≈h₂; unique-diagram) open MR C comm : Y.arr ∘ p.p₂ ≈ X.arr ∘ p.p₁ diff --git a/src/Categories/Category/Extensive/Properties/Distributive.agda b/src/Categories/Category/Extensive/Properties/Distributive.agda index a07bb4309..f5d122295 100644 --- a/src/Categories/Category/Extensive/Properties/Distributive.agda +++ b/src/Categories/Category/Extensive/Properties/Distributive.agda @@ -63,11 +63,13 @@ module Categories.Category.Extensive.Properties.Distributive {o ℓ e} (𝒞 : C ⟨ π₁ ∘ h₁ , π₂ ∘ h₁ ⟩ ≈⟨ g-η ⟩ h₁ ∎ ; p₂∘universal≈h₂ = project₂ - ; unique = λ {X} {h₁} {h₂} {i} {eq} H1 H2 → sym (BP.unique (begin - π₁ ∘ i ≈˘⟨ identityˡ ⟩∘⟨refl ⟩ - ((id ∘ π₁) ∘ i) ≈˘⟨ pullˡ π₁∘⁂ ⟩ - (π₁ ∘ (id ⁂ g) ∘ i) ≈⟨ refl⟩∘⟨ H1 ⟩ - π₁ ∘ h₁ ∎) H2) + ; unique-diagram = λ {X} {h₁} {h₂} eq₁ eq₂ → BP.unique′ (begin + π₁ ∘ h₁ ≈⟨ pushˡ (introˡ refl) ⟩ + id ∘ π₁ ∘ h₁ ≈⟨ extendʳ π₁∘⁂ ⟨ + π₁ ∘ (id ⁂ g) ∘ h₁ ≈⟨ refl⟩∘⟨ eq₁ ⟩ + π₁ ∘ (id ⁂ g) ∘ h₂ ≈⟨ extendʳ π₁∘⁂ ⟩ + id ∘ π₁ ∘ h₂ ≈⟨ pullˡ (elimˡ refl) ⟩ + π₁ ∘ h₂ ∎) eq₂ } } -- by the diagram we get the canonical distributivity (iso-)morphism diff --git a/src/Categories/Category/Instance/Properties/Setoids/Exact.agda b/src/Categories/Category/Instance/Properties/Setoids/Exact.agda index 365b9db48..a1119630d 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Exact.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Exact.agda @@ -280,13 +280,13 @@ module _ ℓ where { regular = Setoids-Regular ; quotient = Quotient-Coequalizer ; effective = λ {X} E → record - { commute = eqn _ (refl X) (refl X) - ; universal = λ { {Z}{h₁}{h₂} → universal E h₁ h₂ } - ; p₁∘universal≈h₁ = λ { {eq = eq} → x₁≈ eq} - ; p₂∘universal≈h₂ = λ { {eq = eq} → ≈x₂ eq} - ; unique = λ {Z}{h₁}{h₂}{u}{eq} eq₁ eq₂ {x} → Relation.relation (R E) u (universal E h₁ h₂ eq) - λ { zero {x} → trans X eq₁ (sym X (x₁≈ eq)) - ; (nzero _) {x} → trans X eq₂ (sym X (≈x₂ eq)) + { commute = eqn _ (refl X) (refl X) + ; universal = λ {Z} {h₁} {h₂} → universal E h₁ h₂ + ; p₁∘universal≈h₁ = λ { {eq = eq} → x₁≈ eq } + ; p₂∘universal≈h₂ = λ { {eq = eq} → ≈x₂ eq } + ; unique-diagram = λ {Z} {h₁} {h₂} eq₁ eq₂ → Relation.relation (R E) h₁ h₂ + λ { zero → eq₁ + ; (nzero _) → eq₂ } } } diff --git a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda b/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda index b6eb89ae9..81713f625 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda @@ -3,6 +3,7 @@ module Categories.Category.Instance.Properties.Setoids.Extensive where open import Level using (Level) +open import Data.Empty renaming (⊥ to ⊥′) open import Data.Product using (_,_) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) open import Data.Sum.Relation.Binary.Pointwise using (inj₁; inj₂; _⊎ₛ_; drop-inj₁; drop-inj₂) @@ -48,7 +49,10 @@ Setoids-Extensive ℓ = record } ; p₁∘universal≈h₁ = λ {_ _ _ eq x} → conflict A B (eq {x}) ; p₂∘universal≈h₂ = λ {_ _ _ eq y} → conflict A B (eq {y}) - ; unique = λ {_} {_} {_} {_} {eq} _ _ {x} → conflict A B (eq {x}) + ; unique-diagram = λ {X} {h} {i} eq₁ eq₂ {x} → + let fromBottom : Level.Lift ℓ ⊥′ → [ ⊥ ][ h ⟨$⟩ x ≈ i ⟨$⟩ x ] + fromBottom = λ () + in fromBottom (h ⟨$⟩ x) } } where diff --git a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda index e350220e1..440bbce4b 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda @@ -60,7 +60,7 @@ pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record } ; p₁∘universal≈h₁ = X.refl ; p₂∘universal≈h₂ = Y.refl - ; unique = λ eq₁ eq₂ → eq₁ , eq₂ + ; unique-diagram = λ eq₁ eq₂ → eq₁ , eq₂ } } where diff --git a/src/Categories/Category/Slice/Properties.agda b/src/Categories/Category/Slice/Properties.agda index eac35e79c..d4810c300 100644 --- a/src/Categories/Category/Slice/Properties.agda +++ b/src/Categories/Category/Slice/Properties.agda @@ -27,7 +27,7 @@ module _ {A : C.Obj} where open C.Equiv product⇒pullback : ∀ {X Y : Obj} → Product (Slice A) X Y → Pullback C (arr X) (arr Y) - product⇒pullback p = record + product⇒pullback {X} p = record { p₁ = h π₁ ; p₂ = h π₂ ; isPullback = record @@ -35,7 +35,20 @@ module _ {A : C.Obj} where ; universal = λ eq → h ⟨ slicearr eq , slicearr refl ⟩ ; p₁∘universal≈h₁ = project₁ ; p₂∘universal≈h₂ = project₂ - ; unique = λ {_ _ _ _ eq} eq′ eq″ → ⟺ (unique {h = slicearr (pushˡ (⟺ (△ π₁)) ○ C.∘-resp-≈ʳ eq′ ○ eq)} eq′ eq″) + ; unique-diagram = λ {D j i} eq₁ eq₂ → + let D′ : SliceObj A + D′ = sliceobj (arr A×B C.∘ i) + arr∘j≈arr∘i : arr A×B C.∘ j C.≈ arr A×B C.∘ i + arr∘j≈arr∘i = begin + arr A×B C.∘ j ≈⟨ pushˡ (⟺ (△ π₁)) ⟩ + arr X C.∘ h π₁ C.∘ j ≈⟨ refl⟩∘⟨ eq₁ ⟩ + arr X C.∘ h π₁ C.∘ i ≈⟨ pullˡ (△ π₁) ⟩ + arr A×B C.∘ i ∎ + j′ : D′ ⇒ A×B + j′ = slicearr {h = j} arr∘j≈arr∘i + i′ : D′ ⇒ A×B + i′ = slicearr {h = i} refl + in unique′ {h = j′} {i = i′} eq₁ eq₂ } } where open Product (Slice A) p diff --git a/src/Categories/Diagram/Duality.agda b/src/Categories/Diagram/Duality.agda index 821f3d348..9cec440e6 100644 --- a/src/Categories/Diagram/Duality.agda +++ b/src/Categories/Diagram/Duality.agda @@ -82,7 +82,7 @@ coPullback⇒Pushout p = record ; universal = universal ; universal∘i₁≈h₁ = p₁∘universal≈h₁ ; universal∘i₂≈h₂ = p₂∘universal≈h₂ - ; unique = unique + ; unique-diagram = unique-diagram } where open Pullback p @@ -95,7 +95,7 @@ Pushout⇒coPullback p = record ; universal = universal ; p₁∘universal≈h₁ = universal∘i₁≈h₁ ; p₂∘universal≈h₂ = universal∘i₂≈h₂ - ; unique = unique + ; unique-diagram = unique-diagram } } where open Pushout p diff --git a/src/Categories/Diagram/Pullback.agda b/src/Categories/Diagram/Pullback.agda index 358968e78..fd01b819e 100644 --- a/src/Categories/Diagram/Pullback.agda +++ b/src/Categories/Diagram/Pullback.agda @@ -30,9 +30,15 @@ record IsPullback {P : Obj} (p₁ : P ⇒ X) (p₂ : P ⇒ Y) (f : X ⇒ Z) (g : p₁ ∘ universal eq ≈ h₁ p₂∘universal≈h₂ : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} → p₂ ∘ universal eq ≈ h₂ - unique : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} → - p₁ ∘ i ≈ h₁ → p₂ ∘ i ≈ h₂ → - i ≈ universal eq + unique-diagram : p₁ ∘ h ≈ p₁ ∘ i → + p₂ ∘ h ≈ p₂ ∘ i → + h ≈ i + + unique : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} → p₁ ∘ i ≈ h₁ → p₂ ∘ i ≈ h₂ → i ≈ universal eq + unique p₁∘i≈h₁ p₂∘i≈h₂ = + unique-diagram + (p₁∘i≈h₁ ○ ⟺ p₁∘universal≈h₁) + (p₂∘i≈h₂ ○ ⟺ p₂∘universal≈h₂) unique′ : (eq eq′ : f ∘ h₁ ≈ g ∘ h₂) → universal eq ≈ universal eq′ unique′ eq eq′ = unique p₁∘universal≈h₁ p₂∘universal≈h₂ @@ -43,16 +49,6 @@ record IsPullback {P : Obj} (p₁ : P ⇒ X) (p₂ : P ⇒ Y) (f : X ⇒ Z) (g : universal-resp-≈ : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} {eq′ : f ∘ i₁ ≈ g ∘ i₂} → h₁ ≈ i₁ → h₂ ≈ i₂ → universal eq ≈ universal eq′ universal-resp-≈ h₁≈i₁ h₂≈i₂ = unique (p₁∘universal≈h₁ ○ h₁≈i₁) (p₂∘universal≈h₂ ○ h₂≈i₂) - unique-diagram : p₁ ∘ h ≈ p₁ ∘ i → - p₂ ∘ h ≈ p₂ ∘ i → - h ≈ i - unique-diagram {h = h} {i = i} eq₁ eq₂ = begin - h ≈⟨ unique eq₁ eq₂ ⟩ - universal eq ≈˘⟨ unique refl refl ⟩ - i ∎ - where eq = extendʳ commute - - -- Pullback of two arrows with a common codomain record Pullback (f : X ⇒ Z) (g : Y ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where field @@ -96,7 +92,7 @@ swap p = record ; universal = universal ● ⟺ ; p₁∘universal≈h₁ = p₂∘universal≈h₂ ; p₂∘universal≈h₂ = p₁∘universal≈h₁ - ; unique = flip unique + ; unique-diagram = flip unique-diagram } } where open Pullback p @@ -106,16 +102,18 @@ glue {h = h} p q = record { p₁ = q.p₁ ; p₂ = p.p₂ ∘ q.p₂ ; isPullback = record - { commute = glue-square p.commute q.commute + { commute = glue-square p.commute q.commute ; universal = λ eq → q.universal (⟺ (p.p₁∘universal≈h₁ {eq = sym-assoc ○ eq})) ; p₁∘universal≈h₁ = q.p₁∘universal≈h₁ ; p₂∘universal≈h₂ = assoc ○ ∘-resp-≈ʳ q.p₂∘universal≈h₂ ○ p.p₂∘universal≈h₂ - ; unique = λ {_ h₁ h₂ i} eq eq′ → - q.unique eq (p.unique (begin - p.p₁ ∘ q.p₂ ∘ i ≈˘⟨ extendʳ q.commute ⟩ - h ∘ q.p₁ ∘ i ≈⟨ refl⟩∘⟨ eq ⟩ - h ∘ h₁ ∎) - (sym-assoc ○ eq′)) + ; unique-diagram = λ {_ j i} eq₁ eq₂ → + let eq′ : p.p₁ ∘ q.p₂ ∘ j ≈ p.p₁ ∘ q.p₂ ∘ i + eq′ = begin + p.p₁ ∘ q.p₂ ∘ j ≈⟨ extendʳ q.commute ⟨ + h ∘ q.p₁ ∘ j ≈⟨ refl⟩∘⟨ eq₁ ⟩ + h ∘ q.p₁ ∘ i ≈⟨ extendʳ q.commute ⟩ + p.p₁ ∘ q.p₂ ∘ i ∎ + in q.unique-diagram eq₁ (p.unique-diagram eq′ (sym-assoc ○ eq₂ ○ assoc)) } } where module p = Pullback p @@ -126,7 +124,7 @@ unglue {f = f} {g = g} {h = h} p q = record { p₁ = q.p₁ ; p₂ = p₂′ ; isPullback = record - { commute = ⟺ p.p₁∘universal≈h₁ + { commute = ⟺ p.p₁∘universal≈h₁ ; universal = λ {_ h₁ h₂} eq → q.universal $ begin (f ∘ h) ∘ h₁ ≈⟨ pullʳ eq ⟩ f ∘ p.p₁ ∘ h₂ ≈⟨ extendʳ p.commute ⟩ @@ -135,10 +133,14 @@ unglue {f = f} {g = g} {h = h} p q = record ; p₂∘universal≈h₂ = λ {_ _ _ eq} → p.unique-diagram ((pullˡ p.p₁∘universal≈h₁) ○ pullʳ q.p₁∘universal≈h₁ ○ eq) (pullˡ p.p₂∘universal≈h₂ ○ q.p₂∘universal≈h₂) - ; unique = λ {_ h₁ h₂ i} eq eq′ → q.unique eq $ begin - q.p₂ ∘ i ≈⟨ pushˡ (⟺ p.p₂∘universal≈h₂) ⟩ - p.p₂ ∘ p₂′ ∘ i ≈⟨ refl⟩∘⟨ eq′ ⟩ - p.p₂ ∘ h₂ ∎ + ; unique-diagram = λ {_ j i} eq₁ eq₂ → + let eq′ : q.p₂ ∘ j ≈ q.p₂ ∘ i +   eq′ = begin + q.p₂ ∘ j ≈⟨ pushˡ (⟺ p.p₂∘universal≈h₂) ⟩ + p.p₂ ∘ p₂′ ∘ j ≈⟨ refl⟩∘⟨ eq₂ ⟩ + p.p₂ ∘ p₂′ ∘ i ≈⟨ pullˡ p.p₂∘universal≈h₂ ⟩ + q.p₂ ∘ i ∎ + in q.unique-diagram eq₁ eq′ } } where module p = Pullback p @@ -160,7 +162,8 @@ Product×Equalizer⇒Pullback {f = f} {g = g} p e = record (g ∘ π₂) ∘ ⟨ h₁ , h₂ ⟩ ∎ ; p₁∘universal≈h₁ = pullʳ (⟺ e.universal) ○ project₁ ; p₂∘universal≈h₂ = pullʳ (⟺ e.universal) ○ project₂ - ; unique = λ eq eq′ → e.unique (p.unique (sym-assoc ○ eq) (sym-assoc ○ eq′)) + ; unique-diagram = λ eq₁ eq₂ → + e.unique-diagram (p.unique′ (sym-assoc ○ eq₁ ○ assoc) (sym-assoc ○ eq₂ ○ assoc)) } } where module p = Product p @@ -204,7 +207,7 @@ module _ (p : Pullback f g) where ; universal = λ eq″ → universal (∘-resp-≈ˡ (⟺ eq) ○ eq″ ○ ∘-resp-≈ˡ eq′) ; p₁∘universal≈h₁ = p₁∘universal≈h₁ ; p₂∘universal≈h₂ = p₂∘universal≈h₂ - ; unique = unique + ; unique-diagram = unique-diagram } } diff --git a/src/Categories/Diagram/Pullback/Limit.agda b/src/Categories/Diagram/Pullback/Limit.agda index eff94b13f..062b1b53d 100644 --- a/src/Categories/Diagram/Pullback/Limit.agda +++ b/src/Categories/Diagram/Pullback/Limit.agda @@ -24,7 +24,7 @@ private open Category C variable X Y Z : Obj - f g h : X ⇒ Y + f g h i : X ⇒ Y open HomReasoning @@ -49,11 +49,11 @@ module _ {F : Functor Span.op C} where { p₁ = proj left ; p₂ = proj right ; isPullback = record - { commute = trans (limit-commute span-arrˡ) (sym (limit-commute span-arrʳ)) + { commute = commute-left ○ ⟺ commute-right ; universal = universal ; p₁∘universal≈h₁ = commute ; p₂∘universal≈h₂ = commute - ; unique = commute′ + ; unique-diagram = unique-diagram } } where open Limit lim @@ -65,29 +65,57 @@ module _ {F : Functor Span.op C} where ; left → f ; right → g } - ; commute = λ { {center} {center} span-id → elimˡ identity - ; {left} {center} span-arrˡ → eq - ; {left} {left} span-id → elimˡ identity - ; {right} {center} span-arrʳ → refl - ; {right} {right} span-id → elimˡ identity - } + ; commute = λ { span-id → elimˡ identity + ; span-arrˡ → eq + ; span-arrʳ → refl + } } } - proj-center : proj center ≈ B⇒W ∘ proj right - proj-center = sym (limit-commute span-arrʳ) - - commute′ : ∀ {eq : A⇒W ∘ f ≈ B⇒W ∘ g} → proj left ∘ h ≈ f → proj right ∘ h ≈ g → h ≈ universal eq - commute′ {f = f} {g = g} {h = h} {eq = eq} eq₁ eq₂ = sym $ terminal.!-unique $ record - { arr = h - ; commute = λ { {center} → begin - proj center ∘ h ≈⟨ pushˡ proj-center ⟩ - B⇒W ∘ proj right ∘ h ≈⟨ refl⟩∘⟨ eq₂ ⟩ - B⇒W ∘ g ∎ - ; {left} → eq₁ - ; {right} → eq₂ - } - } + commute-left : A⇒W ∘ proj left ≈ proj center + commute-left = limit-commute span-arrˡ + + commute-right : B⇒W ∘ proj right ≈ proj center + commute-right = limit-commute span-arrʳ + + unique-diagram : proj left ∘ h ≈ proj left ∘ i → + proj right ∘ h ≈ proj right ∘ i → + h ≈ i + unique-diagram {D} {h} {i} eq₁ eq₂ = terminal.!-unique₂ {f = h-cone} {g = i-cone} + where + D-cone : Cone + D-cone = record + { apex = record + { ψ = λ { center → proj center ∘ h + ; left → proj left ∘ h + ; right → proj right ∘ h + } + ; commute = λ { span-id → elimˡ identity + ; span-arrˡ → pullˡ commute-left + ; span-arrʳ → pullˡ commute-right + } + } + } + h-cone : Cone⇒ D-cone limit + h-cone = record + { arr = h + ; commute = λ { {center} → refl + ; {left} → refl + ; {right} → refl + } + } + i-cone : Cone⇒ D-cone limit + i-cone = record + { arr = i + ; commute = λ { {center} → begin + proj center ∘ i ≈⟨ pullˡ commute-left ⟨ + A⇒W ∘ proj left ∘ i ≈⟨ refl⟩∘⟨ eq₁ ⟨ + A⇒W ∘ proj left ∘ h ≈⟨ pullˡ commute-left ⟩ + proj center ∘ h ∎ + ; {left} → sym eq₁ + ; {right} → sym eq₂ + } + } module _ {fA fB gA : Obj} {f : fA ⇒ fB} {g : gA ⇒ fB} (p : Pullback f g) where open Pullback p diff --git a/src/Categories/Diagram/Pullback/Properties.agda b/src/Categories/Diagram/Pullback/Properties.agda index 4973d9d0f..d72b824b6 100644 --- a/src/Categories/Diagram/Pullback/Properties.agda +++ b/src/Categories/Diagram/Pullback/Properties.agda @@ -32,7 +32,7 @@ pullback-self-mono mono = record ; universal = λ {X} {h₁} {h₂} eq → h₁ ; p₁∘universal≈h₁ = identityˡ ; p₂∘universal≈h₂ = λ {X} {h₁} {h₂} {eq} → identityˡ ○ mono h₁ h₂ eq - ; unique = λ id∘i≈h₁ _ → ⟺ identityˡ ○ id∘i≈h₁ + ; unique-diagram = λ id∘h≈id∘i _ → introˡ refl ○ id∘h≈id∘i ○ elimˡ refl } -- pullback from a terminal object is the same as a product @@ -60,7 +60,7 @@ module _ (t : Terminal) where ; universal = λ {_ f g} _ → ⟨ f , g ⟩ ; p₁∘universal≈h₁ = project₁ ; p₂∘universal≈h₂ = project₂ - ; unique = λ eq eq′ → ⟺ (unique eq eq′) + ; unique-diagram = unique′ } } where open Product p @@ -78,7 +78,7 @@ module _ (p : Pullback f g) where ; universal = λ eq″ → universal (∘-resp-≈ˡ eq ○ eq″ ○ ∘-resp-≈ˡ (⟺ eq′)) ; p₁∘universal≈h₁ = p₁∘universal≈h₁ ; p₂∘universal≈h₂ = p₂∘universal≈h₂ - ; unique = unique + ; unique-diagram = unique-diagram } } diff --git a/src/Categories/Diagram/Pushout.agda b/src/Categories/Diagram/Pushout.agda index f49797608..ddb84b378 100644 --- a/src/Categories/Diagram/Pushout.agda +++ b/src/Categories/Diagram/Pushout.agda @@ -28,18 +28,14 @@ record Pushout (f : X ⇒ Y) (g : X ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where commute : i₁ ∘ f ≈ i₂ ∘ g universal : {h₁ : Y ⇒ B} {h₂ : Z ⇒ B} → h₁ ∘ f ≈ h₂ ∘ g → Q ⇒ B universal∘i₁≈h₁ : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} → - universal eq ∘ i₁ ≈ h₁ + universal eq ∘ i₁ ≈ h₁ universal∘i₂≈h₂ : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} → - universal eq ∘ i₂ ≈ h₂ - unique : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {j : Q ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} → - j ∘ i₁ ≈ h₁ → j ∘ i₂ ≈ h₂ → - j ≈ universal eq - - unique-diagram : h ∘ i₁ ≈ j ∘ i₁ → - h ∘ i₂ ≈ j ∘ i₂ → - h ≈ j - unique-diagram {h = h} {j = j} eq₁ eq₂ = begin - h ≈⟨ unique eq₁ eq₂ ⟩ - universal eq ≈˘⟨ unique refl refl ⟩ - j ∎ - where eq = extendˡ commute + universal eq ∘ i₂ ≈ h₂ + unique-diagram : h ∘ i₁ ≈ j ∘ i₁ → h ∘ i₂ ≈ j ∘ i₂ → h ≈ j + + unique : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} → + j ∘ i₁ ≈ h₁ → j ∘ i₂ ≈ h₂ → j ≈ universal eq + unique j∘i₁≈h₁ j∘i₂≈h₂ = + unique-diagram + (j∘i₁≈h₁ ○ ⟺ universal∘i₁≈h₁) + (j∘i₂≈h₂ ○ ⟺ universal∘i₂≈h₂) diff --git a/src/Categories/Object/Kernel.agda b/src/Categories/Object/Kernel.agda index ff0e8d7f3..9f57fdf1d 100644 --- a/src/Categories/Object/Kernel.agda +++ b/src/Categories/Object/Kernel.agda @@ -35,6 +35,18 @@ record IsKernel {A B K} (k : K ⇒ A) (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) wher factors : ∀ {eq : f ∘ h ≈ zero⇒} → h ≈ k ∘ universal eq unique : ∀ {eq : f ∘ h ≈ zero⇒} → h ≈ k ∘ i → i ≈ universal eq + unique-diagram : k ∘ h ≈ k ∘ i → h ≈ i + unique-diagram {_} {h} {i} k∘h≈k∘i = begin + h ≈⟨ unique Equiv.refl ⟩ + universal eq ≈⟨ unique k∘h≈k∘i ⟨ + i ∎ + where + eq : f ∘ k ∘ h ≈ zero⇒ + eq = begin + f ∘ k ∘ h ≈⟨ glue′ commute Equiv.refl ⟩ + zero⇒ ∘ h ≈⟨ zero-∘ʳ h ⟩ + zero⇒ ∎ + universal-resp-≈ : ∀ {eq : f ∘ h ≈ zero⇒} {eq′ : f ∘ i ≈ zero⇒} → h ≈ i → universal eq ≈ universal eq′ universal-resp-≈ h≈i = unique (⟺ h≈i ○ factors) diff --git a/src/Categories/Object/Kernel/Properties.agda b/src/Categories/Object/Kernel/Properties.agda index 92c05c7a4..31564bece 100644 --- a/src/Categories/Object/Kernel/Properties.agda +++ b/src/Categories/Object/Kernel/Properties.agda @@ -40,9 +40,7 @@ Kernel⇒Pullback {f = f} kernel = record zero⇒ ∎ ; p₁∘universal≈h₁ = ⟺ factors ; p₂∘universal≈h₂ = !-unique₂ - ; unique = λ {C} {h₁} {h₂} {i} k-eq h-eq → unique $ begin - h₁ ≈˘⟨ k-eq ⟩ - kernel⇒ ∘ i ∎ + ; unique-diagram = λ k-eq _ → unique-diagram k-eq } } where From de29737ee7544ebe8895e78c5d2c3a654b028367 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 9 Aug 2024 15:33:52 -0500 Subject: [PATCH 4/5] Use level-polymorphic empty type --- .../Category/Instance/Properties/Setoids/Extensive.agda | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda b/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda index 81713f625..4eb4a48b1 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda @@ -3,7 +3,7 @@ module Categories.Category.Instance.Properties.Setoids.Extensive where open import Level using (Level) -open import Data.Empty renaming (⊥ to ⊥′) +open import Data.Empty.Polymorphic using (⊥-elim) open import Data.Product using (_,_) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) open import Data.Sum.Relation.Binary.Pointwise using (inj₁; inj₂; _⊎ₛ_; drop-inj₁; drop-inj₂) @@ -49,10 +49,7 @@ Setoids-Extensive ℓ = record } ; p₁∘universal≈h₁ = λ {_ _ _ eq x} → conflict A B (eq {x}) ; p₂∘universal≈h₂ = λ {_ _ _ eq y} → conflict A B (eq {y}) - ; unique-diagram = λ {X} {h} {i} eq₁ eq₂ {x} → - let fromBottom : Level.Lift ℓ ⊥′ → [ ⊥ ][ h ⟨$⟩ x ≈ i ⟨$⟩ x ] - fromBottom = λ () - in fromBottom (h ⟨$⟩ x) + ; unique-diagram = λ {X} {h} {i} eq₁ eq₂ {x} → ⊥-elim {ℓ} {ℓ} {λ ()} (h ⟨$⟩ x) } } where From f25b6e7151daa8181a9602c779dd1d69d09fccdd Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 9 Aug 2024 15:57:52 -0500 Subject: [PATCH 5/5] Indicate implicit argument in lambda pattern --- .../Category/Instance/Properties/Setoids/Limits/Canonical.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda index 440bbce4b..246ea575f 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda @@ -60,7 +60,7 @@ pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record } ; p₁∘universal≈h₁ = X.refl ; p₂∘universal≈h₂ = Y.refl - ; unique-diagram = λ eq₁ eq₂ → eq₁ , eq₂ + ; unique-diagram = λ eq₁ eq₂ {_} → eq₁ , eq₂ } } where