From b79075733db3d05bd1434c8b14ba1abf5e53a5ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Fri, 17 Jul 2026 11:41:52 -0300 Subject: [PATCH 1/4] chore: one direction for uniqueness paths --- src/Algebra/Group/Ab/Abelianisation.lagda.md | 2 +- src/Algebra/Group/Ab/Sum.lagda.md | 2 +- src/Algebra/Group/Ab/Tensor.lagda.md | 1 - .../Group/Cat/FinitelyComplete.lagda.md | 11 +- .../Group/Concrete/FinitelyComplete.lagda.md | 2 +- src/Algebra/Group/Free.lagda.md | 32 ++++-- src/Algebra/Group/Free/Product.lagda.md | 2 +- src/Algebra/Group/Free/Words.lagda.md | 2 +- src/Algebra/Group/Instances/Integers.lagda.md | 6 +- src/Algebra/Group/Subgroup.lagda.md | 3 +- src/Algebra/Ring/Module/Category.lagda.md | 2 +- src/Algebra/Ring/Module/Free.lagda.md | 2 +- src/Algebra/Ring/Module/Vec.lagda.md | 2 +- src/Cat/Abelian/Base.lagda.md | 5 +- src/Cat/Abelian/Limits.lagda.md | 8 +- src/Cat/Bi/Functor/IndexedCategory.lagda.md | 2 +- src/Cat/Bi/Instances/Relations.lagda.md | 24 ++-- src/Cat/Bi/Instances/Spans.lagda.md | 12 +- src/Cat/Cartesian.lagda.md | 4 +- src/Cat/CartesianClosed/Free.lagda.md | 47 ++++---- src/Cat/CartesianClosed/Locally.lagda.md | 6 +- src/Cat/CartesianClosed/Solver.lagda.md | 21 ++-- src/Cat/Diagram/Biproduct.lagda.md | 2 +- src/Cat/Diagram/Coend.lagda.md | 2 +- src/Cat/Diagram/Coend/Sets.lagda.md | 2 +- src/Cat/Diagram/Coequaliser.lagda.md | 26 ++--- src/Cat/Diagram/Colimit/Base.lagda.md | 16 +-- src/Cat/Diagram/Colimit/Cocone.lagda.md | 4 +- src/Cat/Diagram/Colimit/Finite.lagda.md | 17 ++- src/Cat/Diagram/Colimit/Initial.lagda.md | 10 +- src/Cat/Diagram/Colimit/Pushout.lagda.md | 4 +- src/Cat/Diagram/Comonad/Writer.lagda.md | 15 ++- src/Cat/Diagram/Congruence.lagda.md | 4 +- src/Cat/Diagram/Coproduct.lagda.md | 48 ++++---- src/Cat/Diagram/Coproduct/Copower.lagda.md | 11 +- src/Cat/Diagram/Coproduct/Indexed.lagda.md | 28 +++-- src/Cat/Diagram/Equaliser.lagda.md | 10 +- src/Cat/Diagram/Equaliser/Joint.lagda.md | 8 +- src/Cat/Diagram/Exponential.lagda.md | 107 ++++++++---------- src/Cat/Diagram/Limit/Base.lagda.md | 18 +-- src/Cat/Diagram/Limit/Cone.lagda.md | 2 +- src/Cat/Diagram/Limit/Finite.lagda.md | 12 +- src/Cat/Diagram/Limit/Initial.lagda.md | 2 +- src/Cat/Diagram/Limit/Isomorph.lagda.md | 2 +- src/Cat/Diagram/Limit/Pullback.lagda.md | 6 +- src/Cat/Diagram/Limit/Terminal.lagda.md | 10 +- src/Cat/Diagram/Omega.lagda.md | 16 +-- src/Cat/Diagram/Product.lagda.md | 67 +++++------ src/Cat/Diagram/Product/Finite.lagda.md | 12 +- src/Cat/Diagram/Product/Indexed.lagda.md | 36 +++--- src/Cat/Diagram/Product/Power.lagda.md | 4 +- src/Cat/Diagram/Product/Solver.lagda.md | 4 +- src/Cat/Diagram/Pullback.lagda.md | 28 +++-- src/Cat/Diagram/Pullback/Properties.lagda.md | 10 +- src/Cat/Diagram/Pushout.lagda.md | 10 +- src/Cat/Diagram/Pushout/Properties.lagda.md | 24 ++-- src/Cat/Diagram/Separator.lagda.md | 43 +++---- src/Cat/Diagram/Separator/Strong.lagda.md | 28 ++--- src/Cat/Diagram/Subterminal.lagda.md | 34 +++--- src/Cat/Displayed/BeckChevalley.lagda.md | 36 +++--- src/Cat/Displayed/Bifibration.lagda.md | 2 +- src/Cat/Displayed/Cartesian.lagda.md | 60 +++++----- src/Cat/Displayed/Cartesian/Indexing.lagda.md | 22 ++-- src/Cat/Displayed/Cartesian/Joint.lagda.md | 45 ++++---- src/Cat/Displayed/Cartesian/Weak.lagda.md | 68 +++++------ src/Cat/Displayed/Cocartesian.lagda.md | 41 +++---- .../Displayed/Cocartesian/Indexing.lagda.md | 4 +- src/Cat/Displayed/Cocartesian/Weak.lagda.md | 79 +++++-------- src/Cat/Displayed/Comprehension.lagda.md | 16 ++- .../Comprehension/Coproduct.lagda.md | 14 +-- .../Diagram/Total/Exponential.lagda.md | 2 +- .../Displayed/Diagram/Total/Product.lagda.md | 4 +- src/Cat/Displayed/Doctrine/Logic.lagda.md | 17 +-- src/Cat/Displayed/GenericObject.lagda.md | 6 +- .../Displayed/Instances/CT-Structure.lagda.md | 4 +- src/Cat/Displayed/Instances/Chaotic.lagda.md | 56 +++++---- .../Instances/DisplayedFamilies.lagda.md | 12 +- .../Instances/Externalisation.lagda.md | 52 ++++----- src/Cat/Displayed/Instances/Family.lagda.md | 19 ++-- .../Instances/Family/Properties.lagda.md | 4 +- src/Cat/Displayed/Instances/Gluing.lagda.md | 12 +- src/Cat/Displayed/Instances/Lifting.lagda.md | 4 +- src/Cat/Displayed/Instances/Opposite.lagda.md | 2 +- src/Cat/Displayed/Instances/Simple.lagda.md | 18 +-- src/Cat/Displayed/Instances/Slice.lagda.md | 2 +- src/Cat/Displayed/Total.lagda.md | 6 +- src/Cat/Displayed/Univalence/Thin.lagda.md | 1 + src/Cat/Functor/Adjoint.lagda.md | 32 +++--- src/Cat/Functor/Adjoint/Cofree.lagda.md | 2 +- src/Cat/Functor/Adjoint/Colimit.lagda.md | 2 +- src/Cat/Functor/Adjoint/Continuous.lagda.md | 37 +++--- src/Cat/Functor/Adjoint/Properties.lagda.md | 4 +- src/Cat/Functor/Algebra.lagda.md | 2 +- src/Cat/Functor/Dense.lagda.md | 4 +- src/Cat/Functor/Hom/Coyoneda.lagda.md | 2 +- src/Cat/Functor/Kan/Pointwise.lagda.md | 18 ++- src/Cat/Functor/Monadic/Beck.lagda.md | 28 +++-- src/Cat/Functor/Pullback.lagda.md | 8 +- .../Instances/Assemblies/Colimits.lagda.md | 4 +- .../Assemblies/Exponentials.lagda.md | 2 +- src/Cat/Instances/Assemblies/Limits.lagda.md | 5 +- .../Instances/Coalgebras/Cartesian.lagda.md | 4 +- src/Cat/Instances/Coalgebras/Limits.lagda.md | 2 +- src/Cat/Instances/Comma/Limits.lagda.md | 3 +- src/Cat/Instances/FinSets/Omega.lagda.md | 4 +- src/Cat/Instances/Free.lagda.md | 4 +- src/Cat/Instances/Functor/Limits.lagda.md | 4 +- .../Instances/Graphs/Exponentials.lagda.md | 4 +- src/Cat/Instances/Graphs/Limits.lagda.md | 8 +- src/Cat/Instances/MarkedGraphs.lagda.md | 4 +- src/Cat/Instances/OFE/Coproduct.lagda.md | 4 +- src/Cat/Instances/OFE/Product.lagda.md | 4 +- src/Cat/Instances/OuterFunctor.lagda.md | 5 +- src/Cat/Instances/Presheaf/Colimits.lagda.md | 6 +- src/Cat/Instances/Presheaf/Limits.lagda.md | 5 +- src/Cat/Instances/Presheaf/Omega.lagda.md | 4 +- src/Cat/Instances/Sets/Cocomplete.lagda.md | 14 +-- src/Cat/Instances/Sets/Complete.lagda.md | 13 +-- src/Cat/Instances/Sets/Congruences.lagda.md | 16 ++- src/Cat/Instances/Slice.lagda.md | 24 ++-- src/Cat/Instances/Slice/Colimit.lagda.md | 4 +- src/Cat/Instances/StrictCat.lagda.md | 5 +- src/Cat/Internal/Functor/Outer.lagda.md | 32 +++--- .../Internal/Instances/Congruence.lagda.md | 24 ++-- .../Diagram/Monoid/Representable.lagda.md | 2 +- src/Cat/Monoidal/Instances/Cartesian.lagda.md | 2 +- src/Cat/Morphism/Joint/Mono.lagda.md | 22 ++-- src/Cat/Regular.lagda.md | 30 ++--- src/Cat/Site/Instances/Canonical.lagda.md | 2 +- src/Cat/Site/Sheafification.lagda.md | 3 +- src/Data/Set/Surjection.lagda.md | 4 +- src/Order/Instances/Coproduct.lagda.md | 4 +- src/Order/Instances/Disjoint.lagda.md | 2 +- .../Instances/Lower/Cocompletion.lagda.md | 4 +- src/Order/Instances/Pointwise.lagda.md | 2 +- src/Order/Instances/Product.lagda.md | 2 +- src/Order/Semilattice/Free.lagda.md | 10 +- 137 files changed, 933 insertions(+), 991 deletions(-) diff --git a/src/Algebra/Group/Ab/Abelianisation.lagda.md b/src/Algebra/Group/Ab/Abelianisation.lagda.md index 28e551c81..35f7132bf 100644 --- a/src/Algebra/Group/Ab/Abelianisation.lagda.md +++ b/src/Algebra/Group/Ab/Abelianisation.lagda.md @@ -220,5 +220,5 @@ make-free-abelian G .fold {H} f .fst = make-free-abelian G .fold {H} f .snd .is-group-hom.pres-⋆ = elim! λ _ _ → f .snd .is-group-hom.pres-⋆ _ _ make-free-abelian G .commute = ext λ _ → refl -make-free-abelian G .unique f p = ext (p ·ₚ_) +make-free-abelian G .unique f p = ext (sym p ·ₚ_) ``` diff --git a/src/Algebra/Group/Ab/Sum.lagda.md b/src/Algebra/Group/Ab/Sum.lagda.md index 01caf55ba..52216a3c8 100644 --- a/src/Algebra/Group/Ab/Sum.lagda.md +++ b/src/Algebra/Group/Ab/Sum.lagda.md @@ -85,5 +85,5 @@ limits][rapl]). Direct-sum-is-product .π₁∘⟨⟩ = ext λ _ → refl Direct-sum-is-product .π₂∘⟨⟩ = ext λ _ → refl - Direct-sum-is-product .unique p q = ext λ x → p ·ₚ x ,ₚ q ·ₚ x + Direct-sum-is-product .unique p q = ext λ x → sym p ·ₚ x ,ₚ sym q ·ₚ x ``` diff --git a/src/Algebra/Group/Ab/Tensor.lagda.md b/src/Algebra/Group/Ab/Tensor.lagda.md index 3858e936d..b00dd3860 100644 --- a/src/Algebra/Group/Ab/Tensor.lagda.md +++ b/src/Algebra/Group/Ab/Tensor.lagda.md @@ -328,7 +328,6 @@ module _ {ℓ} {A B C : Abelian-group ℓ} where instance {f = λ h → curry-bilinear (Hom≃Bilinear.to h)} (λ {x} p → Hom≃Bilinear.injective (Equiv.injective (_ , curry-bilinear-is-equiv) p)) ef - {-# OVERLAPS Extensional-tensor-hom #-} ``` --> diff --git a/src/Algebra/Group/Cat/FinitelyComplete.lagda.md b/src/Algebra/Group/Cat/FinitelyComplete.lagda.md index 313ea90cf..27f52f72a 100644 --- a/src/Algebra/Group/Cat/FinitelyComplete.lagda.md +++ b/src/Algebra/Group/Cat/FinitelyComplete.lagda.md @@ -129,10 +129,9 @@ Direct-product-is-product {G} {H} = p where open is-product p : is-product _ _ _ p .⟨_,_⟩ = factor - p .π₁∘⟨⟩ = Grp↪Sets-is-faithful refl - p .π₂∘⟨⟩ = Grp↪Sets-is-faithful refl - p .unique p q = Grp↪Sets-is-faithful (funext λ x → - ap₂ _,_ (happly (ap fst p) x) (happly (ap fst q) x)) + p .π₁∘⟨⟩ = ext λ _ → refl + p .π₂∘⟨⟩ = ext λ _ → refl + p .unique p q = ext λ x i → p (~ i) .fst x , q (~ i) .fst x ``` What sets the direct product of groups apart from (e.g.) the cartesian @@ -145,12 +144,12 @@ a coproduct. inj₁ : G Groups.↪ Direct-product G H inj₁ {G} {H} .mor .fst x = x , H .snd .unit inj₁ {G} {H} .mor .snd .pres-⋆ x y = ap (_ ,_) (sym (H .snd .idl)) -inj₁ {G} {H} .monic g h x = Grp↪Sets-is-faithful (funext λ e i → (x i · e) .fst) +inj₁ {G} {H} .monic g h x = ext λ e i → (x i · e) .fst inj₂ : H Groups.↪ Direct-product G H inj₂ {H} {G} .mor .fst x = G .snd .unit , x inj₂ {H} {G} .mor .snd .pres-⋆ x y = ap (_, _) (sym (G .snd .idl)) -inj₂ {H} {G} .monic g h x = Grp↪Sets-is-faithful (funext λ e i → (x i · e) .snd) +inj₂ {H} {G} .monic g h x = ext λ e i → (x i · e) .snd ``` ## Equalisers diff --git a/src/Algebra/Group/Concrete/FinitelyComplete.lagda.md b/src/Algebra/Group/Concrete/FinitelyComplete.lagda.md index de1f8af71..4e584eb6d 100644 --- a/src/Algebra/Group/Concrete/FinitelyComplete.lagda.md +++ b/src/Algebra/Group/Concrete/FinitelyComplete.lagda.md @@ -63,7 +63,7 @@ ConcreteGroups-products X Y = prod where prod .has-is-product .π₁∘⟨⟩ = funext∙ (λ _ → refl) (∙-idr _) prod .has-is-product .π₂∘⟨⟩ = funext∙ (λ _ → refl) (∙-idr _) prod .has-is-product .unique {Q} {f} {g} {u} p1 p2 = - funext∙ (λ x → p1 ·ₚ x ,ₚ p2 ·ₚ x) (fix ◁ square) + sym $ funext∙ (λ x → p1 ·ₚ x ,ₚ p2 ·ₚ x) (fix ◁ square) where square : Square (p1 ·ₚ pt Q ,ₚ p2 ·ₚ pt Q) ((fst∙ ∘∙ u) .snd ,ₚ (snd∙ ∘∙ u) .snd) diff --git a/src/Algebra/Group/Free.lagda.md b/src/Algebra/Group/Free.lagda.md index b9bae9e8c..a10f24988 100644 --- a/src/Algebra/Group/Free.lagda.md +++ b/src/Algebra/Group/Free.lagda.md @@ -105,6 +105,28 @@ unquoteDef Free-elim-prop = make-elim-with (default-elim-visible into 1) + + ## Universal property {defines=free-group} We now prove the universal property of `Free-group`{.Agda}, or, more @@ -175,15 +197,7 @@ make-free-group S .free = Free-Group ⌞ S ⌟ make-free-group S .unit = inc make-free-group S .fold = fold-free-group make-free-group S .commute = refl -make-free-group S .unique {H} g p = - ext $ Free-elim-prop _ (λ _ → hlevel 1) - (p ·ₚ_) - (λ a p b q → g.pres-⋆ a b ∙ ap₂ H._⋆_ p q) - (λ a p → g.pres-inv ∙ ap H.inverse p) - g.pres-id - where - module H = Group-on (H .snd) - module g = is-group-hom (g .snd) +make-free-group S .unique {H} g p = ext (sym p ·ₚ_) module Free-groups {ℓ} (S : Set ℓ) = Free-object (make-free-group S) ``` diff --git a/src/Algebra/Group/Free/Product.lagda.md b/src/Algebra/Group/Free/Product.lagda.md index f8eebe205..43968e9c9 100644 --- a/src/Algebra/Group/Free/Product.lagda.md +++ b/src/Algebra/Group/Free/Product.lagda.md @@ -158,7 +158,7 @@ The universal property of the pushout is easy to verify. Groups-pushout .universal comm .snd .pres-⋆ _ _ = refl Groups-pushout .universal∘i₁ = ext λ _ → refl Groups-pushout .universal∘i₂ = ext λ _ → refl - Groups-pushout .unique {Q = Q} {colim' = u} comm₁ comm₂ = ext $ + Groups-pushout .unique {Q = Q} {colim' = u} comm₁ comm₂ = sym $ ext $ Amalgamated-elim-prop (λ _ → hlevel 1) (λ x p y q → u .snd .pres-⋆ x y ∙ ap₂ Q._⋆_ p q) (λ x p → pres-inv (u .snd) ∙ ap Q._⁻¹ p) diff --git a/src/Algebra/Group/Free/Words.lagda.md b/src/Algebra/Group/Free/Words.lagda.md index f902e56c4..6493881c1 100644 --- a/src/Algebra/Group/Free/Words.lagda.md +++ b/src/Algebra/Group/Free/Words.lagda.md @@ -553,7 +553,7 @@ more case bashes. First, we'll show that a group homomorphism $g : F(A) letters. ```agda -make-free-group .unique {Y} {f} g h = ext uniq where +make-free-group .unique {Y} {f} g h = sym $ ext uniq where open fold {Y} f module g = is-group-hom (g .snd) diff --git a/src/Algebra/Group/Instances/Integers.lagda.md b/src/Algebra/Group/Instances/Integers.lagda.md index 10879933e..29b7e6230 100644 --- a/src/Algebra/Group/Instances/Integers.lagda.md +++ b/src/Algebra/Group/Instances/Integers.lagda.md @@ -110,8 +110,8 @@ must lift it. This is the unique group homomorphism $\ZZ \to G$ that sends $1$ to $x$. ```agda - pow-unique : (g : Groups.Hom (Lift-group ℓ ℤ) G) → g · 1 ≡ x → g ≡ pow-hom - pow-unique g g1≡x = ext λ x → p x ∙ sym (q x) where + pow-unique : (g : Groups.Hom (Lift-group ℓ ℤ) G) → g · 1 ≡ x → pow-hom ≡ g + pow-unique g g1≡x = ext λ x → q x ∙ sym (p x) where pow' = ℤ.map-out unit ((_⋆ x) , ⋆-equivr x) p : ∀ x → g · lift x ≡ pow' x p = ℤ.map-out-unique (λ i → g · lift i) (pres-id (g .snd)) λ y → @@ -126,7 +126,7 @@ This is the unique group homomorphism $\ZZ \to G$ that sends $1$ to $x$. open pow public pow-unique₂ : (g h : Groups.Hom (Lift-group ℓ ℤ) G) → g · 1 ≡ h · 1 → g ≡ h - pow-unique₂ g h p = pow-unique (g · 1) g refl ∙ sym (pow-unique (g · 1) h (sym p)) + pow-unique₂ g h p = sym (pow-unique (g · 1) g refl) ∙ pow-unique (g · 1) h (sym p) ```
diff --git a/src/Algebra/Group/Subgroup.lagda.md b/src/Algebra/Group/Subgroup.lagda.md index f12c3a4db..ea96138b1 100644 --- a/src/Algebra/Group/Subgroup.lagda.md +++ b/src/Algebra/Group/Subgroup.lagda.md @@ -330,7 +330,8 @@ will compute. coeq .factors = Grp↪Sets-is-faithful refl coeq .unique {F} {p = p} {colim = colim} prf = ext λ x y p → - ap· colim (Σ-prop-path! (sym p)) ∙ happly (ap fst prf) y + sym (ap fst prf) ·ₚ y + ∙ ap· colim (Σ-prop-path! p) ``` ## Representing kernels diff --git a/src/Algebra/Ring/Module/Category.lagda.md b/src/Algebra/Ring/Module/Category.lagda.md index aa179cce7..ba2716d58 100644 --- a/src/Algebra/Ring/Module/Category.lagda.md +++ b/src/Algebra/Ring/Module/Category.lagda.md @@ -261,7 +261,7 @@ path-mangling, but it's nothing _too_ bad: Σ-pathp (f .snd .linear _ _ _) (g .snd .linear _ _ _) prod .has-is-product .π₁∘⟨⟩ = ext λ _ → refl prod .has-is-product .π₂∘⟨⟩ = ext λ _ → refl - prod .has-is-product .unique p q = ext λ x → p ·ₚ x ,ₚ q ·ₚ x + prod .has-is-product .unique p q = ext λ x → sym p ·ₚ x ,ₚ sym q ·ₚ x ``` diff --git a/src/Cat/CartesianClosed/Locally.lagda.md b/src/Cat/CartesianClosed/Locally.lagda.md index fd04047da..51822771e 100644 --- a/src/Cat/CartesianClosed/Locally.lagda.md +++ b/src/Cat/CartesianClosed/Locally.lagda.md @@ -188,8 +188,10 @@ isomorphic. Slice-product-functor .inv x .com = idr _ ∙ sym (pullbacks _ _ .square) Slice-product-functor .eta∘inv x = ext $ idl _ Slice-product-functor .inv∘eta x = ext $ idl _ - Slice-product-functor .natural x y f = ext $ id-comm ∙ ap (id ∘_) (pullbacks _ _ .unique - (pullbacks _ _ .p₁∘universal) (pullbacks _ _ .p₂∘universal ∙ idl _)) + Slice-product-functor .natural x y f = ext $ id-comm ∙ ap (id ∘_) (sym $ + pullbacks _ _ .unique + (pullbacks _ _ .p₁∘universal) + (pullbacks _ _ .p₂∘universal ∙ idl _)) ``` If we then have a functor $\Pi_f$ fitting into an adjoint triple diff --git a/src/Cat/CartesianClosed/Solver.lagda.md b/src/Cat/CartesianClosed/Solver.lagda.md index 1c4056aad..189258512 100644 --- a/src/Cat/CartesianClosed/Solver.lagda.md +++ b/src/Cat/CartesianClosed/Solver.lagda.md @@ -252,7 +252,7 @@ ren-⟦⟧ᵣ : (ρ : Ren Δ Γ) (σ : Sub Γ Θ) → ⟦ ren-sub ρ σ ⟧ᵣ ⟦⟧-∘ʳ (drop ρ) σ = pushl (⟦⟧-∘ʳ ρ σ) ⟦⟧-∘ʳ (keep ρ) stop = introl refl ⟦⟧-∘ʳ (keep ρ) (drop σ) = pushl (⟦⟧-∘ʳ ρ σ) ∙ sym (pullr π₁∘⟨⟩) -⟦⟧-∘ʳ (keep ρ) (keep σ) = sym $ ⟨⟩-unique +⟦⟧-∘ʳ (keep ρ) (keep σ) = ⟨⟩-unique (pulll π₁∘⟨⟩ ∙ pullr π₁∘⟨⟩ ∙ pulll (sym (⟦⟧-∘ʳ ρ σ))) (pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩ ∙ idl _) @@ -263,7 +263,7 @@ ren-⟦⟧ⁿ (keep ρ) (pop v) = pushl (ren-⟦⟧ⁿ ρ v) ∙ sym (pullr π ren-⟦⟧ₛ ρ (var x) = ren-⟦⟧ⁿ ρ x ren-⟦⟧ₛ ρ (app f x) = ap₂ _∘_ refl - (ap₂ ⟨_,_⟩ (ren-⟦⟧ₛ ρ f) (ren-⟦⟧ₙ ρ x) ∙ sym (⟨⟩∘ _)) + (ap₂ ⟨_,_⟩ (ren-⟦⟧ₛ ρ f) (ren-⟦⟧ₙ ρ x) ∙ ⟨⟩∘ _) ∙ pulll refl ren-⟦⟧ₛ ρ (fstₙ t) = pushr (ren-⟦⟧ₛ ρ t) ren-⟦⟧ₛ ρ (sndₙ t) = pushr (ren-⟦⟧ₛ ρ t) @@ -271,17 +271,17 @@ ren-⟦⟧ₛ ρ (hom x a) = pushr (ren-⟦⟧ᵣ ρ a) ren-⟦⟧ₙ ρ (lam t) = ap ƛ (ren-⟦⟧ₙ (keep ρ) t) - ∙ sym (unique _ (ap₂ _∘_ refl rem₁ ∙ pulll (commutes ⟦ t ⟧ₙ))) + ∙ unique _ (ap₂ _∘_ refl rem₁ ∙ pulll (commutes ⟦ t ⟧ₙ)) where rem₁ : (⟦ lam t ⟧ₙ ∘ ⟦ ρ ⟧ʳ) ⊗₁ id ≡ (⟦ lam t ⟧ₙ ⊗₁ id) ∘ ⟦ ρ ⟧ʳ ⊗₁ id rem₁ = Bifunctor.lmap-∘ (Curry ×-functor) _ _ -ren-⟦⟧ₙ ρ (pair a b) = ap₂ ⟨_,_⟩ (ren-⟦⟧ₙ ρ a) (ren-⟦⟧ₙ ρ b) ∙ sym (⟨⟩∘ _) +ren-⟦⟧ₙ ρ (pair a b) = ap₂ ⟨_,_⟩ (ren-⟦⟧ₙ ρ a) (ren-⟦⟧ₙ ρ b) ∙ ⟨⟩∘ _ ren-⟦⟧ₙ ρ (ne x) = ren-⟦⟧ₛ ρ x ren-⟦⟧ₙ ρ unit = !-unique _ ren-⟦⟧ᵣ ρ ∅ = !-unique _ -ren-⟦⟧ᵣ ρ (σ , n) = ap₂ ⟨_,_⟩ (ren-⟦⟧ᵣ ρ σ) (ren-⟦⟧ₙ ρ n) ∙ sym (⟨⟩∘ _) +ren-⟦⟧ᵣ ρ (σ , n) = ap₂ ⟨_,_⟩ (ren-⟦⟧ᵣ ρ σ) (ren-⟦⟧ₙ ρ n) ∙ ⟨⟩∘ _ Tyᵖ : (τ : Ty) (Γ : Cx) → Hom ⟦ Γ ⟧ᶜ ⟦ τ ⟧ᵗ → Type (o ⊔ ℓ) Tyᵖ (τ `× σ) Γ h = Tyᵖ τ Γ (π₁ ∘ h) × Tyᵖ σ Γ (π₂ ∘ h) @@ -338,15 +338,14 @@ reflectᵖ {τ = τ `⇒ σ} n ρ a = tyᵖ⟨ ap₂ (λ e f → ev ∘ ⟨ e , reflectᵖ {τ = ` x} n = n , refl reflectᵖ {τ = `⊤} _ = lift tt -reifyᵖ-correct {τ = τ `× σ} (a , b) = sym $ - ⟨⟩-unique (sym (reifyᵖ-correct a)) (sym (reifyᵖ-correct b)) +reifyᵖ-correct {τ = τ `× σ} (a , b) = ⟨⟩-unique (sym (reifyᵖ-correct a)) (sym (reifyᵖ-correct b)) reifyᵖ-correct {τ = τ `⇒ σ} {h = h} ν = ƛ ⟦ reifyᵖ (ν (drop stop) (reflectᵖ (var stop))) ⟧ₙ ≡⟨ ap ƛ (reifyᵖ-correct (ν (drop stop) (reflectᵖ (var stop)))) ⟩ ƛ (ev ∘ ⟨ h ∘ id ∘ π₁ , π₂ ⟩) ≡⟨ ap₂ (λ a b → ƛ (ev ∘ ⟨ a , b ⟩)) (pulll (elimr refl)) (introl refl) ⟩ ƛ (unlambda h) - ≡˘⟨ unique _ refl ⟩ + ≡⟨ unique _ refl ⟩ h ∎ reifyᵖ-correct {τ = ` x} d = d .snd reifyᵖ-correct {τ = `⊤} d = !-unique _ @@ -363,7 +362,7 @@ private , tyᵖ⟨ pullr refl ⟩ (tickᵖ (π₂ ∘ m) a) tickᵖ {x = x} {y = τ `⇒ σ} m a ρ y = - tyᵖ⟨ pullr (⟨⟩-unique (pulll π₁∘⟨⟩ ∙ extendr π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ π₂∘⟨⟩)) ⟩ + tyᵖ⟨ pullr (sym (⟨⟩-unique (pulll π₁∘⟨⟩ ∙ extendr π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ π₂∘⟨⟩))) ⟩ (tickᵖ {x = x `× τ} (ev ∘ ⟨ m ∘ π₁ , π₂ ⟩) (tyᵖ⟨ sym π₁∘⟨⟩ ⟩ (ren-tyᵖ ρ a) , tyᵖ⟨ sym π₂∘⟨⟩ ⟩ y)) @@ -381,7 +380,7 @@ private ; snd = tyᵖ⟨ sym (pulll π₂∘⟨⟩) ⟩ (morᵖ f ρ) } - morᵖ `ev (f , x) = tyᵖ⟨ ap (ev ∘_) (sym (⟨⟩-unique (intror refl) refl)) ⟩ + morᵖ `ev (f , x) = tyᵖ⟨ ap (ev ∘_) (⟨⟩-unique (intror refl) refl) ⟩ (f stop x) morᵖ {h = h} (`ƛ e) t r {h'} a = tyᵖ⟨ sym p ⟩ (morᵖ e @@ -390,7 +389,7 @@ private where p = ev ∘ ⟨ ((ƛ ⟦ e ⟧ᵐ) ∘ h) ∘ ⟦ r ⟧ʳ , h' ⟩ - ≡⟨ ap (ev ∘_) (sym (⟨⟩-unique (pulll π₁∘⟨⟩ ∙ pullr π₁∘⟨⟩ ∙ pulll refl) (pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩ ∙ idl _))) ⟩ + ≡⟨ ap (ev ∘_) (⟨⟩-unique (pulll π₁∘⟨⟩ ∙ pullr π₁∘⟨⟩ ∙ pulll refl) (pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩ ∙ idl _)) ⟩ ev ∘ (ƛ ⟦ e ⟧ᵐ ⊗₁ id) ∘ ⟨ h ∘ ⟦ r ⟧ʳ , h' ⟩ ≡⟨ pulll (commutes _) ⟩ ⟦ e ⟧ᵐ ∘ ⟨ h ∘ ⟦ r ⟧ʳ , h' ⟩ diff --git a/src/Cat/Diagram/Biproduct.lagda.md b/src/Cat/Diagram/Biproduct.lagda.md index 4e5f4d9b2..aed08c79e 100644 --- a/src/Cat/Diagram/Biproduct.lagda.md +++ b/src/Cat/Diagram/Biproduct.lagda.md @@ -272,7 +272,7 @@ coproducts coincide. ((cancelr πι₂ ⟩∘⟨refl) ∙ πι₂) ∙ sym (pulll π₂∘⟨⟩)) - coswap≡swap = ⟨⟩-unique + coswap≡swap = sym $ ⟨⟩-unique (Biprod.[]-unique₂ (pullr []∘ι₁ ∙ π₁-ι₂) (pullr []∘ι₂ ∙ πι₁) π₂-ι₁ πι₂) diff --git a/src/Cat/Diagram/Coend.lagda.md b/src/Cat/Diagram/Coend.lagda.md index ad341e529..35703a9b6 100644 --- a/src/Cat/Diagram/Coend.lagda.md +++ b/src/Cat/Diagram/Coend.lagda.md @@ -177,5 +177,5 @@ properties of colimiting maps for every other colimit. unique : ∀ {W : Cowedge F} {g : D.Hom cowedge.nadir (W .nadir)} → (∀ {a} → g D.∘ cowedge.ψ a ≡ W .ψ a) - → g ≡ factor W + → factor W ≡ g ``` diff --git a/src/Cat/Diagram/Coend/Sets.lagda.md b/src/Cat/Diagram/Coend/Sets.lagda.md index 0d193de56..2c2487af6 100644 --- a/src/Cat/Diagram/Coend/Sets.lagda.md +++ b/src/Cat/Diagram/Coend/Sets.lagda.md @@ -96,7 +96,7 @@ to the family associated to the cowedge `W`. coend .cowedge = universal-cowedge coend .factor W = factoring W coend .commutes = refl - coend .unique {W = W} p = ext λ X x → p ·ₚ x + coend .unique {W = W} p = ext λ X x → sym p ·ₚ x ``` This construction is actually functorial! Given any functor diff --git a/src/Cat/Diagram/Coequaliser.lagda.md b/src/Cat/Diagram/Coequaliser.lagda.md index 78fb2070a..7792f5b18 100644 --- a/src/Cat/Diagram/Coequaliser.lagda.md +++ b/src/Cat/Diagram/Coequaliser.lagda.md @@ -42,14 +42,14 @@ and $g$. ```agda record is-coequaliser {E} (f g : Hom A B) (coeq : Hom B E) : Type (o ⊔ ℓ) where field - coequal : coeq ∘ f ≡ coeq ∘ g - universal : ∀ {F} {e' : Hom B F} (p : e' ∘ f ≡ e' ∘ g) → Hom E F - factors : ∀ {F} {e' : Hom B F} {p : e' ∘ f ≡ e' ∘ g} - → universal p ∘ coeq ≡ e' - - unique : ∀ {F} {e' : Hom B F} {p : e' ∘ f ≡ e' ∘ g} {colim : Hom E F} - → colim ∘ coeq ≡ e' - → colim ≡ universal p + coequal : coeq ∘ f ≡ coeq ∘ g + universal : ∀ {F} {e' : Hom B F} (p : e' ∘ f ≡ e' ∘ g) → Hom E F + factors + : ∀ {F} {e' : Hom B F} {p : e' ∘ f ≡ e' ∘ g} + → universal p ∘ coeq ≡ e' + unique + : ∀ {F} {e' : Hom B F} {p : e' ∘ f ≡ e' ∘ g} {colim : Hom E F} + → colim ∘ coeq ≡ e' → universal p ≡ colim unique₂ : ∀ {F} {e' : Hom B F} {o1 o2 : Hom E F} @@ -57,9 +57,9 @@ and $g$. → o1 ∘ coeq ≡ e' → o2 ∘ coeq ≡ e' → o1 ≡ o2 - unique₂ p q r = unique {p = p} q ∙ sym (unique r) + unique₂ p q r = sym (unique {p = p} q) ∙ unique r - id-coequalise : id ≡ universal coequal + id-coequalise : universal coequal ≡ id id-coequalise = unique (idl _) ``` @@ -97,9 +97,9 @@ module _ {o ℓ} {C : Precategory o ℓ} where → is-coequaliser C f g coequ → is-epic coequ is-coequaliser→is-epic {f = f} {g = g} equ equalises h i p = - h ≡⟨ unique p ⟩ - universal (extendr coequal) ≡˘⟨ unique refl ⟩ - i ∎ + h ≡˘⟨ unique p ⟩ + universal (extendr coequal) ≡⟨ unique refl ⟩ + i ∎ where open is-coequaliser equalises coequaliser-unique diff --git a/src/Cat/Diagram/Colimit/Base.lagda.md b/src/Cat/Diagram/Colimit/Base.lagda.md index b5cf8b735..73eb7b363 100644 --- a/src/Cat/Diagram/Colimit/Base.lagda.md +++ b/src/Cat/Diagram/Colimit/Base.lagda.md @@ -136,7 +136,7 @@ morphism: → (p : ∀ {x y} (f : J.Hom x y) → eta y C.∘ F₁ f ≡ eta x) → (other : C.Hom coapex x) → (∀ j → other C.∘ ψ j ≡ eta j) - → other ≡ universal eta p + → universal eta p ≡ other ``` @@ -186,7 +186,7 @@ the rest of the data. colim .σ {M = M} α .is-natural _ _ _ = C.idr _ ∙ C.introl (M .F-id) colim .σ-comm {α = α} = ext λ j → factors (α .η) _ colim .σ-uniq {α = α} {σ' = σ'} p = ext λ _ → - sym $ unique (α .η) _ (σ' .η _) (λ j → sym (p ηₚ j)) + unique (α .η) _ (σ' .η _) (λ j → sym (p ηₚ j)) ``` @@ -358,7 +358,7 @@ Understanding the transitivity map is left as an exercise to the reader. cg .trans-factors = sym ( kernel-pair ∘ Kp.universal _ - ≡⟨ a×a.⟨⟩∘ _ ⟩ + ≡⟨ sym (a×a.⟨⟩∘ _) ⟩ a×a.⟨ Kp.p₁ ∘ Kp.universal _ , Kp.p₂ ∘ Kp.universal _ ⟩ ≡⟨ ap₂ a×a.⟨_,_⟩ (Kp.p₁∘universal ∙ ap₂ _∘_ (sym a×a.π₁∘⟨⟩) refl) (Kp.p₂∘universal ∙ ap₂ _∘_ (sym a×a.π₂∘⟨⟩) refl) ⟩ diff --git a/src/Cat/Diagram/Coproduct.lagda.md b/src/Cat/Diagram/Coproduct.lagda.md index afad7ffc4..f1ebebb3e 100644 --- a/src/Cat/Diagram/Coproduct.lagda.md +++ b/src/Cat/Diagram/Coproduct.lagda.md @@ -51,17 +51,17 @@ $Q$. This is best explained by a commutative diagram: []∘ι₁ : ∀ {Q} {inj0 : Hom A Q} {inj1} → [ inj0 , inj1 ] ∘ ι₁ ≡ inj0 []∘ι₂ : ∀ {Q} {inj0 : Hom A Q} {inj1} → [ inj0 , inj1 ] ∘ ι₂ ≡ inj1 - unique : ∀ {Q} {inj0 : Hom A Q} {inj1} - → {other : Hom P Q} - → other ∘ ι₁ ≡ inj0 - → other ∘ ι₂ ≡ inj1 - → other ≡ [ inj0 , inj1 ] - - unique₂ : ∀ {Q} {inj0 : Hom A Q} {inj1} - → ∀ {o1} (p1 : o1 ∘ ι₁ ≡ inj0) (q1 : o1 ∘ ι₂ ≡ inj1) - → ∀ {o2} (p2 : o2 ∘ ι₁ ≡ inj0) (q2 : o2 ∘ ι₂ ≡ inj1) - → o1 ≡ o2 - unique₂ p1 q1 p2 q2 = unique p1 q1 ∙ sym (unique p2 q2) + unique + : ∀ {Q} {inj0 : Hom A Q} {inj1} {other : Hom P Q} + → other ∘ ι₁ ≡ inj0 → other ∘ ι₂ ≡ inj1 + → [ inj0 , inj1 ] ≡ other + + unique₂ + : ∀ {Q} {inj0 : Hom A Q} {inj1} + → ∀ {o1} (p1 : o1 ∘ ι₁ ≡ inj0) (q1 : o1 ∘ ι₂ ≡ inj1) + → ∀ {o2} (p2 : o2 ∘ ι₁ ≡ inj0) (q2 : o2 ∘ ι₂ ≡ inj1) + → o1 ≡ o2 + unique₂ p1 q1 p2 q2 = sym (unique p1 q1) ∙ unique p2 q2 ``` A coproduct of $A$ and $B$ is an explicit choice of coproduct diagram: @@ -88,12 +88,15 @@ module _ {o ℓ} {C : Precategory o ℓ} where is-coproduct-is-prop {X = X} {Y = Y} {i₁ = i₁} {i₂} x y = q where open is-coproduct p : Path (∀ {P'} → Hom X P' → Hom Y P' → _) (x .[_,_]) (y .[_,_]) - p i inj0 inj1 = y .unique {inj0 = inj0} {inj1} (x .[]∘ι₁) (x .[]∘ι₂) i + p i inj0 inj1 = y .unique {inj0 = inj0} {inj1} (x .[]∘ι₁) (x .[]∘ι₂) (~ i) q : x ≡ y q i .[_,_] = p i q i .[]∘ι₁ {inj0 = inj0} {inj1} = is-prop→pathp (λ i → Hom-set _ _ (p i inj0 inj1 ∘ i₁) inj0) (x .[]∘ι₁) (y .[]∘ι₁) i q i .[]∘ι₂ {inj0 = inj0} {inj1} = is-prop→pathp (λ i → Hom-set _ _ (p i inj0 inj1 ∘ i₂) inj1) (x .[]∘ι₂) (y .[]∘ι₂) i - q i .unique {inj0 = inj0} {inj1} {other} c₁ c₂ = is-prop→pathp (λ i → Hom-set _ _ other (p i inj0 inj1)) (x .unique c₁ c₂) (y .unique c₁ c₂) i + q i .unique {inj0 = inj0} {inj1} {other} c₁ c₂ = is-prop→pathp + (λ i → Hom-set _ _ (p i inj0 inj1) other) + (x .unique c₁ c₂) + (y .unique c₁ c₂) i instance H-Level-is-coproduct : ∀ {X Y P} {i₁ : Hom X P} {i₂ : Hom Y P} {n} → H-Level (is-coproduct C i₁ i₂) (suc n) @@ -184,8 +187,8 @@ module _ {o ℓ} {C : Precategory o ℓ} where coprod' .[_,_] qa qb = coprod .[_,_] qa qb ∘ fi.inv coprod' .[]∘ι₁ = pullr (lswizzle (sym f-ι₁) fi.invr) ∙ coprod .[]∘ι₁ coprod' .[]∘ι₂ = pullr (lswizzle (sym f-ι₂) fi.invr) ∙ coprod .[]∘ι₂ - coprod' .unique p q = sym $ rswizzle - (sym (coprod .unique (pullr f-ι₁ ∙ p) (pullr f-ι₂ ∙ q))) fi.invl + coprod' .unique p q = rswizzle + (coprod .unique (pullr f-ι₁ ∙ p) (pullr f-ι₂ ∙ q)) fi.invl Coproduct-is-prop : ∀ {A B} @@ -224,11 +227,10 @@ module Binary-coproducts ⊕-functor : Functor (C ×ᶜ C) C ⊕-functor .F₀ (a , b) = a ⊕₀ b ⊕-functor .F₁ (f , g) = f ⊕₁ g - ⊕-functor .F-id = sym $ []-unique id-comm-sym id-comm-sym - ⊕-functor .F-∘ (f , g) (h , i) = - sym $ []-unique - (pullr []∘ι₁ ∙ extendl []∘ι₁) - (pullr []∘ι₂ ∙ extendl []∘ι₂) + ⊕-functor .F-id = []-unique id-comm-sym id-comm-sym + ⊕-functor .F-∘ (f , g) (h , i) = []-unique + (pullr []∘ι₁ ∙ extendl []∘ι₁) + (pullr []∘ι₂ ∙ extendl []∘ι₂) ∇ : ∀ {a} → Hom (a ⊕₀ a) a ∇ = [ id , id ] @@ -248,14 +250,14 @@ module Binary-coproducts (cancelr []∘ι₁) (cancelr []∘ι₂) ∇-coswap : ∀ {a} → ∇ ∘ coswap ≡ ∇ {a} - ∇-coswap = []-unique (pullr []∘ι₁ ∙ []∘ι₂) (pullr []∘ι₂ ∙ []∘ι₁) + ∇-coswap = sym $ []-unique (pullr []∘ι₁ ∙ []∘ι₂) (pullr []∘ι₂ ∙ []∘ι₁) ∇-assoc : ∀ {a} → ∇ {a} ∘ (∇ {a} ⊕₁ id) ∘ ⊕-assoc ≡ ∇ ∘ (id ⊕₁ ∇) ∇-assoc = unique₂ (pullr (pullr []∘ι₁) ∙ (refl⟩∘⟨ pulll []∘ι₁) ∙ pulll (pulll []∘ι₁) ∙ pullr []∘ι₁) - (pullr (pullr []∘ι₂) ∙ []-unique + (pullr (pullr []∘ι₂) ∙ sym ([]-unique (pullr (pullr []∘ι₁) ∙ extend-inner []∘ι₁ ∙ cancell []∘ι₁ ∙ []∘ι₂) - (pullr (pullr []∘ι₂) ∙ (refl⟩∘⟨ []∘ι₂) ∙ cancell []∘ι₂)) + (pullr (pullr []∘ι₂) ∙ (refl⟩∘⟨ []∘ι₂) ∙ cancell []∘ι₂))) (pullr []∘ι₁ ∙ pulll []∘ι₁) (pullr []∘ι₂ ∙ cancell []∘ι₂) ``` diff --git a/src/Cat/Diagram/Coproduct/Copower.lagda.md b/src/Cat/Diagram/Coproduct/Copower.lagda.md index 1a5bc0d18..eae761dc2 100644 --- a/src/Cat/Diagram/Coproduct/Copower.lagda.md +++ b/src/Cat/Diagram/Coproduct/Copower.lagda.md @@ -92,9 +92,8 @@ uniqueness properties of colimiting maps. Copowering .F₀ (X , A) = X ⊗ A Copowering .F₁ {X , A} {Y , B} (idx , obj) = coprods X (λ _ → A) .match λ i → coprods Y (λ _ → B) .ι (idx i) ∘ obj - Copowering .F-id {X , A} = sym $ - coprods X (λ _ → A) .unique _ λ i → sym id-comm - Copowering .F-∘ {X , A} f g = sym $ coprods X (λ _ → A) .unique _ λ i → + Copowering .F-id {X , A} = coprods X (λ _ → A) .unique _ λ i → sym id-comm + Copowering .F-∘ {X , A} f g = coprods X (λ _ → A) .unique _ λ i → pullr (coprods _ _ .commute) ∙ extendl (coprods _ _ .commute) ``` @@ -151,8 +150,8 @@ module Consts Constant-objects : Functor (Sets ℓ) C Constant-objects .F₀ S = S ⊗ *C Constant-objects .F₁ f = coprods _ _ .match λ i → coprods _ _ .ι (f i) - Constant-objects .F-id = sym $ coprods _ _ .unique _ λ i → idl _ - Constant-objects .F-∘ f g = sym $ coprods _ _ .unique _ λ i → + Constant-objects .F-id = coprods _ _ .unique _ λ i → idl _ + Constant-objects .F-∘ f g = coprods _ _ .unique _ λ i → pullr (coprods _ _ .commute) ∙ coprods _ _ .commute Const⊣Γ : Constant-objects ⊣ Hom-from _ *C @@ -161,6 +160,6 @@ module Consts (is-iso→is-equiv (iso (λ h → coprods _ _ .match h) (λ h → ext λ i → coprods _ _ .commute) - (λ x → sym (coprods _ _ .unique _ λ i → refl)))) + (λ x → coprods _ _ .unique _ λ i → refl))) (λ g h x → ext λ y → pullr (pullr (coprods _ _ .commute))) ``` diff --git a/src/Cat/Diagram/Coproduct/Indexed.lagda.md b/src/Cat/Diagram/Coproduct/Indexed.lagda.md index a604d99e7..cde79da84 100644 --- a/src/Cat/Diagram/Coproduct/Indexed.lagda.md +++ b/src/Cat/Diagram/Coproduct/Indexed.lagda.md @@ -39,21 +39,22 @@ record is-indexed-coproduct (F : Idx → C.Ob) (ι : ∀ i → C.Hom (F i) S) field match : ∀ {Y} → (∀ i → C.Hom (F i) Y) → C.Hom S Y commute : ∀ {i} {Y} {f : ∀ i → C.Hom (F i) Y} → match f C.∘ ι i ≡ f i - unique : ∀ {Y} {h : C.Hom S Y} (f : ∀ i → C.Hom (F i) Y) - → (∀ i → h C.∘ ι i ≡ f i) - → h ≡ match f + unique + : ∀ {Y} {h : C.Hom S Y} (f : ∀ i → C.Hom (F i) Y) + → (∀ i → h C.∘ ι i ≡ f i) + → match f ≡ h - eta : ∀ {Y} (h : C.Hom S Y) → h ≡ match (λ i → h C.∘ ι i) + eta : ∀ {Y} (h : C.Hom S Y) → match (λ i → h C.∘ ι i) ≡ h eta h = unique _ λ _ → refl unique₂ : ∀ {Y} {g h : C.Hom S Y} → (∀ i → g C.∘ ι i ≡ h C.∘ ι i) → g ≡ h - unique₂ {g = g} {h} eq = eta g ∙ ap match (funext eq) ∙ sym (eta h) + unique₂ {g = g} {h} eq = sym (eta g) ∙∙ ap match (funext eq) ∙∙ eta h hom-iso : ∀ {Y} → C.Hom S Y ≃ (∀ i → C.Hom (F i) Y) hom-iso = (λ z i → z C.∘ ι i) , is-iso→is-equiv λ where .is-iso.from → match .is-iso.rinv x → funext λ i → commute - .is-iso.linv x → sym (unique _ λ _ → refl) + .is-iso.linv x → unique _ λ _ → refl ``` A category $\cC$ **admits indexed coproducts** (of level $\ell$) if, @@ -104,7 +105,7 @@ is-indexed-coproduct-is-prop {Idx = Idx} {F} {ΣF} {ι} P Q = path where open is-indexed-coproduct p : ∀ {X} → (f : ∀ i → C.Hom (F i) X) → P .match f ≡ Q .match f - p f = Q .unique f (λ i → P .commute) + p f = P .unique f (λ i → Q .commute) path : P ≡ Q path i .match f = p f i @@ -112,10 +113,9 @@ is-indexed-coproduct-is-prop {Idx = Idx} {F} {ΣF} {ι} P Q = path where is-prop→pathp (λ i → C.Hom-set _ _ (p f i C.∘ ι idx) (f idx)) (P .commute) (Q .commute) i - path i .unique {h = h} f q = - is-prop→pathp (λ i → C.Hom-set _ _ h (p f i)) - (P .unique f q) - (Q .unique f q) i + path i .unique {h = h} f q = is-prop→pathp (λ i → C.Hom-set _ _ (p f i) h) + (P .unique f q) + (Q .unique f q) i module _ {ℓ'} {Idx : Type ℓ'} {F : Idx → C.Ob} {P P' : Indexed-coproduct F} where private @@ -213,9 +213,7 @@ is-indexed-coproduct-assoc {A = A} {B} {X} {ΣᵃΣᵇX = ΣᵃΣᵇX} {ιᵃ = Σᵃᵇ' : is-indexed-coproduct X ιᵃᵇ' Σᵃᵇ' .match f = ΣᵃΣᵇ .match λ a → Σᵇ a .match λ b → f (a , b) Σᵃᵇ' .commute = C.pulll (ΣᵃΣᵇ .commute) ∙ Σᵇ _ .commute - Σᵃᵇ' .unique {h = h} f p = - ΣᵃΣᵇ .unique _ λ a → - Σᵇ _ .unique _ λ b → + Σᵃᵇ' .unique {h = h} f p = ΣᵃΣᵇ .unique _ λ a → sym $ Σᵇ _ .unique _ λ b → sym (C.assoc _ _ _) ∙ p (a , b) ``` @@ -298,7 +296,7 @@ is-initial→is-disjoint-coproduct {F = F} {i = i} init = is-disjoint where is-coprod : is-indexed-coproduct F i is-coprod .match _ = init _ .centre is-coprod .commute {i = i} = absurd i - is-coprod .unique {h = h} f p i = init _ .paths h (~ i) + is-coprod .unique {h = h} f p = init _ .paths h open is-disjoint-coproduct is-disjoint : is-disjoint-coproduct F i diff --git a/src/Cat/Diagram/Equaliser.lagda.md b/src/Cat/Diagram/Equaliser.lagda.md index d6ff85f08..f13680cb3 100644 --- a/src/Cat/Diagram/Equaliser.lagda.md +++ b/src/Cat/Diagram/Equaliser.lagda.md @@ -38,7 +38,7 @@ right-hand-sides agree. unique : ∀ {F} {e' : Hom F A} {p : f ∘ e' ≡ g ∘ e'} {other : Hom F E} → equ ∘ other ≡ e' - → other ≡ universal p + → universal p ≡ other equal-∘ : f ∘ equ ∘ h ≡ g ∘ equ ∘ h equal-∘ {h = h} = @@ -51,7 +51,7 @@ right-hand-sides agree. → equ ∘ o1 ≡ e' → equ ∘ o2 ≡ e' → o1 ≡ o2 - unique₂ p q r = unique {p = p} q ∙ sym (unique r) + unique₂ p q r = sym (unique {p = p} q) ∙ unique r ``` We can visualise the situation using the commutative diagram below: @@ -74,8 +74,8 @@ its domain: ```agda record Equaliser (f g : Hom A B) : Type (o ⊔ ℓ) where field - {apex} : Ob - equ : Hom apex A + {apex} : Ob + equ : Hom apex A has-is-eq : is-equaliser f g equ open is-equaliser has-is-eq public @@ -137,7 +137,7 @@ by the identity map $\id : A \to A$. id-is-equaliser .is-equaliser.equal = refl id-is-equaliser .is-equaliser.universal {e' = e'} _ = e' id-is-equaliser .is-equaliser.factors = idl _ - id-is-equaliser .is-equaliser.unique p = sym (idl _) ∙ p + id-is-equaliser .is-equaliser.unique p = sym p ∙ idl _ ``` If $e : E \to A$ is an equaliser and an [[epimorphism]], then $e$ is diff --git a/src/Cat/Diagram/Equaliser/Joint.lagda.md b/src/Cat/Diagram/Equaliser/Joint.lagda.md index e3cf8b2c3..2f3458119 100644 --- a/src/Cat/Diagram/Equaliser/Joint.lagda.md +++ b/src/Cat/Diagram/Equaliser/Joint.lagda.md @@ -32,11 +32,13 @@ record is-joint-equaliser {ℓ'} {I : Type ℓ'} {E x y} (F : I → Hom x y) (eq field equal : ∀ {i j} → F i ∘ equ ≡ F j ∘ equ universal : ∀ {E'} {e' : Hom E' x} (eq : ∀ i j → F i ∘ e' ≡ F j ∘ e') → Hom E' E - factors : ∀ {E'} {e' : Hom E' x} {eq : ∀ i j → F i ∘ e' ≡ F j ∘ e'} → equ ∘ universal eq ≡ e' + factors + : ∀ {E'} {e' : Hom E' x} {eq : ∀ i j → F i ∘ e' ≡ F j ∘ e'} + → equ ∘ universal eq ≡ e' unique : ∀ {E'} {e' : Hom E' x} {eq : ∀ i j → F i ∘ e' ≡ F j ∘ e'} {o : Hom E' E} → equ ∘ o ≡ e' - → o ≡ universal eq + → universal eq ≡ o ``` diff --git a/src/Cat/Diagram/Exponential.lagda.md b/src/Cat/Diagram/Exponential.lagda.md index c6328f666..7c356f527 100644 --- a/src/Cat/Diagram/Exponential.lagda.md +++ b/src/Cat/Diagram/Exponential.lagda.md @@ -59,9 +59,10 @@ record is-exponential (B^A : Ob) (ev : Hom (B^A ⊗₀ A) B) : Type (o ⊔ ℓ) field ƛ : ∀ {Γ} (m : Hom (Γ ⊗₀ A) B) → Hom Γ B^A commutes : ∀ {Γ} (m : Hom (Γ ⊗₀ A) B) → ev ∘ ƛ m ⊗₁ id ≡ m - unique : ∀ {Γ} {m : Hom (Γ ⊗₀ _) _} m' - → ev ∘ m' ⊗₁ id ≡ m - → m' ≡ ƛ m + unique + : ∀ {Γ} {m : Hom (Γ ⊗₀ _) _} m' + → ev ∘ m' ⊗₁ id ≡ m + → ƛ m ≡ m' ``` The data above is an unpacked way of saying that the evaluation map @@ -77,20 +78,19 @@ structure. lambda-is-equiv : ∀ {C} → is-equiv (ƛ {C}) lambda-is-equiv = is-iso→is-equiv λ where .is-iso.from → unlambda - .is-iso.rinv x → sym (unique x refl) + .is-iso.rinv x → unique x refl .is-iso.linv x → commutes x ``` @@ -122,14 +122,14 @@ module _ where open is-exponential p : Path (∀ {C} m → Hom C B^A) (x .ƛ) (y .ƛ) - p i {C} m = y .unique (x .ƛ m) (x .commutes m) i + p i {C} m = x .unique (y .ƛ m) (y .commutes m) i q : x ≡ y q i .ƛ = p i q i .commutes m = is-prop→pathp (λ i → Hom-set _ _ (ev ∘ p i m ⊗₁ id) m) (x .commutes m) (y .commutes m) i q i .unique {m = m} m' q = - is-prop→pathp (λ i → Hom-set _ _ m' (p i m)) (x .unique m' q) (y .unique m' q) i + is-prop→pathp (λ i → Hom-set _ _ (p i m) m') (x .unique m' q) (y .unique m' q) i ``` --> @@ -168,33 +168,25 @@ closed category" to "CCC". module _ A B where open Exponential (has-exp A B) renaming (B^A to [_,_]) using () public unlambda-∘ : ∀ {a b c d} (α : Hom a [ c , d ]) (β : Hom b a) → unlambda (α ∘ β) ≡ unlambda α ∘ β ⊗₁ id - unlambda-∘ α β = sym (Equiv.adjunctl (ƛ , lambda-is-equiv) (sym (unique (α ∘ β) aux))) where + unlambda-∘ α β = sym (Equiv.adjunctl (ƛ , lambda-is-equiv) (unique (α ∘ β) aux)) where aux = ev ∘ (α ∘ β) ⊗₁ id ≡⟨ ap (λ x → ev ∘ (α ∘ β) ⊗₁ x) (sym $ idl id) ⟩ ev ∘ (α ∘ β) ⊗₁ (id ∘ id) ≡⟨ ap (ev ∘_) (×-functor .F-∘ (α , id) (β , id)) ⟩ ev ∘ α ⊗₁ id ∘ β ⊗₁ id ≡⟨ assoc _ _ _ ⟩ (ev ∘ α ⊗₁ id) ∘ β ⊗₁ id ∎ - ƛ-∘' : ∀ {a a' b b' c} (f : Hom (a ⊗₀ b) c) (g : Hom a' a) (h : Hom b' b) - → ƛ (f ∘ g ⊗₁ h) ≡ ƛ (ev ∘ id ⊗₁ h) ∘ ƛ f ∘ g - ƛ-∘' f g h = sym (unique _ aux) where - aux = - unlambda (ƛ (ev ∘ id ⊗₁ h) ∘ ƛ f ∘ g) - ≡⟨ unlambda-∘ (ƛ (ev ∘ id ⊗₁ h)) (ƛ f ∘ g) ⟩ - unlambda (ƛ (ev ∘ id ⊗₁ h)) ∘ (ƛ f ∘ g) ⊗₁ id - ≡⟨ pushl (commutes _) ⟩ - ev ∘ id ⊗₁ h ∘ (ƛ f ∘ g) ⊗₁ id - ≡⟨ ap (ev ∘_) (sym (×-functor .F-∘ (id , h) (ƛ f ∘ g , id))) ⟩ - ev ∘ (id ∘ (ƛ f ∘ g)) ⊗₁ (h ∘ id) - ≡⟨ (λ i → ev ∘ idl (ƛ f ∘ g) i ⊗₁ idr h i) ⟩ - ev ∘ (ƛ f ∘ g) ⊗₁ h - ≡⟨ (λ i → ev ∘ (ƛ f ∘ g) ⊗₁ idl h (~ i)) ⟩ - ev ∘ (ƛ f ∘ g) ⊗₁ (id ∘ h) - ≡⟨ ap (ev ∘_) (×-functor .F-∘ (ƛ f , id) (g , h)) ⟩ - ev ∘ (ƛ f ⊗₁ id) ∘ (g ⊗₁ h) - ≡⟨ pulll (commutes _) ⟩ - f ∘ g ⊗₁ h - ∎ + ƛ-∘' + : ∀ {a a' b b' c} (f : Hom (a ⊗₀ b) c) (g : Hom a' a) (h : Hom b' b) + → ƛ (f ∘ g ⊗₁ h) ≡ ƛ (ev ∘ id ⊗₁ h) ∘ ƛ f ∘ g + ƛ-∘' f g h = unique _ $ + unlambda (ƛ (ev ∘ id ⊗₁ h) ∘ ƛ f ∘ g) ≡⟨ unlambda-∘ (ƛ (ev ∘ id ⊗₁ h)) (ƛ f ∘ g) ⟩ + unlambda (ƛ (ev ∘ id ⊗₁ h)) ∘ (ƛ f ∘ g) ⊗₁ id ≡⟨ pushl (commutes _) ⟩ + ev ∘ id ⊗₁ h ∘ (ƛ f ∘ g) ⊗₁ id ≡⟨ ap (ev ∘_) (sym (×-functor .F-∘ (id , h) (ƛ f ∘ g , id))) ⟩ + ev ∘ (id ∘ (ƛ f ∘ g)) ⊗₁ (h ∘ id) ≡⟨ (λ i → ev ∘ idl (ƛ f ∘ g) i ⊗₁ idr h i) ⟩ + ev ∘ (ƛ f ∘ g) ⊗₁ h ≡⟨ (λ i → ev ∘ (ƛ f ∘ g) ⊗₁ idl h (~ i)) ⟩ + ev ∘ (ƛ f ∘ g) ⊗₁ (id ∘ h) ≡⟨ ap (ev ∘_) (×-functor .F-∘ (ƛ f , id) (g , h)) ⟩ + ev ∘ (ƛ f ⊗₁ id) ∘ (g ⊗₁ h) ≡⟨ pulll (commutes _) ⟩ + f ∘ g ⊗₁ h ∎ ƛ-∘-idl : ∀ {a b b' c} (f : Hom (a ⊗₀ b) c) (h : Hom b' b) @@ -250,7 +242,7 @@ closed category" to "CCC". : ∀ {A B C X A^X B^X} {evA : Hom (A^X ⊗₀ X) A} {evB : Hom (B^X ⊗₀ X) B} → {f : Hom A B} {g : Hom C A^X} → (exp : is-exponential B^X evB) - → exp .is-exponential.ƛ (f ∘ evA) ∘ g ≡ exp .is-exponential.ƛ (f ∘ evA ∘ g ⊗₁ id) + → exp .is-exponential.ƛ (f ∘ evA ∘ g ⊗₁ id) ≡ exp .is-exponential.ƛ (f ∘ evA) ∘ g ƛ-∘ exb = is-exponential.unique exb _ ( ap₂ _∘_ refl (ap₂ _⊗₁_ refl (sym (idl id)) ∙ ×-functor .F-∘ _ _) ∙ extendl (is-exponential.commutes exb _)) @@ -298,21 +290,21 @@ characterise $-^A$ as the [[right adjoint]] to $- \times A$. ```agda [-,-] .F-id = ƛ (id ∘ ev ∘ ⟨ π₁ , id ∘ π₂ ⟩) ≡⟨ ap ƛ (idl _ ∙ ap (ev ∘_) (sym (ap₂ ⟨_,_⟩ (idl _) refl))) ⟩ - ƛ (ev ∘ id ⊗₁ id) ≡˘⟨ unique id refl ⟩ + ƛ (ev ∘ id ⊗₁ id) ≡⟨ unique id refl ⟩ id ∎ - [-,-] .F-∘ (f , g) (f' , g') = sym $ unique _ $ + [-,-] .F-∘ (f , g) (f' , g') = unique _ $ ev ∘ ⟨ (ƛ (g ∘ ev ∘ ⟨ π₁ , f ∘ π₂ ⟩) ∘ ƛ (g' ∘ ev ∘ ⟨ π₁ , f' ∘ π₂ ⟩)) ∘ π₁ , id ∘ π₂ ⟩ ≡⟨ refl⟩∘⟨ ap₂ _⊗₁_ refl (introl refl) ∙ ×-functor .F-∘ _ _ ⟩ ev ∘ ƛ (g ∘ ev ∘ ⟨ π₁ , f ∘ π₂ ⟩) ⊗₁ id ∘ ƛ (g' ∘ ev ∘ ⟨ π₁ , f' ∘ π₂ ⟩) ⊗₁ id ≡⟨ pulll (commutes _) ⟩ (g ∘ ev ∘ ⟨ π₁ , f ∘ π₂ ⟩) ∘ ƛ (g' ∘ ev ∘ ⟨ π₁ , f' ∘ π₂ ⟩) ⊗₁ id ≡⟨ pullr (pullr (ap₂ _∘_ (ap₂ ⟨_,_⟩ (introl refl) refl) refl ∙ sym (Bifunctor.lrmap ×-bi _ _))) ⟩ g ∘ ev ∘ ƛ (g' ∘ ev ∘ ⟨ π₁ , f' ∘ π₂ ⟩) ⊗₁ id ∘ id ⊗₁ f ≡⟨ refl⟩∘⟨ pulll (commutes _) ⟩ - g ∘ (g' ∘ ev ∘ ⟨ π₁ , f' ∘ π₂ ⟩) ∘ id ⊗₁ f ≡⟨ pulll refl ∙ extendr (pullr (pullr (Product.unique (products _ _) (pulll π₁∘⟨⟩ ∙∙ π₁∘⟨⟩ ∙∙ idl _) (pulll π₂∘⟨⟩ ∙ extendr π₂∘⟨⟩)))) ⟩ + g ∘ (g' ∘ ev ∘ ⟨ π₁ , f' ∘ π₂ ⟩) ∘ id ⊗₁ f ≡⟨ pulll refl ∙ extendr (pullr (pullr (sym (Product.unique (products _ _) (pulll π₁∘⟨⟩ ∙∙ π₁∘⟨⟩ ∙∙ idl _) (pulll π₂∘⟨⟩ ∙ extendr π₂∘⟨⟩))))) ⟩ (g ∘ g') ∘ ev ∘ ⟨ π₁ , (f' ∘ f) ∘ π₂ ⟩ ∎ product⊣exponential : ∀ {A} → Bifunctor.Left ×-bi A ⊣ Bifunctor.Right (Curry [-,-]) A product⊣exponential {A} = hom-iso→adjoints ƛ lambda-is-equiv nat where - module _ {a b c d} (g : Hom a b) (h : Hom c d) (x : Hom (d ⊗₀ A) a) where + module _ {a b c d} (g : Hom a b) (h : Hom c d) (x : Hom (d ⊗₀ A) a) where abstract nat : ƛ (g ∘ x ∘ ⟨ h ∘ π₁ , id ∘ π₂ ⟩) ≡ ƛ (g ∘ ev ∘ ⟨ π₁ , id ∘ π₂ ⟩) ∘ ƛ x ∘ h - nat = sym $ unique _ $ + nat = unique _ $ ev ∘ (ƛ (g ∘ ev ∘ ⟨ π₁ , id ∘ π₂ ⟩) ∘ ƛ x ∘ h) ⊗₁ id ≡⟨ refl⟩∘⟨ ap₂ _⊗₁_ refl (introl refl) ∙ ×-functor .F-∘ _ _ ⟩ ev ∘ ƛ (g ∘ ev ∘ ⟨ π₁ , id ∘ π₂ ⟩) ⊗₁ id ∘ (ƛ x ∘ h) ⊗₁ id ≡⟨ pulll (commutes _) ⟩ (g ∘ ⌜ ev ∘ ⟨ π₁ , id ∘ π₂ ⟩ ⌝) ∘ (ƛ x ∘ h) ⊗₁ id ≡⟨ ap! (elimr (ap₂ ⟨_,_⟩ (introl refl) refl ∙ ×-functor .F-id)) ⟩ @@ -343,9 +335,8 @@ product-adjoint→cartesian-closed A→ adj = cc where exp A B .ev = adj A .ε B exp A B .has-is-exp .ƛ = L-adjunct (adj A) exp A B .has-is-exp .commutes m = R-L-adjunct (adj A) m - exp A B .has-is-exp .unique m' x = sym $ - Equiv.injective₂ (_ , R-adjunct-is-equiv (adj A)) - (R-L-adjunct (adj A) _) x + exp A B .has-is-exp .unique m' x = + Equiv.injective₂ (_ , R-adjunct-is-equiv (adj A)) (R-L-adjunct (adj A) _) x cc : Cartesian-closed cc .Cartesian-closed.has-exp = exp @@ -376,10 +367,10 @@ exponentiability of $B$ by a condition on the slice category $C/B$. -^B .F₀ = -^B₀ -^B .F₁ h = ƛ (h ∘ ev) -^B .F-id = ap ƛ (idl ev) ∙ lambda-ev _ - -^B .F-∘ f g = sym $ Exponential.unique (exp _) _ - ( ap₂ _∘_ refl (ap₂ _⊗₁_ refl (introl refl) ∙ ×-functor .F-∘ _ _) + -^B .F-∘ f g = Exponential.unique (exp _) _ $ + ap₂ _∘_ refl (ap₂ _⊗₁_ refl (introl refl) ∙ ×-functor .F-∘ _ _) ∙∙ pulll (Exponential.commutes (exp _) _) - ∙∙ extendr (Exponential.commutes (exp _) _)) + ∙∙ extendr (Exponential.commutes (exp _) _) ``` Recall the [[constant families]] functor $\Delta_B : \cC \to \cC/B$, @@ -412,9 +403,7 @@ that we can extend maps $h : X \to Y$ over $B$ to maps $\Pi_B(X) \to omit it from the page. ```agda - exponentiable→product - : has-pullbacks C - → Functor (Slice C B) C + exponentiable→product : has-pullbacks C → Functor (Slice C B) C exponentiable→product pb = f where f : Functor (Slice C B) C f .F₀ h = pb {B = top} (-^B .F₁ (h .map)) (ƛ π₂) .apex @@ -429,10 +418,10 @@ omit it from the page. @@ -516,7 +505,7 @@ $\Delta_B \dashv \Pi_B$ we've been chasing. nat : hom-iso-inv-natural {L = constant-family products} {R = exponentiable→product pb} (rem₁ _ .fst) nat g h x = ext $ rem₁ _ .fst (Π.₁ g ∘ x ∘ h) .map ≡⟨ rem₁-β _ _ ⟩ - app (pb _ _ .p₁ ∘ Π.₁ g ∘ x ∘ h) ≡⟨ ap app (pulll (pb _ _ .p₁∘universal ∙ ƛ-∘ {f = g .map} {g = pb _ _ .p₁} (has-is-exp _))) ⟩ + app (pb _ _ .p₁ ∘ Π.₁ g ∘ x ∘ h) ≡⟨ ap app (pulll (pb _ _ .p₁∘universal ∙ sym (ƛ-∘ {f = g .map} {g = pb _ _ .p₁} (has-is-exp _)))) ⟩ app (ƛ (g .map ∘ ev ∘ pb _ _ .p₁ ⊗₁ id) ∘ x ∘ h) ≡⟨ ap₂ _∘_ refl (ap₂ _⊗₁_ refl (sym (idl id)) ∙ ×-functor .F-∘ _ _) ∙ pulll refl ⟩ app (ƛ (g .map ∘ ev ∘ pb _ _ .p₁ ⊗₁ id)) ∘ (x ∘ h) ⊗₁ id ≡⟨ ap₂ _∘_ (Equiv.η (_ , lambda-is-equiv _) _) refl ⟩ (g .map ∘ ev ∘ pb _ _ .p₁ ⊗₁ id) ∘ (x ∘ h) ⊗₁ id ≡⟨ pullr (pullr (sym (×-functor .F-∘ _ _) ∙ ap₂ _⊗₁_ (assoc _ _ _) refl ∙ ×-functor .F-∘ _ _)) ⟩ diff --git a/src/Cat/Diagram/Limit/Base.lagda.md b/src/Cat/Diagram/Limit/Base.lagda.md index 269083a9f..f1133f887 100644 --- a/src/Cat/Diagram/Limit/Base.lagda.md +++ b/src/Cat/Diagram/Limit/Base.lagda.md @@ -255,7 +255,7 @@ the apex by a single, _unique_ universal morphism: → (p : ∀ {x y} (f : J.Hom x y) → F₁ f C.∘ eps x ≡ eps y) → (other : C.Hom x apex) → (∀ j → ψ j C.∘ other ≡ eps j) - → other ≡ universal eps p + → universal eps p ≡ other ``` @@ -304,8 +304,8 @@ other data we have been given: lim .σ α .η _ ≡˘⟨ C.idl _ ⟩ C.id C.∘ lim .σ α .η _ ∎ lim .σ-comm {β = β} = ext λ j → factors (β .η) _ - lim .σ-uniq {β = β} {σ' = σ'} p = ext λ _ → - sym $ unique (β .η) _ (σ' .η tt) (λ j → sym (p ηₚ j)) + lim .σ-uniq {β = β} {σ' = σ'} p = ext λ _ → unique (β .η) _ (σ' .η tt) λ j → + sym (p ηₚ j) ``` diff --git a/src/Cat/Diagram/Limit/Initial.lagda.md b/src/Cat/Diagram/Limit/Initial.lagda.md index 0dbd3780f..6647ef6f0 100644 --- a/src/Cat/Diagram/Limit/Initial.lagda.md +++ b/src/Cat/Diagram/Limit/Initial.lagda.md @@ -65,5 +65,5 @@ module _ {o ℓ} {C : Precategory o ℓ} (L : Initial C) where mk .commutes f = L.¡-unique₂ _ _ mk .universal eps x = eps L.bot mk .factors eps p = p _ - mk .unique eps p other x = introl (L.¡-unique₂ _ _) ∙ x L.bot + mk .unique eps p other x = sym (x L.bot) ∙ eliml (L.¡-unique₂ _ _) ``` diff --git a/src/Cat/Diagram/Limit/Isomorph.lagda.md b/src/Cat/Diagram/Limit/Isomorph.lagda.md index 33f93a2a6..612b22fc4 100644 --- a/src/Cat/Diagram/Limit/Isomorph.lagda.md +++ b/src/Cat/Diagram/Limit/Isomorph.lagda.md @@ -52,7 +52,7 @@ cone is limiting if and only if $f$ is [[invertible]]. ml .commutes _ = eliml (A .F-id) ml .universal eps' _ = inv.inv ∘ eps' tt ml .factors eps' _ = cancell inv.invl - ml .unique eps' _ other com = sym (lswizzle (sym (com tt)) inv.invr) + ml .unique eps' _ other com = lswizzle (sym (com tt)) inv.invr is-limit→is-iso : ∀ {A B : Functor ⊤Cat C} {eps : B F∘ !F => A} diff --git a/src/Cat/Diagram/Limit/Pullback.lagda.md b/src/Cat/Diagram/Limit/Pullback.lagda.md index 9f8ef261b..1ca43f3e4 100644 --- a/src/Cat/Diagram/Limit/Pullback.lagda.md +++ b/src/Cat/Diagram/Limit/Pullback.lagda.md @@ -58,7 +58,9 @@ Pullback→Terminal-cone {f = f} {g} pb = lim where lim .has⊤ cone .centre .com cs-a = pb.p₁∘universal lim .has⊤ cone .centre .com cs-b = pb.p₂∘universal lim .has⊤ cone .centre .com cs-c = pullr pb.p₁∘universal ∙ cone .commutes (lift tt) - lim .has⊤ cone .paths otherhom = Cone-hom-path _ (sym (pb.unique (otherhom .com _) (otherhom .com _))) + lim .has⊤ cone .paths otherhom = Cone-hom-path _ $ pb.unique + (otherhom .com _) + (otherhom .com _) Terminal-cone→Pullback : ∀ {x y} @@ -76,7 +78,7 @@ Terminal-cone→Pullback {F = F} lim = pb where pb .has-is-pb .p₁∘universal {p = p} = lim.has⊤ (Square→Cone _ _ p) .centre .com cs-a pb .has-is-pb .p₂∘universal {p = p} = lim.has⊤ (Square→Cone _ _ p) .centre .com cs-b pb .has-is-pb .unique {p₁' = p₁'} {p₂'} {p} {lim'} a b = - sym (ap map (lim.has⊤ (Square→Cone _ _ p) .paths other)) + ap map (lim.has⊤ (Square→Cone _ _ p) .paths other) where other : Cone-hom _ _ _ other .map = _ diff --git a/src/Cat/Diagram/Limit/Terminal.lagda.md b/src/Cat/Diagram/Limit/Terminal.lagda.md index 03dd049a6..5c615d63e 100644 --- a/src/Cat/Diagram/Limit/Terminal.lagda.md +++ b/src/Cat/Diagram/Limit/Terminal.lagda.md @@ -38,9 +38,11 @@ is-limit→is-terminal : ∀ {T : Ob} {eps : Const T => ¡F} → is-limit {C = C} ¡F T eps → is-terminal C T -is-limit→is-terminal lim Y = contr (lim.universal (λ ()) (λ ())) - (λ _ → sym (lim.unique _ _ _ λ ())) - where module lim = is-limit lim +is-limit→is-terminal lim Y = record where + module lim = is-limit lim + + centre = lim.universal (λ ()) (λ ()) + paths _ = lim.unique _ _ _ λ () is-terminal→is-limit : ∀ {T : Ob} {F : Functor ⊥Cat C} → is-terminal C T → is-limit {C = C} F T ¡nt is-terminal→is-limit {T} {F} term = to-is-limitp ml λ {} where @@ -50,7 +52,7 @@ is-terminal→is-limit {T} {F} term = to-is-limitp ml λ {} where ml .commutes () ml .universal _ _ = term _ .centre ml .factors {} - ml .unique _ _ _ _ = sym (term _ .paths _) + ml .unique _ _ _ _ = term _ .paths _ Limit→Terminal : Limit {C = C} ¡F → Terminal C Limit→Terminal lim .top = Limit.apex lim diff --git a/src/Cat/Diagram/Omega.lagda.md b/src/Cat/Diagram/Omega.lagda.md index 5d119921c..70cac6ffb 100644 --- a/src/Cat/Diagram/Omega.lagda.md +++ b/src/Cat/Diagram/Omega.lagda.md @@ -87,7 +87,7 @@ module _ {o ℓ} (C : Precategory o ℓ) where unique : ∀ {X} {m : Subobject X} {nm : Hom X Ω} → is-pullback-along C (m .map) nm (true .map) - → nm ≡ name m + → name m ≡ nm ``` ::: terminology @@ -183,7 +183,7 @@ $\Sub(A)$; so we have $$\name{m} = \name{h'^*\true} = h'$$. rem₁ : m ≡ h' ^* point→subobject tru rem₁ = Sub-is-category cat .to-path $ is-pullback-along→iso {m = m} {n = point→subobject tru} p - in sym (ap nm rem₁ ∙ invr _) + in ap nm rem₁ ∙ invr _ ``` @@ -138,13 +139,16 @@ module _ {o ℓ} {C : Precategory o ℓ} where is-pullback-is-prop {X = X} {Y = Y} {p₁ = p₁} {f} {p₂} {g} x y = q where open is-pullback p : Path (∀ {P'} {p₁' : Hom P' X} {p₂' : Hom P' Y} → f ∘ p₁' ≡ g ∘ p₂' → _) (x .universal) (y .universal) - p i sq = y .unique {p = sq} (x .p₁∘universal {p = sq}) (x .p₂∘universal) i + p i sq = x .unique {p = sq} (y .p₁∘universal {p = sq}) (y .p₂∘universal) i + q : x ≡ y q i .square = Hom-set _ _ _ _ (x .square) (y .square) i q i .universal = p i q i .p₁∘universal {p₁' = p₁'} {p = sq} = is-prop→pathp (λ i → Hom-set _ _ (p₁ ∘ p i sq) p₁') (x .p₁∘universal) (y .p₁∘universal) i q i .p₂∘universal {p = sq} = is-prop→pathp (λ i → Hom-set _ _ (p₂ ∘ p i sq) _) (x .p₂∘universal) (y .p₂∘universal) i - q i .unique {p = sq} {lim' = lim'} c₁ c₂ = is-prop→pathp (λ i → Hom-set _ _ lim' (p i sq)) (x .unique c₁ c₂) (y .unique c₁ c₂) i + q i .unique {p = sq} {lim' = lim'} c₁ c₂ = is-prop→pathp + (λ i → Hom-set _ _ (p i sq) lim') + (x .unique c₁ c₂) (y .unique c₁ c₂) i instance H-Level-is-pullback : ∀ {P} {p₁ : Hom P X} {f : Hom X Z} {p₂ : Hom P Y} {g : Hom Y Z} {n} → H-Level (is-pullback C p₁ f p₂ g) (suc n) @@ -282,7 +286,7 @@ observation. id-kp .universal {p₁' = p₁'} _ = p₁' id-kp .p₁∘universal = idl _ id-kp .p₂∘universal {p = p} = idl _ ∙ f-monic _ _ p - id-kp .unique p q = sym (idl _) ∙ p + id-kp .unique p q = sym p ∙ idl _ ``` Conversely, if $(\id, \id)$ is the kernel pair of $f$, then $f$ is @@ -363,7 +367,7 @@ it is the unique such map! id-kp .universal q = p ∘ p-kp .universal q id-kp .p₁∘universal {p = q} = idl _ ∙ p-kp .p₁∘universal id-kp .p₂∘universal {p = q} = idl _ ∙ p-kp .p₂∘universal - id-kp .unique q r = (sym (idl _)) ∙ q ∙ sym (p-kp .p₁∘universal) + id-kp .unique q r = p-kp .p₁∘universal ∙∙ sym q ∙∙ idl _ ``` # Categories with all pullbacks diff --git a/src/Cat/Diagram/Pullback/Properties.lagda.md b/src/Cat/Diagram/Pullback/Properties.lagda.md index a4becd713..6142532ee 100644 --- a/src/Cat/Diagram/Pullback/Properties.lagda.md +++ b/src/Cat/Diagram/Pullback/Properties.lagda.md @@ -48,7 +48,7 @@ Degenerate squares where two opposite sides are identities are pullbacks. id-is-pullback .universal {p₁' = p₁'} _ = p₁' id-is-pullback .p₁∘universal = idl _ id-is-pullback .p₂∘universal {p = p} = p ∙ idl _ - id-is-pullback .unique q r = sym (idl _) ∙ q + id-is-pullback .unique q r = sym q ∙ idl _ ``` ## Pasting law {defines="pasting-law-for-pullbacks"} @@ -183,7 +183,7 @@ then have a map $x \to a$, as we wanted. pb .p₁∘universal = pullr left.p₁∘universal ∙ right.p₁∘universal pb .p₂∘universal = left.p₂∘universal pb .unique {p₁' = P→c} {P→d} {p = p} {lim'} q r = - left.unique (right.unique (assoc _ _ _ ∙ q) s) r + left.unique (sym (right.unique (assoc _ _ _ ∙ q) s)) r where s : b→e ∘ a→b ∘ lim' ≡ d→e ∘ P→d s = @@ -216,7 +216,7 @@ is a monomorphism iff. the square below is a pullback. is-monic→is-pullback mono .universal {p₁' = p₁'} p = p₁' is-monic→is-pullback mono .p₁∘universal = idl _ is-monic→is-pullback mono .p₂∘universal {p = p} = idl _ ∙ mono _ _ p - is-monic→is-pullback mono .unique p q = introl refl ∙ p + is-monic→is-pullback mono .unique p q = sym p ∙ eliml refl is-pullback→is-monic : is-pullback C id f id f → is-monic f is-pullback→is-monic pb f g p = sym (pb .p₁∘universal {p = p}) ∙ pb .p₂∘universal @@ -302,7 +302,7 @@ A similar result holds for isomorphisms. inv→pb .p₁∘universal = pulll (rswizzle (sym (pb .p₁∘universal)) i.invl) ∙ pb .p₁∘universal inv→pb .p₂∘universal = pulll (rswizzle (sym (pb .p₂∘universal)) i.invl) ∙ pb .p₂∘universal inv→pb .unique p q = - sym (lswizzle (sym (pb .unique (pulll (pb .p₁∘universal) ∙ p) (pulll (pb .p₂∘universal) ∙ q))) i.invr) + lswizzle (pb .unique (pulll (pb .p₁∘universal) ∙ p) (pulll (pb .p₂∘universal) ∙ q)) i.invr pb→inv : is-pullback C p1' f p2' g → is-invertible (pb .universal sq) pb→inv pb' = make-invertible (pb' .universal (pb .square)) (unique₂ pb {p = pb .square} @@ -330,7 +330,7 @@ A similar result holds for isomorphisms. → is-pullback C (p1 ∘ _≅_.from i) f (p2 ∘ _≅_.from i) g is-pullback-iso i pb = Equiv.to (invertible≃pullback pb (extendl (pb .square))) - (subst is-invertible (pb .unique refl refl) (iso→invertible (i Iso⁻¹))) + (subst is-invertible (sym (pb .unique refl refl)) (iso→invertible (i Iso⁻¹))) is-pullback-iso' : ∀ {p p' x y z} {f : Hom x z} {g : Hom y z} {p1 : Hom p x} {p2 : Hom p y} diff --git a/src/Cat/Diagram/Pushout.lagda.md b/src/Cat/Diagram/Pushout.lagda.md index 4ca1ef718..ab7101968 100644 --- a/src/Cat/Diagram/Pushout.lagda.md +++ b/src/Cat/Diagram/Pushout.lagda.md @@ -66,17 +66,17 @@ of identifications required to make the aforementioned square commute. universal∘i₁ : {p : i₁' ∘ f ≡ i₂' ∘ g} → universal p ∘ i₁ ≡ i₁' universal∘i₂ : {p : i₁' ∘ f ≡ i₂' ∘ g} → universal p ∘ i₂ ≡ i₂' - unique : {p : i₁' ∘ f ≡ i₂' ∘ g} {colim' : Hom P Q} - → colim' ∘ i₁ ≡ i₁' - → colim' ∘ i₂ ≡ i₂' - → colim' ≡ universal p + unique + : {p : i₁' ∘ f ≡ i₂' ∘ g} {colim' : Hom P Q} + → colim' ∘ i₁ ≡ i₁' → colim' ∘ i₂ ≡ i₂' + → universal p ≡ colim' unique₂ : {p : i₁' ∘ f ≡ i₂' ∘ g} {colim' colim'' : Hom P Q} → colim' ∘ i₁ ≡ i₁' → colim' ∘ i₂ ≡ i₂' → colim'' ∘ i₁ ≡ i₁' → colim'' ∘ i₂ ≡ i₂' → colim' ≡ colim'' - unique₂ {p = o} p q r s = unique {p = o} p q ∙ sym (unique r s) + unique₂ {p = o} p q r s = sym (unique {p = o} p q) ∙ unique r s ``` We provide a convenient packaging of the pushout and the injection diff --git a/src/Cat/Diagram/Pushout/Properties.lagda.md b/src/Cat/Diagram/Pushout/Properties.lagda.md index 4e08b437a..b0f706a8e 100644 --- a/src/Cat/Diagram/Pushout/Properties.lagda.md +++ b/src/Cat/Diagram/Pushout/Properties.lagda.md @@ -43,7 +43,7 @@ $f : A \to B$ is an epimorphism iff. the square below is a pushout is-epic→is-pushout epi .universal {i₁' = i₁'} p = i₁' is-epic→is-pushout epi .universal∘i₁ = idr _ is-epic→is-pushout epi .universal∘i₂ {p = p} = idr _ ∙ epi _ _ p - is-epic→is-pushout epi .unique p q = intror refl ∙ p + is-epic→is-pushout epi .unique p q = sym p ∙ elimr refl is-pushout→is-epic : is-pushout C f id f id → is-epic f is-pushout→is-epic po g h p = sym (po .universal∘i₁ {p = p}) ∙ po .universal∘i₂ @@ -105,15 +105,19 @@ If $\iota_1=\iota_2$, then the identity is a pushout. injections-eq→id-is-pushout .universal∘i₂ = idr _ ∙ ap (_ ∘_) eq ∙ po .universal∘i₂ injections-eq→id-is-pushout .unique {a} {f'} {g'} {p = sq} {c} p₁ p₂ = - c ≡⟨ insertr i⁻¹∘i₁≡id ⟩ - (c ∘ i⁻¹) ∘ i₁ ≡⟨ po .unique {colim' = c ∘ i⁻¹} (pullr i⁻¹∘i₁≡id ∙ p₁) (pullr i⁻¹∘i₂≡id ∙ p₂) ⟩∘⟨refl ⟩ - po.universal sq ∘ i₁ ∎ - where i⁻¹ : Hom p y - i⁻¹ = universal po $ idl f ∙ sym (idl f) - i⁻¹∘i₁≡id : i⁻¹ ∘ i₁ ≡ id - i⁻¹∘i₁≡id = po.universal∘i₁ - i⁻¹∘i₂≡id : i⁻¹ ∘ i₂ ≡ id - i⁻¹∘i₂≡id = ap (i⁻¹ ∘_) (sym eq) ∙ i⁻¹∘i₁≡id + let + i⁻¹ : Hom p y + i⁻¹ = universal po $ idl f ∙ sym (idl f) + + i⁻¹∘i₁≡id : i⁻¹ ∘ i₁ ≡ id + i⁻¹∘i₁≡id = po.universal∘i₁ + + i⁻¹∘i₂≡id : i⁻¹ ∘ i₂ ≡ id + i⁻¹∘i₂≡id = ap (i⁻¹ ∘_) (sym eq) ∙ i⁻¹∘i₁≡id + in + po.universal sq ∘ i₁ ≡⟨ car (po .unique {colim' = c ∘ i⁻¹} (pullr i⁻¹∘i₁≡id ∙ p₁) (pullr i⁻¹∘i₂≡id ∙ p₂)) ⟩ + (c ∘ i⁻¹) ∘ i₁ ≡⟨ cancelr i⁻¹∘i₁≡id ⟩ + c ∎ injections-eq→is-epic : is-epic f injections-eq→is-epic = is-pushout→is-epic injections-eq→id-is-pushout diff --git a/src/Cat/Diagram/Separator.lagda.md b/src/Cat/Diagram/Separator.lagda.md index d4009061d..19b8484ca 100644 --- a/src/Cat/Diagram/Separator.lagda.md +++ b/src/Cat/Diagram/Separator.lagda.md @@ -287,13 +287,10 @@ This follows immediately from the universal property of equalisers! ```agda equ-invertible : is-invertible Eq.equ - equ-invertible = - f∘-conservative $ - is-equiv→is-invertible $ - is-iso→is-equiv $ iso - (λ e → Eq.universal (p e)) - (λ e → Eq.factors) - (λ h → sym (Eq.unique refl)) + equ-invertible = f∘-conservative $ is-equiv→is-invertible $ is-iso→is-equiv $ iso + (λ e → Eq.universal (p e)) + (λ e → Eq.factors) + (λ h → Eq.unique refl) ``` A similar line of argument lets us generalize this result to separating @@ -318,13 +315,11 @@ equalisers+jointly-conservative→separating-family module Eq = Equaliser (equalisers f g) equ-invertible : is-invertible Eq.equ - equ-invertible = - fᵢ∘-conservative λ i → - is-equiv→is-invertible $ - is-iso→is-equiv $ iso + equ-invertible = fᵢ∘-conservative λ i → + is-equiv→is-invertible $ is-iso→is-equiv $ iso (λ eᵢ → Eq.universal (p eᵢ)) (λ eᵢ → Eq.factors) - (λ h → sym (Eq.unique refl)) + (λ h → Eq.unique refl) ```
@@ -433,7 +428,7 @@ record is-dense-separator (s : Ob) : Type (o ⊔ ℓ) where → {eta : Hom s x → Hom s y} → (h : Hom x y) → (∀ (e : Hom s x) → h ∘ e ≡ eta e) - → h ≡ universal eta + → universal eta ≡ h ``` As the name suggests, dense separators are separators: this follows @@ -445,7 +440,7 @@ directly from the uniqueness of the universal map. → {f g : Hom x y} → (∀ (e : Hom s x) → f ∘ e ≡ g ∘ e) → f ≡ g - separate p = unique _ p ∙ sym (unique _ λ _ → refl) + separate p = sym (unique _ p) ∙ unique _ λ _ → refl ``` @@ -426,9 +424,9 @@ opaque (π*.commutesp (sym p ∙ sym (idl _ )) _)) (pulll[] _ (π*.commutesp id-comm _) ∙[] pullr[] _ (π*.commutesv _) - ∙[] π*.uniquep _ (idl _) (sym p ∙ sym (idl _)) _ - (pulll[] _ (π*.commutesp id-comm _ ) - ∙[] pullr[] _ (π*.commutesp (sym p) _))) + ∙[] symP (π*.uniquep _ (idl _) (sym p ∙ sym (idl _)) _ + ( pulll[] _ (π*.commutesp id-comm _) + ∙[] pullr[] _ (π*.commutesp (sym p) _)))) base-change-square-inv : ∀ {Γ Δ Θ Ψ : Ob} diff --git a/src/Cat/Displayed/Cartesian/Joint.lagda.md b/src/Cat/Displayed/Cartesian/Joint.lagda.md index db955f2c9..ce48efbfb 100644 --- a/src/Cat/Displayed/Cartesian/Joint.lagda.md +++ b/src/Cat/Displayed/Cartesian/Joint.lagda.md @@ -88,7 +88,7 @@ such that $f_{i} \circ \langle v , h_{i} \rangle = h_{i}$. → {hᵢ : ∀ ix → Hom[ uᵢ ix ∘ v ] x' (bᵢ' ix)} → (other : Hom[ v ] x' a') → (∀ ix → fᵢ ix ∘' other ≡ hᵢ ix) - → other ≡ universal v hᵢ + → universal v hᵢ ≡ other ``` @@ -248,11 +248,11 @@ empty-jointly-cartesian→codiscrete → ¬ Ix → is-jointly-cartesian uᵢ fᵢ → ∀ {x} (v : Hom x a) → (x' : Ob[ x ]) → is-contr (Hom[ v ] x' a') -empty-jointly-cartesian→codiscrete ¬ix fᵢ-cart v x' = - contr (fᵢ.universal v λ ix → absurd (¬ix ix)) λ other → - sym (fᵢ.unique other λ ix → absurd (¬ix ix)) - where - module fᵢ = is-jointly-cartesian fᵢ-cart +empty-jointly-cartesian→codiscrete ¬ix fᵢ-cart v x' = record where + module fᵢ = is-jointly-cartesian fᵢ-cart + + centre = fᵢ.universal v λ ix → absurd (¬ix ix) + paths other = fᵢ.unique other λ ix → absurd (¬ix ix) ``` In the other direction, let $f : \cE_{u}(A', B')$ be some map. @@ -354,7 +354,7 @@ jointly-cartesian-∘ {Ix = Ix} {uᵢⱼ = uᵢⱼ} {fᵢⱼ = fᵢⱼ} {vᵢ = ≡[]⟨ fᵢⱼ.commutesp i _ _ j ⟩ hᵢⱼ (i , j) ∎[] - fᵢⱼ∘gᵢ-cart .unique {hᵢ = hᵢⱼ} other p = gᵢ.unique other $ λ i → + fᵢⱼ∘gᵢ-cart .unique {hᵢ = hᵢⱼ} other p = gᵢ.unique other $ λ i → symP $ fᵢⱼ.uniquep i _ _ _ (gᵢ i ∘' other) λ j → begin fᵢⱼ i j ∘' gᵢ i ∘' other ≡[]⟨ assoc' (fᵢⱼ i j) (gᵢ i) other ⟩ (fᵢⱼ i j ∘' gᵢ i) ∘' other ≡[]⟨ p (i , j) ⟩ @@ -391,8 +391,7 @@ jointly-cartesian-cartesian-∘ {uᵢ = uᵢ} {fᵢ = fᵢ} {v = v} {g = g} fᵢ (fᵢ ix ∘' g) ∘' universal fᵢ∘g-cart w hᵢ ≡[]⟨ pullr[] _ (g.commutes w _) ⟩ fᵢ ix ∘' fᵢ.universal' (λ ix → assoc (uᵢ ix) v w) hᵢ ≡[]⟨ fᵢ.commutesp _ hᵢ ix ⟩ hᵢ ix ∎[] - fᵢ∘g-cart .unique other pᵢ = - g.unique other $ + fᵢ∘g-cart .unique other pᵢ = g.unique other $ symP $ fᵢ.uniquep _ _ _ (g ∘' other) λ ix → assoc' (fᵢ ix) g other ∙[] pᵢ ix ``` @@ -426,7 +425,7 @@ pointwise-cartesian-jointly-cartesian-∘ (fᵢ ix ∘' gᵢ ix) ∘' gᵢ.universal v (λ ix → fᵢ.universal' ix _ (hᵢ ix)) ≡[]⟨ pullr[] refl (gᵢ.commutes v _ ix) ⟩ fᵢ ix ∘' fᵢ.universal' ix _ (hᵢ ix) ≡[]⟨ fᵢ.commutesp ix (assoc (uᵢ ix) (vᵢ ix) v) (hᵢ ix) ⟩ hᵢ ix ∎[] - fᵢ∘gᵢ-cart .unique other p = gᵢ.unique other λ ix → fᵢ.uniquep ix _ _ _ + fᵢ∘gᵢ-cart .unique other p = gᵢ.unique other λ ix → symP $ fᵢ.uniquep ix _ _ _ (gᵢ ix ∘' other) (assoc' (fᵢ ix) (gᵢ ix) other ∙[] p ix) ``` @@ -471,7 +470,7 @@ jointly-cartesian-vertical-retraction-stable fᵢ' ix ∘' ϕ ∘' fᵢ.universal v hᵢ ≡[]⟨ pulll[] (idr (uᵢ ix)) (factor ix) ⟩ fᵢ ix ∘' fᵢ.universal v hᵢ ≡[]⟨ fᵢ.commutes v hᵢ ix ⟩ hᵢ ix ∎[] - fᵢ'-cart .is-jointly-cartesian.unique {v = v} {hᵢ = hᵢ} other p = begin[] + fᵢ'-cart .is-jointly-cartesian.unique {v = v} {hᵢ = hᵢ} other p = symP $ begin[] let unique-lemma : ∀ ix → fᵢ ix ∘' hom[ idl v ] (ϕ.section' ∘' other) ≡ hᵢ ix unique-lemma ix = begin[] @@ -481,7 +480,7 @@ jointly-cartesian-vertical-retraction-stable hᵢ ix ∎[] in other ≡[]⟨ introl[] _ ϕ.is-section' ⟩ - (ϕ ∘' ϕ.section') ∘' other ≡[]⟨ pullr[] _ (wrap (idl v) ∙[] fᵢ.unique _ unique-lemma) ⟩ + (ϕ ∘' ϕ.section') ∘' other ≡[]⟨ pullr[] _ (wrap (idl v) ∙[] sym (fᵢ.unique _ unique-lemma)) ⟩ ϕ ∘' fᵢ.universal v hᵢ ≡[]⟨ wrap (idl v) ⟩ hom[ idl v ] (ϕ ∘' fᵢ.universal v hᵢ) ∎[] ``` @@ -737,12 +736,14 @@ postcompose-equiv→jointly-cartesian {a = a} {uᵢ = uᵢ} fᵢ eqv = fᵢ-cart fᵢ-cart : is-jointly-cartesian uᵢ fᵢ fᵢ-cart .universal v hᵢ = eqv.from hᵢ fᵢ-cart .commutes v hᵢ ix = eqv.ε hᵢ ·ₚ ix - fᵢ-cart .unique {hᵢ = hᵢ} other p = sym (eqv.η other) ∙ ap eqv.from (ext p) + fᵢ-cart .unique {hᵢ = hᵢ} other p = ap eqv.from (sym (ext p)) ∙ eqv.η other jointly-cartesian→postcompose-equiv {uᵢ = uᵢ} {fᵢ = fᵢ} fᵢ-cart v x' .is-eqv hᵢ = - contr (fᵢ.universal v hᵢ , ext (fᵢ.commutes v hᵢ)) λ fib → - Σ-prop-pathp! (sym (fᵢ.unique (fib .fst) (λ ix → fib .snd ·ₚ ix))) - where module fᵢ = is-jointly-cartesian fᵢ-cart + record where + module fᵢ = is-jointly-cartesian fᵢ-cart + + centre = fᵢ.universal v hᵢ , ext (fᵢ.commutes v hᵢ) + paths fib = Σ-prop-pathp! $ fᵢ.unique (fib .fst) (λ ix → fib .snd ·ₚ ix) ``` @@ -843,6 +844,6 @@ spaces arising from lifts of empty families. : ∀ {x y : Ob} → {u : Hom x y} {x' : Ob[ x ]} → (other : Hom[ u ] x' (Codisc* y)) - → other ≡ codisc* u x' + → codisc* u x' ≡ other codisc*-unique other = π*.unique other (λ ()) ``` diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md index d9779e9dc..bee2d5711 100644 --- a/src/Cat/Displayed/Cartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cartesian/Weak.lagda.md @@ -73,10 +73,11 @@ record is-weak-cartesian field universal : ∀ {x'} → (g' : Hom[ f ] x' b') → Hom[ id ] x' a' commutes : ∀ {x'} → (g' : Hom[ f ] x' b') → f' ∘' universal g' ≡[ idr _ ] g' - unique : ∀ {x'} {g' : Hom[ f ] x' b'} - → (h' : Hom[ id ] x' a') - → f' ∘' h' ≡[ idr _ ] g' - → h' ≡ universal g' + unique + : ∀ {x'} {g' : Hom[ f ] x' b'} + → (h' : Hom[ id ] x' a') + → f' ∘' h' ≡[ idr _ ] g' + → universal g' ≡ h' open is-weak-cartesian ``` @@ -93,8 +94,8 @@ weak-cartesian-domain-unique → x' ≅↓ x'' weak-cartesian-domain-unique {f' = f'} {f'' = f''} f'-weak f''-weak = make-iso[ _ ] to* from* - (to-pathp[] $ unique f''-weak _ invl* ∙ (sym $ unique f''-weak _ (idr' f''))) - (to-pathp[] $ unique f'-weak _ invr* ∙ (sym $ unique f'-weak _ (idr' f'))) + (to-pathp[] $ sym (unique f''-weak _ invl*) ∙ unique f''-weak _ (idr' f'')) + (to-pathp[] $ sym (unique f'-weak _ invr*) ∙ unique f'-weak _ (idr' f')) where open is-weak-cartesian @@ -105,7 +106,7 @@ weak-cartesian-domain-unique {f' = f'} {f'' = f''} f'-weak f''-weak = invl* = to-pathp[] $ hom[] (f'' ∘' hom[] (to* ∘' from*)) ≡⟨ smashr _ _ ⟩ hom[] (f'' ∘' to* ∘' from*) ≡⟨ revive₁ {p = ap (_ ∘_) (idl _)} (pulll' (idr _) (f''-weak .commutes f')) ⟩ - hom[] (f' ∘' from*) ≡⟨ revive₁ (f'-weak .commutes f'') ⟩ + hom[] (f' ∘' from*) ≡⟨ revive₁ (f'-weak .commutes f'') ⟩ hom[] f'' ≡⟨ liberate _ ⟩ f'' ∎ @@ -176,9 +177,9 @@ postcompose-equiv→weak-cartesian f' eqv .universal h' = equiv→inverse eqv h' postcompose-equiv→weak-cartesian f' eqv .commutes h' = to-pathp[] $ equiv→counit eqv h' postcompose-equiv→weak-cartesian f' eqv .unique {g' = g'} m' p = - m' ≡˘⟨ equiv→unit eqv m' ⟩ - equiv→inverse eqv (hom[] (f' ∘' m')) ≡⟨ ap (equiv→inverse eqv) (from-pathp[] p) ⟩ - equiv→inverse eqv g' ∎ + equiv→inverse eqv g' ≡˘⟨ ap (equiv→inverse eqv) (from-pathp[] p) ⟩ + equiv→inverse eqv (hom[] (f' ∘' m')) ≡⟨ equiv→unit eqv _ ⟩ + m' ∎ weak-cartesian→postcompose-equiv : ∀ {x y x' x'' y'} {f : Hom x y} {f' : Hom[ f ] x' y'} @@ -187,7 +188,7 @@ weak-cartesian→postcompose-equiv weak-cartesian→postcompose-equiv wcart = is-iso→is-equiv $ iso (λ h' → wcart .universal h') (λ h' → from-pathp[] (wcart .commutes h')) - (λ h' → sym (wcart .unique _ (wrap (idr _)))) + (λ h' → wcart .unique _ (wrap (idr _))) ``` ## Weak cartesian lifts {defines=weak-cartesian-fibration} @@ -378,7 +379,7 @@ maps. ```agda - f*-cartesian .unique {u = u} {u' = u'} {m = m} {h' = h'} m' p = path where abstract + f*-cartesian .unique {u = u} {u' = u'} {m = m} {h' = h'} m' p = sym path where abstract universal-path : (π* f y' ∘' π* m (f ^* y')) ∘' π*.universal m' ≡[ idr (f ∘ m) ] h' universal-path = to-pathp[] $ hom[] ((π* f y' ∘' π* m (f ^* y')) ∘' π*.universal m') ≡˘⟨ assoc[] {p = ap (f ∘_) (idr m)} ⟩ @@ -391,7 +392,7 @@ maps. path = m' ≡˘⟨ from-pathp[] (π*.commutes m') ⟩ hom[] (π* m (f ^* y') ∘' π*.universal m') ≡⟨ reindex _ (idr m) ⟩ - hom[] (π* m (f ^* y') ∘' π*.universal m') ≡⟨ hom[]⟩⟨ ap (π* m (f ^* y') ∘'_) (f*∘m*.unique m h' _ universal-path) ⟩ + hom[] (π* m (f ^* y') ∘' π*.universal m') ≡˘⟨ hom[]⟩⟨ ap (π* m (f ^* y') ∘'_) (f*∘m*.unique m h' _ universal-path) ⟩ hom[] (π* m (f ^* y') ∘' f*∘m*.universal m h' h') ∎ ``` @@ -469,18 +470,17 @@ module _ (wfib : Weak-cartesian-fibration) where : ∀ {x y x' y'} → (f : Hom x y) → is-equiv (π*.universal {f = f} {y' = y'} {x'}) - weak-fibration→universal-is-equiv {y' = y'} f = is-iso→is-equiv $ - iso (λ f' → hom[ idr f ] (π* f y' ∘' f') ) - (λ f' → sym $ π*.unique f' (to-pathp[] refl)) - (λ f' → cancel _ _ (π*.commutes f')) + weak-fibration→universal-is-equiv {y' = y'} f = is-iso→is-equiv $ iso + (λ f' → hom[ idr f ] (π* f y' ∘' f') ) + (λ f' → π*.unique f' (to-pathp[] refl)) + (λ f' → cancel _ _ (π*.commutes f')) weak-fibration→vertical-equiv : ∀ {x y x' y'} → (f : Hom x y) → Hom[ f ] x' y' ≃ Hom[ id ] x' (f ^* y') weak-fibration→vertical-equiv {y' = y'} f = - π*.universal , - weak-fibration→universal-is-equiv f + π*.universal , weak-fibration→universal-is-equiv f ``` Furthermore, this equivalence can be extended into a natural isomorphism @@ -497,14 +497,11 @@ between $\cE_{u}(-,y')$ and $\cE_{x}(-,u^{*}(y'))$. mi : make-natural-iso (Hom-over-into ℰ u y') (Hom-into (Fibre ℰ x) (u ^* y')) mi .eta x u' = π*.universal u' mi .inv x v' = hom[ idr u ] (π* u y' ∘' v') - mi .eta∘inv x = funext λ v' → - sym $ π*.unique _ (to-pathp[] refl) - mi .inv∘eta x = funext λ u' → - from-pathp[] (π*.commutes _) - mi .natural x y v' = funext λ u' → - π*.unique _ $ to-pathp[] $ + mi .eta∘inv x = funext λ v' → π*.unique _ (to-pathp[] refl) + mi .inv∘eta x = funext λ u' → from-pathp[] (π*.commutes _) + mi .natural x y v' = funext λ u' → sym $ π*.unique _ $ to-pathp[] $ smashr _ _ - ∙ weave _ (ap (u ∘_) (idl id)) _ (pulll' _ (π*.commutes _)) + ∙ weave _ (ap (u ∘_) (idl id)) _ (pulll' _ (π*.commutes _)) ``` An *extremely* useful fact is that the converse is true: if there is some @@ -580,7 +577,7 @@ the equivalence is natural. from* (hom[] (id' ∘' to* g')) ≡⟨ ap from* idl[] ⟩ from* (to* g') ≡⟨ equiv→unit to-eqv g' ⟩ g' ∎ - f-lift .weak-cartesian .unique {g' = g'} h' p = + f-lift .weak-cartesian .unique {g' = g'} h' p = sym $ h' ≡˘⟨ idl[] {p = idl id} ⟩ hom[] (id' ∘' h') ≡˘⟨ hom[]⟩⟨ ap (_∘' h') (equiv→counit to-eqv id') ⟩ hom[] (to* (from* id') ∘' h') ≡˘⟨ from-pathp[]⁻ (natural (from* id') h') ⟩ @@ -632,15 +629,12 @@ module _ (fib : Cartesian-fibration) where (Hom-from (Fibre ℰ x) x' F∘ base-change u) mi .eta x u' = π*.universalv u' mi .inv x v' = hom[ idr u ] (π* u x ∘' v') - mi .eta∘inv x = funext λ v' → - sym $ π*.uniquev _ (to-pathp[] refl) - mi .inv∘eta x = funext λ u' → - from-pathp[] (π*.commutesv _) - mi .natural _ _ v' = funext λ u' → - π*.uniquep _ _ _ _ $ - Fib.pulllf (π*.commutesp id-comm _) - ∙[] pullr[] _ (π*.commutesv _) - ∙[] to-pathp[] refl + mi .eta∘inv x = funext λ v' → π*.uniquev _ (to-pathp[] refl) + mi .inv∘eta x = funext λ u' → from-pathp[] (π*.commutesv _) + mi .natural _ _ v' = funext λ u' → sym $ π*.uniquep _ _ _ _ $ + Fib.pulllf (π*.commutesp id-comm _) + ∙[] pullr[] _ (π*.commutesv _) + ∙[] to-pathp[] refl ``` @@ -393,7 +394,7 @@ sub-prop-correct ρ (s =ᵖ t) = exists ⟨ id , id ⟩ aye [ ⟨ ⟦ sub-tm ρ s ⟧ᵉ , ⟦ sub-tm ρ t ⟧ᵉ ⟩ ] ≡⟨ ap₂ _[_] refl (ap₂ ⟨_,_⟩ (sub-tm-correct ρ s) (sub-tm-correct ρ t)) ⟩ exists ⟨ id , id ⟩ aye [ ⟨ ⟦ s ⟧ᵉ ∘ ⟦ ρ ⟧ˢ , ⟦ t ⟧ᵉ ∘ ⟦ ρ ⟧ˢ ⟩ ] - ≡⟨ ap₂ _[_] refl (sym (⟨⟩∘ _)) ⟩ + ≡⟨ ap₂ _[_] refl (⟨⟩∘ _) ⟩ exists ⟨ id , id ⟩ aye [ ⟨ ⟦ s ⟧ᵉ , ⟦ t ⟧ᵉ ⟩ ∘ ⟦ ρ ⟧ˢ ] ≡⟨ sym (subst-∘ _ _) ⟩ (exists ⟨ id , id ⟩ aye [ ⟨ ⟦ s ⟧ᵉ , ⟦ t ⟧ᵉ ⟩ ]) [ ⟦ ρ ⟧ˢ ] @@ -598,7 +599,7 @@ too. ```agda =-refl : entails φ (t =ᵖ t) =-refl {t = t} = - π*.universal _ $ hom[ pulll (⟨⟩∘ _ ∙ ap₂ ⟨_,_⟩ (idl _) (idl _)) ] $ + π*.universal _ $ hom[ pulll (sym (⟨⟩∘ _) ∙ ap₂ ⟨_,_⟩ (idl _) (idl _)) ] $ ι! ⟨ id , id ⟩ aye ℙ.∘' π* _ _ ℙ.∘' subst-! ⟦ t ⟧ᵉ diff --git a/src/Cat/Displayed/GenericObject.lagda.md b/src/Cat/Displayed/GenericObject.lagda.md index b87f685a9..a78e191e2 100644 --- a/src/Cat/Displayed/GenericObject.lagda.md +++ b/src/Cat/Displayed/GenericObject.lagda.md @@ -139,11 +139,11 @@ complexity of this sentence is a bit high, so please refer to the code: hom[] ((π* _ _ ∘' viso.from' x') ∘' (viso.to' x' ∘' π*.universal _ _)) ≡⟨ weave _ _ refl (cancel-inner[] _ (viso.invr' x')) ⟩ hom[] (π* _ _ ∘' π*.universal _ _) ≡⟨ shiftl _ (π*.commutes _ _) ⟩ h' ∎ - gobj .classify-cartesian x' .is-cartesian.unique {m = m} {h' = h'} m' p = + gobj .classify-cartesian x' .is-cartesian.unique {m = m} {h' = h'} m' p = sym $ m' ≡⟨ shiftr (sym (idl _) ∙ sym (idl _)) (insertl' _ (viso.invl' x')) ⟩ hom[] (viso.to' x' ∘' viso.from' x' ∘' m') ≡⟨ reindex _ _ ∙ sym (hom[]-∙ (idl _) (idl _)) ∙ ap hom[] (unwhisker-r (idl _) (idl _)) ⟩ - hom[] (viso.to' x' ∘' ⌜ hom[ idl _ ] (viso.from' x' ∘' m') ⌝) ≡⟨ ap! (π*.unique _ (whisker-r _ ∙ assoc[] ∙ unwhisker-l (ap (_∘ m) (idr _)) _ ∙ p)) ⟩ - hom[] (viso.to' x' ∘' π*.universal _ h') ∎ + hom[] (viso.to' x' ∘' ⌜ hom[ idl _ ] (viso.from' x' ∘' m') ⌝) ≡˘⟨ ap¡ (π*.unique _ (whisker-r _ ∙ assoc[] ∙ unwhisker-l (ap (_∘ m) (idr _)) _ ∙ p)) ⟩ + hom[] (viso.to' x' ∘' π*.universal _ h') ∎ ``` --> diff --git a/src/Cat/Displayed/Instances/CT-Structure.lagda.md b/src/Cat/Displayed/Instances/CT-Structure.lagda.md index 341cd83ac..5dff6c3f0 100644 --- a/src/Cat/Displayed/Instances/CT-Structure.lagda.md +++ b/src/Cat/Displayed/Instances/CT-Structure.lagda.md @@ -112,10 +112,10 @@ Simple-ct-fibration ct u Y .x' = Y Simple-ct-fibration ct u Y .lifting = π₂ Simple-ct-fibration ct u Y .cartesian .universal _ h = h Simple-ct-fibration ct u Y .cartesian .commutes g h = π₂∘⟨⟩ -Simple-ct-fibration ct u Y .cartesian .unique {m = g} {h' = h} h' p = +Simple-ct-fibration ct u Y .cartesian .unique {m = g} {h' = h} h' p = sym $ h' ≡˘⟨ π₂∘⟨⟩ ⟩ π₂ ∘ ⟨ g ∘ π₁ , h' ⟩ ≡⟨ p ⟩ - h ∎ + h ∎ ``` # Embeddings diff --git a/src/Cat/Displayed/Instances/Chaotic.lagda.md b/src/Cat/Displayed/Instances/Chaotic.lagda.md index 69a60a25d..bec9016a5 100644 --- a/src/Cat/Displayed/Instances/Chaotic.lagda.md +++ b/src/Cat/Displayed/Instances/Chaotic.lagda.md @@ -62,25 +62,24 @@ chaotic-cartesian→is-iso cart = J.make-invertible (universal B.id J.id) (commutes B.id J.id) - (unique _ (J.cancell (commutes B.id J.id)) - ∙ sym (unique {m = B.id} J.id (J.idr _))) + ( sym (unique _ (J.cancell (commutes B.id J.id))) + ∙ unique {m = B.id} J.id (J.idr _)) where open is-cartesian cart is-iso→chaotic-cartesian : ∀ {x y x' y'} {f : B.Hom x y} {g : J.Hom x' y'} → J.is-invertible g → is-cartesian Chaotic f g -is-iso→chaotic-cartesian {f = f} {g = g} is-inv = cart - where - open J.is-invertible is-inv - open is-cartesian - - cart : is-cartesian Chaotic f g - cart .universal _ h = inv J.∘ h - cart .commutes _ h = J.cancell invl - cart .unique {h' = h} m p = - m ≡⟨ J.introl invr ⟩ - (inv J.∘ g) J.∘ m ≡⟨ J.pullr p ⟩ - inv J.∘ h ∎ +is-iso→chaotic-cartesian {f = f} {g = g} is-inv = cart where + open J.is-invertible is-inv + open is-cartesian + + cart : is-cartesian Chaotic f g + cart .universal _ h = inv J.∘ h + cart .commutes _ h = J.cancell invl + cart .unique {h' = h} m p = sym $ + m ≡⟨ J.introl invr ⟩ + (inv J.∘ g) J.∘ m ≡⟨ J.pullr p ⟩ + inv J.∘ h ∎ ``` This implies that the chaotic fibration is a fibration, as $\id$ is @@ -99,7 +98,7 @@ Chaotic-fibration f y = cart-lift where cart-lift .lifting = J.id cart-lift .cartesian .universal _ g = g cart-lift .cartesian .commutes _ g = J.idl g - cart-lift .cartesian .unique m p = sym (J.idl m) ∙ p + cart-lift .cartesian .unique m p = sym p ∙ J.idl m ``` We observe a similar situation for cocartesian morphisms. @@ -111,26 +110,25 @@ chaotic-cocartesian→is-iso chaotic-cocartesian→is-iso cocart = J.make-invertible (universal B.id J.id) - (unique _ (J.cancelr (commutes B.id J.id)) - ∙ sym (unique {m = B.id} J.id (J.idl _))) + ( sym (unique _ (J.cancelr (commutes B.id J.id))) + ∙ unique {m = B.id} J.id (J.idl _)) (commutes B.id J.id) where open is-cocartesian cocart is-iso→chaotic-cocartesian : ∀ {x y x' y'} {f : B.Hom x y} {g : J.Hom x' y'} → J.is-invertible g → is-cocartesian Chaotic f g -is-iso→chaotic-cocartesian {f = f} {g = g} is-inv = cocart - where - open J.is-invertible is-inv - open is-cocartesian +is-iso→chaotic-cocartesian {f = f} {g = g} is-inv = cocart where + open J.is-invertible is-inv + open is-cocartesian - cocart : is-cocartesian Chaotic f g - cocart .universal _ h = h J.∘ inv - cocart .commutes _ h = J.cancelr invr - cocart .unique {h' = h} m p = - m ≡⟨ J.intror invl ⟩ - m J.∘ g J.∘ inv ≡⟨ J.pulll p ⟩ - h J.∘ inv ∎ + cocart : is-cocartesian Chaotic f g + cocart .universal _ h = h J.∘ inv + cocart .commutes _ h = J.cancelr invr + cocart .unique {h' = h} m p = sym $ + m ≡⟨ J.intror invl ⟩ + m J.∘ g J.∘ inv ≡⟨ J.pulll p ⟩ + h J.∘ inv ∎ Chaotic-opfibration : Cocartesian-fibration Chaotic Chaotic-opfibration f x' = cocart-lift where @@ -142,7 +140,7 @@ Chaotic-opfibration f x' = cocart-lift where cocart-lift .lifting = J.id cocart-lift .cocartesian .universal _ g = g cocart-lift .cocartesian .commutes _ g = J.idr g - cocart-lift .cocartesian .unique m p = sym (J.idr m) ∙ p + cocart-lift .cocartesian .unique m p = sym p ∙ J.idr m ``` This implies that the chaotic bifibration actually lives up to its name. diff --git a/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md b/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md index 4486ce13d..a12089cd4 100644 --- a/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md +++ b/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md @@ -250,11 +250,9 @@ Commutivity and uniqueness follow from the fact that $f'$ is cartesian. map-tot' h' ∎[] cart .unique {x} {P} {m = m} {h' = h'} m' p = - Σ-path (Slice-pathp (sym (fam-square m' ∙ idl _))) $ - let - p = f'.unique _ $ from-pathp[]⁻ $ begin[] - f' ∘' hom[] (map-tot' m') ≡[]⟨ to-pathp[] (smashr _ (ap (f ∘_) (fam-square m' ∙ idl _)) ∙ reindex _ _) ⟩ - hom[] (f' ∘' map-tot' m') ≡[]⟨ ap map-tot' p ⟩ - map-tot' h' ∎[] - in sym (hom[]-is-subst _ _) ∙ p + Σ-pathp (Slice-pathp (fam-square m' ∙ idl _)) $ + f'.uniquep (ap map (ap fst p)) _ _ _ $ begin[] + f' ∘' map-tot' m' ≡[]⟨ wrap refl ⟩ + hom[] (f' ∘' map-tot' m') ≡[]⟨ ap map-tot' p ⟩ + map-tot' h' ∎[] ``` diff --git a/src/Cat/Displayed/Instances/Externalisation.lagda.md b/src/Cat/Displayed/Instances/Externalisation.lagda.md index 5c3200469..63b6f8ecd 100644 --- a/src/Cat/Displayed/Instances/Externalisation.lagda.md +++ b/src/Cat/Displayed/Instances/Externalisation.lagda.md @@ -152,15 +152,13 @@ internal-iso→cartesian {Γ} {Δ} {u} {x} {y} f f-inv = cart where cart : is-cartesian _ _ _ cart .universal {u' = u'} m h' = invi [ m ] ∘i adjusti refl (assoc y u m) h' - cart .commutes {u' = u'} m h' = - Internal-hom-path $ + cart .commutes {u' = u'} m h' = Internal-hom-path $ (f [ m ] ∘i invi [ m ] ∘i _) .ihom ≡⟨ ap ihom (pullli (sym (∘i-nat f invi m))) ⟩ (⌜ f ∘i invi ⌝ [ m ] ∘i _) .ihom ≡⟨ ap! f-inv.invli ⟩ (⌜ idi _ [ m ] ⌝ ∘i _) .ihom ≡⟨ ap! (idi-nat m) ⟩ (idi _ ∘i _) .ihom ≡⟨ ap ihom (idli _) ⟩ h' .ihom ∎ - cart .unique {u' = u'} {m = m} {h' = h'} m' p = - Internal-hom-path $ + cart .unique {u' = u'} {m = m} {h' = h'} m' p = sym $ Internal-hom-path $ m' .ihom ≡⟨ ap ihom (introli (Internal-hom-path (ap ihom (idi-nat m)))) ⟩ (⌜ idi _ [ m ] ⌝ ∘i m') .ihom ≡⟨ ap! (ap (λ e → e [ m ]) (sym (f-inv.invri)) ∙ ∘i-nat _ _ _) ⟩ ((invi [ m ] ∘i f [ m ]) ∘i m') .ihom ≡⟨ ap ihom (pullri (Internal-hom-path (ap ihom p))) ⟩ @@ -192,12 +190,11 @@ cartesian→internal-iso {Γ} {Δ} {u} {x} {y} f f-cart = f-inv where (f [ id ] ∘i universal id (idi _)) .ihom ≡⟨ ap ihom (commutes id (idi _)) ⟩ idi (y ∘ ⌜ u ∘ id ⌝) .ihom ≡⟨ ap! (idr _) ⟩ idi (y ∘ u) .ihom ∎ - f-inv .inversesi .invri = - Internal-hom-path $ - (f-inv .invi ∘i f) .ihom ≡⟨ ∘i-ihom refl refl (sym (idr _)) refl refl ⟩ - (adjusti _ _ (f-inv .invi) ∘i f) .ihom ≡⟨ ap ihom (unique (adjusti refl (sym (idr _)) (f-inv .invi) ∘i f) f∘f⁻¹∘f≡f*) ⟩ - universal id (adjusti _ _ f) .ihom ≡˘⟨ ap ihom (unique (adjusti refl (sym (idr _)) (idi _)) f∘id≡f*) ⟩ - idi x .ihom ∎ + f-inv .inversesi .invri = Internal-hom-path $ + (f-inv .invi ∘i f) .ihom ≡⟨ ∘i-ihom refl refl (sym (idr _)) refl refl ⟩ + (adjusti _ _ (f-inv .invi) ∘i f) .ihom ≡˘⟨ ap ihom (unique (adjusti refl (sym (idr _)) (f-inv .invi) ∘i f) f∘f⁻¹∘f≡f*) ⟩ + universal id (adjusti _ _ f) .ihom ≡⟨ ap ihom (unique (adjusti refl (sym (idr _)) (idi _)) f∘id≡f*) ⟩ + idi x .ihom ∎ ```
The right inverse case needs some nightmare re-adjustments. @@ -242,17 +239,16 @@ Externalisation-fibration u y = u-lift where u-lift .lifting = idi _ u-lift .cartesian .is-cartesian.universal m h' = adjusti refl (assoc _ _ _) h' - u-lift .cartesian .is-cartesian.commutes m h' = - Internal-hom-path $ - (⌜ idi _ [ m ] ⌝ ∘i _) .ihom ≡⟨ ap! (idi-nat m) ⟩ - (idi _ ∘i _) .ihom ≡⟨ ap ihom (idli _) ⟩ - h' .ihom ∎ + u-lift .cartesian .is-cartesian.commutes m h' = Internal-hom-path $ + (⌜ idi _ [ m ] ⌝ ∘i _) .ihom ≡⟨ ap! (idi-nat m) ⟩ + (idi _ ∘i _) .ihom ≡⟨ ap ihom (idli _) ⟩ + h' .ihom ∎ u-lift .cartesian .is-cartesian.unique {m = m} {h' = h'} m' p = - Internal-hom-path $ - m' .ihom ≡˘⟨ ap ihom (idli _) ⟩ - (⌜ idi _ ⌝ ∘i m') .ihom ≡⟨ ap! (sym (idi-nat m)) ⟩ - (idi _ [ m ] ∘i m') .ihom ≡⟨ ap ihom p ⟩ - h' .ihom ∎ + sym $ Internal-hom-path $ + m' .ihom ≡˘⟨ ap ihom (idli _) ⟩ + (⌜ idi _ ⌝ ∘i m') .ihom ≡⟨ ap! (sym (idi-nat m)) ⟩ + (idi _ [ m ] ∘i m') .ihom ≡⟨ ap ihom p ⟩ + h' .ihom ∎ ``` ## Generic objects @@ -289,17 +285,13 @@ some tedious calculations. ```agda small .has-generic-ob .classify-cartesian x' .universal m h' = adjusti refl (idl _) h' - small .has-generic-ob .classify-cartesian x' .commutes m h' = - Internal-hom-path $ - ∘i-ihom refl - (sym (idl _)) - (sym (assoc _ _ _)) - (ap ihom (idi-nat _) ∙ ap (λ ϕ → idi ϕ .ihom) (sym (idl _))) - refl - ∙ ap ihom (idli h') + small .has-generic-ob .classify-cartesian x' .commutes m h' = Internal-hom-path $ + ∘i-ihom refl (sym (idl _)) (sym (assoc _ _ _)) + (ap ihom (idi-nat _) ∙ ap (λ ϕ → idi ϕ .ihom) (sym (idl _))) refl + ∙ ap ihom (idli h') small .has-generic-ob .classify-cartesian x' .unique {m = m} m' p = - Internal-hom-path $ - sym (ap ihom (idli m')) + sym $ Internal-hom-path $ + sym (ap ihom (idli m')) ∙∙ ∘i-ihom refl refl (ap (_∘ m) (sym (idl _))) (sym (ap ihom (idi-nat m))) refl ∙∙ ap ihom p ``` diff --git a/src/Cat/Displayed/Instances/Family.lagda.md b/src/Cat/Displayed/Instances/Family.lagda.md index d8f65bc6d..6d0e5552d 100644 --- a/src/Cat/Displayed/Instances/Family.lagda.md +++ b/src/Cat/Displayed/Instances/Family.lagda.md @@ -86,7 +86,7 @@ Family-is-cartesian = iscart where → is-cartesian Family f λ _ → id cart f y' .universal m nt = nt cart f y' .commutes m h' = funext λ _ → idl _ - cart f y' .unique m' p = funext λ _ → introl refl ∙ happly p _ + cart f y' .unique m' p = funext λ _ → sym (p · _) ∙ eliml refl iscart : Cartesian-fibration Family iscart f y' .x' z = y' (f z) @@ -114,8 +114,8 @@ pointwise-iso→cartesian {fₓ = fₓ} fₓ-inv = fₓ-cart where fₓ-inv.inv (m x) ∘ h' x fₓ-cart .commutes m h' = funext λ x → cancell (fₓ-inv.invl (m x)) - fₓ-cart .unique {m = m} m' p = - funext λ x → introl (fₓ-inv.invr (m x)) ∙ pullr (happly p x) + fₓ-cart .unique {m = m} m' p = funext λ x → + pushr (sym p ·ₚ x) ∙ eliml (fₓ-inv.invr (m x)) ``` Showing the backwards direction requires using the usual trick of @@ -132,8 +132,8 @@ cartesian→pointwise-iso {X = X} {f = f} {P = P} {Q = Q} {fₓ = fₓ} fₓ-car make-invertible fₓ⁻¹ (happly (fₓ-cart.commutes _ _) x) - (happly (fₓ-cart.unique {u = X} (λ _ → fₓ⁻¹ ∘ fₓ x) (funext λ _ → cancell (happly (fₓ-cart.commutes _ _) x))) x ∙ - sym (happly (fₓ-cart.unique (λ _ → id) (funext λ _ → idr _)) x)) + ( sym (fₓ-cart.unique {u = X} (λ _ → fₓ⁻¹ ∘ fₓ x) (funext λ _ → cancell (happly (fₓ-cart.commutes _ _) x))) ·ₚ x + ∙ happly (fₓ-cart.unique (λ _ → id) (funext λ _ → idr _)) x) where module fₓ-cart = is-cartesian fₓ-cart @@ -302,10 +302,10 @@ the equivalence around. gsmall .has-generic-ob .classify-cartesian f .commutes m h' = funext λ _ → cancell (is-invertible.invr (counit-iso _)) gsmall .has-generic-ob .classify-cartesian f .unique {m = m} {h' = h'} m' p = - funext λ x → + funext λ x → sym $ m' x ≡⟨ introl (is-invertible.invl (counit-iso _)) ⟩ - (counit .η (f (m x)) ∘ counit⁻¹ .η (f (m x))) ∘ m' x ≡⟨ pullr (p $ₚ x) ⟩ - counit .η (f (m x)) ∘ h' x ∎ + (counit .η (f (m x)) ∘ counit⁻¹ .η (f (m x))) ∘ m' x ≡⟨ pullr (p ·ₚ x) ⟩ + counit .η (f (m x)) ∘ h' x ∎ ``` If $\cC$ is itself strict, then the set of objects of $\cC$ forms a @@ -323,8 +323,7 @@ Strict→Family-generic-object ob-set = gobj where gobj .classify' _ _ = id gobj .classify-cartesian _ .universal _ h' = h' gobj .classify-cartesian _ .commutes _ h' = funext λ _ → idl _ - gobj .classify-cartesian _ .unique m' p = funext λ x → - sym (idl _) ∙ p · x + gobj .classify-cartesian _ .unique m' p = funext λ x → sym (p · x) ∙ idl _ ``` ### Skeletal generic objects diff --git a/src/Cat/Displayed/Instances/Family/Properties.lagda.md b/src/Cat/Displayed/Instances/Family/Properties.lagda.md index a5e34f5c0..15e598f7a 100644 --- a/src/Cat/Displayed/Instances/Family/Properties.lagda.md +++ b/src/Cat/Displayed/Instances/Family/Properties.lagda.md @@ -72,8 +72,8 @@ up. total-prod .has-is-product' .π₂∘⟨⟩' = ext (λ k → π₂∘⟨⟩) total-prod .has-is-product' .unique' {a' = Zₖ} {p1 = p1} {p2 = p2} {other' = other'} p q i k = unique - (coe0→i (λ i → π₁ C.∘ other-line k i ≡ p i k) i refl) - (coe0→i (λ i → π₂ C.∘ other-line k i ≡ q i k) i refl) + (coe0→i (λ i → π₁ C.∘ other-line k i ≡ p i k) (~ i) refl) + (coe0→i (λ i → π₂ C.∘ other-line k i ≡ q i k) (~ i) refl) i where other-line : ∀ k i → C.Hom (Zₖ k) (Xᵢ×Yⱼ (p1 i k) (p2 i k)) diff --git a/src/Cat/Displayed/Instances/Gluing.lagda.md b/src/Cat/Displayed/Instances/Gluing.lagda.md index e97218580..191f888af 100644 --- a/src/Cat/Displayed/Instances/Gluing.lagda.md +++ b/src/Cat/Displayed/Instances/Gluing.lagda.md @@ -157,9 +157,9 @@ Gl-products {x} {y} a b = done module Gl-products where record { com = coh } where abstract coh : apx .map C.∘ C.⟨ f' .map , g' .map ⟩ ≡ F.₁ (D.⟨ f , g ⟩) C.∘ a' .map - coh = C.pullr (C.⟨⟩∘ _) ∙ sym (is.unique + coh = C.pullr (sym (C.⟨⟩∘ _)) ∙ is.unique (F.pulll D.π₁∘⟨⟩ ∙ sym (f' .com) ∙ sym (C.pullr C.π₁∘⟨⟩)) - (F.pulll D.π₂∘⟨⟩ ∙ sym (g' .com) ∙ sym (C.pullr C.π₂∘⟨⟩))) + (F.pulll D.π₂∘⟨⟩ ∙ sym (g' .com) ∙ sym (C.pullr C.π₂∘⟨⟩)) done .has-is-product' .π₁∘⟨⟩' = Slice-pathp C.π₁∘⟨⟩ done .has-is-product' .π₂∘⟨⟩' = Slice-pathp C.π₂∘⟨⟩ @@ -377,8 +377,8 @@ indeed an exponential transpose. done .has-is-exponential' .commutes' m = Slice-pathp comm1 where abstract comm1 : (Cλ.ev C.∘ (pb.p₂ C.⊗₁ C.id)) C.∘ (alpha.alpha m C.⊗₁ C.id) ≡ m .map comm1 = C.pullr (sym (Bifunctor.lmap-∘ (Curry C.×-functor) _ _)) - ∙∙ ap (Cλ.ev C.∘_) (ap₂ C._⊗₁_ pb.p₂∘universal refl) - ∙∙ Cλ.commutes _ + ∙∙ ap (Cλ.ev C.∘_) (ap₂ C._⊗₁_ pb.p₂∘universal refl) + ∙∙ Cλ.commutes _ done .has-is-exponential' .unique' {Γ' = Γ} {m = mβ} {m'β} {p} {m' = m} m' q = Slice-pathp (pb.unique coh₁ coh₂) @@ -389,12 +389,12 @@ indeed an exponential transpose. pb.p₁ C.∘ m' .map ≡⟨ m' .com ⟩ F.₁ (m'β) C.∘ Γ .map - ≡⟨ ap₂ C._∘_ (ap F.₁ (Dλ.unique _ p)) refl ⟩ + ≡˘⟨ ap₂ C._∘_ (ap F.₁ (Dλ.unique _ p)) refl ⟩ F.₁ (Dλ.ƛ mβ) C.∘ Γ .map ∎ coh₂ : pb.p₂ C.∘ m' .map ≡ Cλ.ƛ (m .map) - coh₂ = Cλ.unique _ $ + coh₂ = sym $ Cλ.unique _ $ Cλ.ev C.∘ (pb.p₂ C.∘ m' .map) C.⊗₁ C.id ≡⟨ ap₂ C._∘_ refl (Bifunctor.lmap-∘ (Curry C.×-functor) _ _) ⟩ Cλ.ev C.∘ pb.p₂ C.⊗₁ C.id C.∘ m' .map C.⊗₁ C.id diff --git a/src/Cat/Displayed/Instances/Lifting.lagda.md b/src/Cat/Displayed/Instances/Lifting.lagda.md index b76705c13..f1e18fe33 100644 --- a/src/Cat/Displayed/Instances/Lifting.lagda.md +++ b/src/Cat/Displayed/Instances/Lifting.lagda.md @@ -386,13 +386,13 @@ reindexing $G'$ pointwise. ```agda - G'* .F-id' = symP $ π*.uniquep _ _ _ _ $ begin + G'* .F-id' = π*.uniquep _ _ _ _ $ begin π* _ _ ∘' id' ≡[]⟨ idr' _ ⟩ π* _ _ ≡[]⟨ symP (idl' _) ⟩ id' ∘' π* _ _ ≡[]⟨ (λ i → G' .F-id' (~ i) ∘' π* (α .η _) (G' .F₀' _)) ⟩ G' .F₁' J.id ∘' π* _ _ ∎[] - G'* .F-∘' f g = symP $ π*.uniquep _ _ _ _ $ begin + G'* .F-∘' f g = π*.uniquep _ _ _ _ $ begin π* _ _ ∘' G'* .F₁' f ∘' G'* .F₁' g ≡[]⟨ pulll[] _ (π*.commutes _ _) ⟩ hom[] (G' .F₁' f ∘' π* _ _) ∘' G'* .F₁' g ≡[ ap (_∘ F.F₁ g) (α .is-natural _ _ _) ]⟨ to-pathp[]⁻ (whisker-l (sym (α .is-natural _ _ _))) ⟩ (G' .F₁' f ∘' π* _ _) ∘' G'* .F₁' g ≡[]⟨ pullr[] _ (π*.commutes _ _) ⟩ diff --git a/src/Cat/Displayed/Instances/Opposite.lagda.md b/src/Cat/Displayed/Instances/Opposite.lagda.md index 919bd6aaf..332f4a98f 100644 --- a/src/Cat/Displayed/Instances/Opposite.lagda.md +++ b/src/Cat/Displayed/Instances/Opposite.lagda.md @@ -382,7 +382,7 @@ Opposite-cartesian f y' = record ; cartesian = record { universal = λ m h → h ∘v γ← ; commutes = λ m h → ∘,-idl (h ∘v γ←) ∙ F.cancelr (^*-comp .F.invr) - ; unique = λ m h → sym (F.cancelr (^*-comp .F.invl)) ∙ ap (_∘v γ←) (sym (∘,-idl m) ∙ h) + ; unique = λ m h → ap (_∘v γ←) (sym h ∙ ∘,-idl m) ∙ F.cancelr (^*-comp .F.invl) } } ``` diff --git a/src/Cat/Displayed/Instances/Simple.lagda.md b/src/Cat/Displayed/Instances/Simple.lagda.md index 461772646..5ff56f98b 100644 --- a/src/Cat/Displayed/Instances/Simple.lagda.md +++ b/src/Cat/Displayed/Instances/Simple.lagda.md @@ -134,11 +134,11 @@ $\langle \pi_1 , f' \rangle$ is, in fact, an inverse. ```agda cart .commutes m h' = - f' ∘ ⟨ m ∘ π₁ , π₂ ∘ ⟨⟩-inv.inv ∘ ⟨ m ∘ π₁ , h' ⟩ ⟩ ≡˘⟨ ap₂ _∘_ refl (⟨⟩-unique (pulll (π₁-inv ⟨⟩-inv) ∙ π₁∘⟨⟩) refl) ⟩ + f' ∘ ⟨ m ∘ π₁ , π₂ ∘ ⟨⟩-inv.inv ∘ ⟨ m ∘ π₁ , h' ⟩ ⟩ ≡⟨ ap₂ _∘_ refl (⟨⟩-unique (pulll (π₁-inv ⟨⟩-inv) ∙ π₁∘⟨⟩) refl) ⟩ f' ∘ ⟨⟩-inv.inv ∘ ⟨ m ∘ π₁ , h' ⟩ ≡⟨ pulll (π₂-inv ⟨⟩-inv) ⟩ π₂ ∘ ⟨ m ∘ π₁ , h' ⟩ ≡⟨ π₂∘⟨⟩ ⟩ h' ∎ - cart .unique {m = m} {h' = h'} m' p = + cart .unique {m = m} {h' = h'} m' p = sym $ m' ≡˘⟨ π₂∘⟨⟩ ⟩ π₂ ∘ ⟨ m ∘ π₁ , m' ⟩ ≡⟨ ap₂ _∘_ refl (introl ⟨⟩-inv.invr) ⟩ π₂ ∘ (⟨⟩-inv.inv ∘ ⟨ π₁ , f' ⟩) ∘ ⟨ m ∘ π₁ , m' ⟩ ≡⟨ products! has-prods ⟩ @@ -236,8 +236,8 @@ see that $i \circ \langle \pi_1 , f' \rangle = \pi_2$. universal-π₂∘f' : universal id π₂ ∘ ⟨ π₁ , f' ⟩ ≡ π₂ universal-π₂∘f' = - universal id π₂ ∘ ⟨ π₁ , f' ⟩ ≡⟨ unique _ universal-π₂-unique ⟩ - universal id f' ≡˘⟨ unique _ (elimr (ap₂ ⟨_,_⟩ (idl _) refl ∙ ⟨⟩-η)) ⟩ + universal id π₂ ∘ ⟨ π₁ , f' ⟩ ≡˘⟨ unique _ universal-π₂-unique ⟩ + universal id f' ≡⟨ unique _ (elimr (ap₂ ⟨_,_⟩ (idl _) refl ∙ ⟨⟩-η)) ⟩ π₂ ∎ ``` @@ -276,7 +276,7 @@ Simple-fibration f Y .x' = Y Simple-fibration f Y .lifting = π₂ Simple-fibration f Y .cartesian .universal _ h = h Simple-fibration f Y .cartesian .commutes g h = π₂∘⟨⟩ -Simple-fibration f Y .cartesian .unique {m = g} {h' = h} h' p = +Simple-fibration f Y .cartesian .unique {m = g} {h' = h} h' p = sym $ h' ≡˘⟨ π₂∘⟨⟩ ⟩ π₂ ∘ ⟨ g ∘ π₁ , h' ⟩ ≡⟨ p ⟩ h ∎ @@ -353,15 +353,15 @@ tedious calculations, so we omit them. π₁ ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩ ≡⟨ π₁∘⟨⟩ ⟩ p₁' ∎ pb .p₂∘universal {P} {p₁'} {p₂'} {p} = - ⟨ f ∘ π₁ , f' ⟩ ∘ ⟨⟩-inv.inv ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩ ≡⟨ pulll (⟨⟩∘ _) ⟩ - ⟨ (f ∘ π₁) ∘ ⟨⟩-inv.inv , f' ∘ ⟨⟩-inv.inv ⟩ ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩ ≡⟨ ap₂ _∘_ (ap₂ ⟨_,_⟩ (pullr (π₁-inv ⟨⟩-inv)) (π₂-inv ⟨⟩-inv)) refl ⟩ + ⟨ f ∘ π₁ , f' ⟩ ∘ ⟨⟩-inv.inv ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩ ≡⟨ pulll (sym (⟨⟩∘ _)) ⟩ + ⟨ (f ∘ π₁) ∘ ⟨⟩-inv.inv , f' ∘ ⟨⟩-inv.inv ⟩ ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩ ≡⟨ car (ap₂ ⟨_,_⟩ (pullr (π₁-inv ⟨⟩-inv)) (π₂-inv ⟨⟩-inv)) ⟩ ⟨ f ∘ π₁ , π₂ ⟩ ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩ ≡⟨ products! has-prods ⟩ ⟨ f ∘ p₁' , π₂ ∘ p₂' ⟩ ≡⟨ ap₂ ⟨_,_⟩ p refl ⟩ ⟨ π₁ ∘ p₂' , π₂ ∘ p₂' ⟩ ≡⟨ products! has-prods ⟩ p₂' ∎ - pb .unique {P} {p₁'} {p₂'} {p} {h'} q r = + pb .unique {P} {p₁'} {p₂'} {p} {h'} q r = sym $ h' ≡⟨ insertl ⟨⟩-inv.invr ⟩ - ⟨⟩-inv.inv ∘ ⟨ π₁ , f' ⟩ ∘ h' ≡⟨ ap₂ _∘_ refl (⟨⟩∘ h') ⟩ + ⟨⟩-inv.inv ∘ ⟨ π₁ , f' ⟩ ∘ h' ≡˘⟨ cdr (⟨⟩∘ h') ⟩ ⟨⟩-inv.inv ∘ ⟨ ⌜ π₁ ∘ h' ⌝ , f' ∘ h' ⟩ ≡⟨ ap! q ⟩ ⟨⟩-inv.inv ∘ ⟨ p₁' , ⌜ f' ∘ h' ⌝ ⟩ ≡⟨ ap! (pushl (sym π₂∘⟨⟩)) ⟩ ⟨⟩-inv.inv ∘ ⟨ p₁' , π₂ ∘ ⌜ ⟨ f ∘ π₁ , f' ⟩ ∘ h' ⌝ ⟩ ≡⟨ ap! r ⟩ diff --git a/src/Cat/Displayed/Instances/Slice.lagda.md b/src/Cat/Displayed/Instances/Slice.lagda.md index b87c85f26..d77f2f29e 100644 --- a/src/Cat/Displayed/Instances/Slice.lagda.md +++ b/src/Cat/Displayed/Instances/Slice.lagda.md @@ -378,7 +378,7 @@ exactly those squares whose underlying top map is invertible. m ∘ y' .map ∘ f' .map ∘ inv.inv ≡⟨ (refl⟩∘⟨ elimr inv.invl) ⟩ m ∘ y' .map ∎ cocart .commutes m h' = Slice-path (cancelr inv.invr) - cocart .unique m' p = Slice-path (sym (rswizzle (sym (ap map p)) inv.invl)) + cocart .unique m' p = Slice-path (rswizzle (sym (ap map p)) inv.invl) ``` Given a map $f : X \to Y$ and an object $X' : \cB/X$, the cocartesian diff --git a/src/Cat/Displayed/Total.lagda.md b/src/Cat/Displayed/Total.lagda.md index 6d02812de..df95a5810 100644 --- a/src/Cat/Displayed/Total.lagda.md +++ b/src/Cat/Displayed/Total.lagda.md @@ -319,9 +319,9 @@ $g'$ are cartesian to construct the relevant paths. pb .p₂∘universal = ap fst $ total-pb .p₂∘universal pb .unique {p = p} q r = ap fst $ total-pb .unique (∫Hom-path q (p₁'.commutesp q _)) - (∫Hom-path r (g'.uniquep _ _ (sym $ p) _ - (pulll[] _ (symP $ ap snd (total-pb .square)) - ∙[] pullr[] _ (p₁'.commutesp q _)))) + (∫Hom-path r (symP (g'.uniquep _ _ (sym p) _ + ( pulll[] _ (symP $ ap snd (total-pb .square)) + ∙[] pullr[] _ (p₁'.commutesp q _))))) ``` @@ -435,7 +435,7 @@ the functor $\cD(X,U(-))$. fold-is-equiv : ∀ B → is-equiv (fold {B}) fold-is-equiv B = is-iso→is-equiv λ where .is-iso.from f → U.₁ f D.∘ unit - .is-iso.rinv _ → sym (unique _ refl) + .is-iso.rinv _ → unique _ refl .is-iso.linv _ → commute ``` @@ -486,12 +486,12 @@ so we will omit the details. folds : ∀ {Y} (f : D.Hom X (U.₀ Y)) → PathP (λ i → C.Hom (p i) Y) (x .fold f) (y .fold f) - folds {Y} f = to-pathp $ + folds {Y} f = to-pathp⁻ $ let - it : U.₁ (x .fold f) D.∘ x .unit - ≡ U.₁ (transport (λ i → C.Hom (p i) Y) (x .fold f)) D.∘ y .unit - it i = U.₁ (coe0→i (λ i → C.Hom (p i) Y) i (x .fold f)) D.∘ q i - in y .unique _ (sym it ∙ x .commute) + it : U.₁ (transport (λ i → C.Hom (p (~ i)) Y) (y .fold f)) D.∘ x .unit + ≡ U.₁ (y .fold f) D.∘ y .unit + it i = U.₁ (coe1→i (λ i → C.Hom (p i) Y) i (y .fold f)) D.∘ q i + in x .unique _ (it ∙ y .commute) r : x ≡ y r i .free = p i @@ -501,7 +501,7 @@ so we will omit the details. (λ i → D.Hom-set _ _ (U.₁ (folds f i) D.∘ q i) f) (x .commute) (y .commute) i r i .unique {Y = Y} {f} = is-prop→pathp (λ i → Π-is-hlevel² {A = C.Hom (p i) Y} {B = λ g → U.₁ g D.∘ q i ≡ f} 1 - λ g _ → C.Hom-set _ _ g (folds f i)) + λ g _ → C.Hom-set _ _ (folds f i) g) (x .unique) (y .unique) i instance @@ -538,8 +538,7 @@ equivalence, but it would not be very useful, either. free-object→universal-map fo = λ where .I.bot → ↓obj (fo .unit) .I.has⊥ x .centre → ↓hom (D.idr _ ∙ sym (fo .commute)) - .I.has⊥ x .paths p → ↓Hom-path _ _ refl $ sym $ - fo .unique _ (sym (p .com) ∙ D.idr _) + .I.has⊥ x .paths p → ↓Hom-path _ _ refl $ fo .unique _ (sym (p .com) ∙ D.idr _) ``` ### Free objects and adjoints @@ -563,7 +562,7 @@ even if a functor $F(-)$ does not necessarily exist. left-adjoint→free-objects X .fold f = R-adjunct F⊣U f left-adjoint→free-objects X .commute = L-R-adjunct F⊣U _ left-adjoint→free-objects X .unique g p = - Equiv.injective (_ , L-adjunct-is-equiv F⊣U) (p ∙ sym (L-R-adjunct F⊣U _)) + Equiv.injective (_ , L-adjunct-is-equiv F⊣U) (L-R-adjunct F⊣U _ ∙ sym p) ``` Conversely, if $\cD$ has all free objects, then $U$ has a left adjoint. @@ -715,8 +714,7 @@ $A$ is an initial object in $\cC$. : (F[⊥] : Free-object U init) → is-initial C (F[⊥] .free) free-on-initial→initial F[⊥] x .centre = F[⊥] .fold ¡ - free-on-initial→initial F[⊥] x .paths f = - sym $ F[⊥] .unique f (sym (¡-unique _)) + free-on-initial→initial F[⊥] x .paths f = F[⊥] .unique f (sym (¡-unique _)) ``` Conversely, if $\cC$ has an initial object $\bot_{\cC}$, then $\bot_{\cC}$ @@ -892,7 +890,7 @@ module _ {o h o' h'} {C : Precategory o h} {D : Precategory o' h'} where universal-map→free-object x .fold f = x .has⊥ (↓obj f) .centre .bot universal-map→free-object x .commute = sym (x .has⊥ _ .centre .com) ∙ C.idr _ universal-map→free-object x .unique g p = ap bot - (sym (x .has⊥ _ .paths (↓hom (sym (p ∙ sym (C.idr _)))))) + (x .has⊥ _ .paths (↓hom (sym (p ∙ sym (C.idr _))))) universal-maps→functor : ∀ {R} → (∀ X → Universal-morphism R X) → Functor C D universal-maps→functor u = free-objects→functor diff --git a/src/Cat/Functor/Adjoint/Cofree.lagda.md b/src/Cat/Functor/Adjoint/Cofree.lagda.md index fed637204..5038077c4 100644 --- a/src/Cat/Functor/Adjoint/Cofree.lagda.md +++ b/src/Cat/Functor/Adjoint/Cofree.lagda.md @@ -53,7 +53,7 @@ module _ (F : Functor C D) where unique : ∀ {Y} {f : D.Hom (F₀ Y) X} (g : C.Hom Y cofree) → counit D.∘ F₁ g ≡ f - → g ≡ unfold f + → unfold f ≡ g ``` diff --git a/src/Cat/Functor/Hom/Coyoneda.lagda.md b/src/Cat/Functor/Hom/Coyoneda.lagda.md index 0c3e96ff7..d23fe4b80 100644 --- a/src/Cat/Functor/Hom/Coyoneda.lagda.md +++ b/src/Cat/Functor/Hom/Coyoneda.lagda.md @@ -118,7 +118,7 @@ Finally, uniqueness: This just follows by the commuting conditions on `α`. ```agda - colim .unique eta comm α p = ext λ x px → + colim .unique eta comm α p = sym $ ext λ x px → α .η x px ≡˘⟨ ap (α .η x) (happly P.F-id px) ⟩ α .η x (P.F₁ id px) ≡⟨ happly (p _ ηₚ x) id ⟩ eta (elem x px) .η x id ∎ diff --git a/src/Cat/Functor/Kan/Pointwise.lagda.md b/src/Cat/Functor/Kan/Pointwise.lagda.md index d839d095c..338039625 100644 --- a/src/Cat/Functor/Kan/Pointwise.lagda.md +++ b/src/Cat/Functor/Kan/Pointwise.lagda.md @@ -221,15 +221,13 @@ constraints are satisfied. ``` @@ -283,7 +281,7 @@ properties of colimits. ```agda has-lan .σ-comm {M = M} = ext λ c → ↓colim.factors _ _ _ ∙ D.eliml (M .F-id) - has-lan .σ-uniq {M = M} {α = α} {σ' = σ'} p = ext λ c' → sym $ + has-lan .σ-uniq {M = M} {α = α} {σ' = σ'} p = ext λ c' → ↓colim.unique _ _ _ _ λ j → σ' .η c' D.∘ ↓colim.ψ c' j ≡⟨ ap (λ ϕ → σ' .η c' D.∘ ↓colim.ψ c' ϕ) (↓Obj-path _ _ refl refl (sym (C'.idr _))) ⟩ (σ' .η c' D.∘ ↓colim.ψ c' (↓obj (j .map C'.∘ C'.id))) ≡⟨ D.pushr (sym $ ↓colim.factors _ _ _) ⟩ @@ -391,8 +389,8 @@ up not being very interesting. mi .eta∘inv _ = E.idl _ mi .inv∘eta _ = E.idl _ mi .natural _ _ _ = - E.idr _ - ∙ H-↓colim.unique _ _ _ _ (λ j → pulll H (↓colim.factors _ _ _)) + E.idr _ + ∙ sym (H-↓colim.unique _ _ _ _ (λ j → pulll H (↓colim.factors _ _ _))) ∙ sym (E.idl _) module HF'-cohere = Isoⁿ HF'-cohere diff --git a/src/Cat/Functor/Monadic/Beck.lagda.md b/src/Cat/Functor/Monadic/Beck.lagda.md index fe50a53b4..95b27eeb2 100644 --- a/src/Cat/Functor/Monadic/Beck.lagda.md +++ b/src/Cat/Functor/Monadic/Beck.lagda.md @@ -177,7 +177,7 @@ from the algebra laws. (e' .fst C.∘ T.M₁ A.ν) C.∘ unit.η _ ≡˘⟨ ap fst p C.⟩∘⟨refl ⟩ (e' .fst C.∘ T.mult .η _) C.∘ unit.η _ ≡⟨ C.cancelr T.μ-unitl ⟩ e' .fst ∎ - algebra-is-coequaliser .unique {F = F} {e'} {p} {colim} q = ext $ sym $ + algebra-is-coequaliser .unique {F = F} {e'} {p} {colim} q = ext $ e' .fst C.∘ unit.η A ≡⟨ ap fst (sym q) C.⟩∘⟨refl ⟩ (colim .fst C.∘ A.ν) C.∘ unit.η A ≡⟨ C.cancelr A.ν-unit ⟩ colim .fst ∎ @@ -234,8 +234,8 @@ far $\cD$ is from being the category of $T$-algebras. has-coeq Y .coeq D.∘ F.₁ (Y .snd .ν) D.∘ F.₁ (T.M₁ (alg-map .fst)) ≡⟨ D.extendl (has-coeq Y .coequal) ⟩ has-coeq Y .coeq D.∘ ε _ D.∘ F.₁ (T.M₁ (alg-map .fst)) ≡⟨ D.pushr (counit.is-natural _ _ _) ⟩ (has-coeq Y .coeq D.∘ F.₁ (alg-map .fst)) D.∘ ε _ ∎ - Comparison-EM⁻¹ .F-id {X} = sym $ has-coeq X .unique (D.idl _ ∙ D.intror F.F-id) - Comparison-EM⁻¹ .F-∘ {X} f g = sym $ has-coeq X .unique $ + Comparison-EM⁻¹ .F-id {X} = has-coeq X .unique (D.idl _ ∙ D.intror F.F-id) + Comparison-EM⁻¹ .F-∘ {X} f g = has-coeq X .unique $ D.pullr (has-coeq X .factors) ∙∙ D.pulll (has-coeq _ .factors) ∙∙ F.pullr refl @@ -275,21 +275,19 @@ readers. G.₁ (has-coeq x .universal _ D.∘ has-coeq x .coeq) C.∘ T.unit .η (x .fst) ≡⟨ C.pushl (G.F-∘ _ _) ⟩ G.₁ (has-coeq x .universal _) C.∘ G.₁ (has-coeq x .coeq) C.∘ T.unit.η _ ∎ Comparison-EM⁻¹⊣Comparison-EM .counit .is-natural x y f = - has-coeq (F₀ (Comparison-EM F⊣G) x) .unique + sym (has-coeq (F₀ (Comparison-EM F⊣G) x) .unique {p = ap₂ D._∘_ (F⊣G .counit.is-natural _ _ _) refl ∙∙ D.pullr (F⊣G .counit.is-natural _ _ _) ∙∙ D.pulll (sym (F⊣G .counit.is-natural _ _ _))} - (D.pullr (has-coeq _ .factors) ∙ D.pulll (has-coeq _ .factors)) - ∙ sym (has-coeq _ .unique (D.pullr (has-coeq _ .factors) ∙ sym (F⊣G .counit.is-natural _ _ _))) - Comparison-EM⁻¹⊣Comparison-EM .zig = - unique₂ (has-coeq _) - (has-coeq _ .coequal) - (D.pullr (has-coeq _ .factors) - ∙ D.pulll (has-coeq _ .factors) - ∙ ap₂ D._∘_ refl (F.F-∘ _ _) - ∙ D.pulll (F⊣G .counit.is-natural _ _ _) - ∙ D.cancelr (F⊣G .zig)) - (D.idl _) + (D.pullr (has-coeq _ .factors) ∙ D.pulll (has-coeq _ .factors))) + ∙ has-coeq _ .unique (D.pullr (has-coeq _ .factors) ∙ sym (F⊣G .counit.is-natural _ _ _)) + Comparison-EM⁻¹⊣Comparison-EM .zig = unique₂ (has-coeq _) (has-coeq _ .coequal) + ( D.pullr (has-coeq _ .factors) + ∙ D.pulll (has-coeq _ .factors) + ∙ ap₂ D._∘_ refl (F.F-∘ _ _) + ∙ D.pulll (F⊣G .counit.is-natural _ _ _) + ∙ D.cancelr (F⊣G .zig)) + (D.idl _) Comparison-EM⁻¹⊣Comparison-EM .zag = ext $ G.pulll (has-coeq _ .factors) ∙ F⊣G .zag ``` diff --git a/src/Cat/Functor/Pullback.lagda.md b/src/Cat/Functor/Pullback.lagda.md index b863ac49b..03eceb02f 100644 --- a/src/Cat/Functor/Pullback.lagda.md +++ b/src/Cat/Functor/Pullback.lagda.md @@ -115,13 +115,13 @@ diagram below is a cone over $K' \to X \ot Y$. functorial, but the details are not particularly enlightening. ```agda - Base-change .F-id {x} = ext (sym (xpb.unique id-comm (idr _))) + Base-change .F-id {x} = ext (xpb.unique id-comm (idr _)) where module xpb = Pullback (pullbacks (x .map) f) Base-change .F-∘ {x} {y} {z} am bm = - ext (sym (zpb.unique + ext (zpb.unique (pulll zpb.p₁∘universal ∙ pullr ypb.p₁∘universal ∙ assoc _ _ _) - (pulll zpb.p₂∘universal ∙ ypb.p₂∘universal))) + (pulll zpb.p₂∘universal ∙ ypb.p₂∘universal)) where module ypb = Pullback (pullbacks (y .map) f) module zpb = Pullback (pullbacks (z .map) f) @@ -295,7 +295,7 @@ object of $(\cC/X)/f$, or [[in other words|iterated slice]] $\cC/Y$. eso .rinv (A , c) = Σ-pathp (/-Obj-path refl path) $ Coalgebra-on-pathp _ $ /-Hom-pathp _ _ - $ symP $ Hom-pathp-reflr C $ pb≡.unique i0 + $ symP $ Hom-pathp-reflr C $ sym $ pb≡.unique i0 (pulll (from-pathp-to' C _ λ i → pb≡.p₁ i) ∙ unext (c .ρ-counit)) (pulll (from-pathp-to' C _ λ i → pb≡.p₂ i)) where diff --git a/src/Cat/Instances/Assemblies/Colimits.lagda.md b/src/Cat/Instances/Assemblies/Colimits.lagda.md index f3381287b..04a489904 100644 --- a/src/Cat/Instances/Assemblies/Colimits.lagda.md +++ b/src/Cat/Instances/Assemblies/Colimits.lagda.md @@ -139,6 +139,6 @@ with precisely with the assumptions that $f$ and $g$ are tracked. Assembly-coproducts A B .has-is-coproduct .[]∘ι₁ = ext λ _ → refl Assembly-coproducts A B .has-is-coproduct .[]∘ι₂ = ext λ _ → refl Assembly-coproducts A B .has-is-coproduct .unique p q = ext λ where - (inl x) → ap map p · x - (inr x) → ap map q · x + (inl x) → sym p ·ₚ x + (inr x) → sym q ·ₚ x ``` diff --git a/src/Cat/Instances/Assemblies/Exponentials.lagda.md b/src/Cat/Instances/Assemblies/Exponentials.lagda.md index 132a9313d..c6143f92c 100644 --- a/src/Cat/Instances/Assemblies/Exponentials.lagda.md +++ b/src/Cat/Instances/Assemblies/Exponentials.lagda.md @@ -152,7 +152,7 @@ Assemblies-exp A B .B^A = A ⇒Asm B Assemblies-exp A B .ev = asm-ev Assemblies-exp A B .has-is-exp .ƛ = curry-asm Assemblies-exp A B .has-is-exp .commutes m = ext λ x y → refl -Assemblies-exp A B .has-is-exp .unique m' p = ext λ x y → ap map p · (x , y) +Assemblies-exp A B .has-is-exp .unique m' p = ext λ x y → sym p ·ₚ (x , y) Assemblies-cc : Cartesian-closed (Assemblies 𝔸 ℓA) _ Assemblies-cc = record { has-exp = Assemblies-exp } diff --git a/src/Cat/Instances/Assemblies/Limits.lagda.md b/src/Cat/Instances/Assemblies/Limits.lagda.md index 3cf7e0910..0ff0853cd 100644 --- a/src/Cat/Instances/Assemblies/Limits.lagda.md +++ b/src/Cat/Instances/Assemblies/Limits.lagda.md @@ -133,7 +133,8 @@ Assemblies-products X Y .π₂ = π₂Asm Assemblies-products X Y .has-is-product .⟨_,_⟩ f g = ⟨ f , g ⟩Asm Assemblies-products X Y .has-is-product .π₁∘⟨⟩ = ext λ _ → refl Assemblies-products X Y .has-is-product .π₂∘⟨⟩ = ext λ _ → refl -Assemblies-products X Y .has-is-product .unique p q = ext λ a → p ·ₚ a ,ₚ q ·ₚ a +Assemblies-products X Y .has-is-product .unique p q = ext λ a → + sym p ·ₚ a ,ₚ sym q ·ₚ a ``` --> @@ -208,7 +209,7 @@ Assemblies-equalisers f g .has-is-eq .universal {e' = e'} p = inc record { [_]_⊢_ et } Assemblies-equalisers f g .has-is-eq .factors = ext λ _ → refl -Assemblies-equalisers f g .has-is-eq .unique p = ext λ a → Σ-prop-path! (p ·ₚ a) +Assemblies-equalisers f g .has-is-eq .unique p = ext λ a → Σ-prop-path! (sym p ·ₚ a) Assemblies-finite-limits : Finitely-complete (Assemblies 𝔸 ℓ) Assemblies-finite-limits = with-equalisers _ diff --git a/src/Cat/Instances/Coalgebras/Cartesian.lagda.md b/src/Cat/Instances/Coalgebras/Cartesian.lagda.md index 811e0fd26..1c49831c6 100644 --- a/src/Cat/Instances/Coalgebras/Cartesian.lagda.md +++ b/src/Cat/Instances/Coalgebras/Cartesian.lagda.md @@ -225,9 +225,9 @@ so $\nu$ was indeed the map we were looking for! pb' .universal {p₁' = p₁'} {p₂'} x = factor p₁' p₂' (ap fst x) pb' .p₁∘universal {p₁' = p₁'} {p₂'} {p} = ext $ comm₁ p₁' p₂' (ap fst p) pb' .p₂∘universal {p₁' = p₁'} {p₂'} {p} = ext $ comm₂ p₁' p₂' (ap fst p) - pb' .unique {p₁' = p₁'} {p₂'} {p} q r = ext $ p.unique₂ - {p = ap fst p} (ap fst q) (ap fst r) + pb' .unique {p₁' = p₁'} {p₂'} {p} q r = ext $ p.unique₂ {p = ap fst p} (comm₁ p₁' p₂' (ap fst p)) (comm₂ p₁' p₂' (ap fst p)) + (ap fst q) (ap fst r) ``` ```agda diff --git a/src/Cat/Instances/Coalgebras/Limits.lagda.md b/src/Cat/Instances/Coalgebras/Limits.lagda.md index 337ebf85b..c3baed3d5 100644 --- a/src/Cat/Instances/Coalgebras/Limits.lagda.md +++ b/src/Cat/Instances/Coalgebras/Limits.lagda.md @@ -150,7 +150,7 @@ commutativity condition we remarked was sufficient above; we're done! (λ j → pulll (phi .η j .snd) ∙ pullr (ν-β eta nat)) mk .factors eta nat = ext (ν-β eta nat) mk .unique eta nat other comm = ext (l.unique₂ _ - (λ f → ap fst (nat f)) (λ j → ap fst (comm j)) (λ j → ν-β eta nat)) + (λ f → ap fst (nat f)) (λ j → ν-β eta nat) (λ j → ap fst (comm j))) abstract fixup : ∀ {j} → mk .ψ j ≡ phi .η j diff --git a/src/Cat/Instances/Comma/Limits.lagda.md b/src/Cat/Instances/Comma/Limits.lagda.md index 2c5d27253..74eabc5d9 100644 --- a/src/Cat/Instances/Comma/Limits.lagda.md +++ b/src/Cat/Instances/Comma/Limits.lagda.md @@ -87,7 +87,8 @@ F$ into $L$ componentwise, and these satisfy the universal property. lim' .commutes f = ext (sym (limf.eps .is-natural _ _ _) ∙ C.elimr limf.Ext.F-id) lim' .universal eta p .top = tt lim' .universal eta p .bot = limf.universal (λ j → eta j .bot) λ f → ap bot (p f) - lim' .universal eta p .com = D.elimr refl ∙ sym (flimf.unique _ _ _ λ j → F.pulll (limf.factors _ _) ∙ sym (eta j .com) ∙ D.elimr refl) + lim' .universal eta p .com = D.elimr refl ∙ flimf.unique _ _ _ λ j → + F.pulll (limf.factors _ _) ∙ sym (eta j .com) ∙ D.elimr refl lim' .factors eta p = ext (limf.factors _ _) lim' .unique eta p other q = ext (limf.unique _ _ _ λ j → ap bot (q j)) ``` diff --git a/src/Cat/Instances/FinSets/Omega.lagda.md b/src/Cat/Instances/FinSets/Omega.lagda.md index 0dfcc0b1d..512328831 100644 --- a/src/Cat/Instances/FinSets/Omega.lagda.md +++ b/src/Cat/Instances/FinSets/Omega.lagda.md @@ -82,7 +82,7 @@ FinSets-omega .Subobject-classifier.generic .classifies m = record { top = λ _ fb .is-pullback.universal α x = from-name m _ (happly α x) .fst fb .is-pullback.p₁∘universal = ext λ a → from-name m _ _ .snd fb .is-pullback.p₂∘universal {p₂' = p₂'} = ext λ a → Fin-cases {P = λ x → 0 ≡ x} refl (λ ()) (p₂' a) - fb .is-pullback.unique a e = ext λ x → inj m (happly a x ∙ sym (from-name m _ _ .snd)) + fb .is-pullback.unique a e = ext λ x → inj m (from-name m _ _ .snd ∙ sym a ·ₚ x) ``` We can show uniqueness also by cases on the cardinality of each fibre. @@ -90,7 +90,7 @@ First, if the fibre is inhabited, then let $x'$ be the preimage of $x$; we then have $n(x) = n(mx') = 1$ as needed. ```agda -FinSets-omega .Subobject-classifier.generic .unique {m = m} {nm} pb = ext uniq where +FinSets-omega .Subobject-classifier.generic .unique {m = m} {nm} pb = sym $ ext uniq where uniq : ∀ x → nm x ≡ fin-name m x uniq x with cardinality {A = fibre (m .map) x} | enumeration {A = fibre (m .map) x} | from-name m x ... | suc n | e | f with (x' , α) ← f refl = ap nm (sym α) ∙ happly (pb .square) _ diff --git a/src/Cat/Instances/Free.lagda.md b/src/Cat/Instances/Free.lagda.md index 923ea6d73..abebde3cc 100644 --- a/src/Cat/Instances/Free.lagda.md +++ b/src/Cat/Instances/Free.lagda.md @@ -435,8 +435,8 @@ Free-category G .Free-object.commute {Y = C} {f = f} = where open Precategory (C .fst) Free-category G .Free-object.unique {Y = C} {f} F p = Path-category-functor-path - (λ x i → p i .node x) - (λ e → to-pathp (from-pathp (λ i → p i .edge e) ∙ sym (idl _))) + (λ x i → p (~ i) .node x) + (λ e → to-pathp (ap (subst₂ Hom _ _) (idl _) ∙ from-pathp (λ i → p (~ i) .edge e))) where open Precategory (C .fst) ``` diff --git a/src/Cat/Instances/Functor/Limits.lagda.md b/src/Cat/Instances/Functor/Limits.lagda.md index c021f0b93..6ca06cf14 100644 --- a/src/Cat/Instances/Functor/Limits.lagda.md +++ b/src/Cat/Instances/Functor/Limits.lagda.md @@ -74,9 +74,9 @@ homomorphism $K \to \lim F(-, x)$ will be called `!-for`{.Agda}. functor-apex : Functor E C functor-apex .F₀ x = D-lim.apex x functor-apex .F₁ {x} {y} f = !-for f - functor-apex .F-id = sym $ D-lim.unique _ _ _ _ λ j → + functor-apex .F-id = D-lim.unique _ _ _ _ λ j → C.idr _ ∙ C.introl F'.rmap-id - functor-apex .F-∘ f g = sym $ D-lim.unique _ _ _ _ λ j → + functor-apex .F-∘ f g = D-lim.unique _ _ _ _ λ j → C.pulll (D-lim.factors _ _ _) ∙ C.pullr (D-lim.factors _ _ _) ∙ C.pulll (sym (F'.rmap-∘ _ _)) diff --git a/src/Cat/Instances/Graphs/Exponentials.lagda.md b/src/Cat/Instances/Graphs/Exponentials.lagda.md index 134ebbe76..a3caa0477 100644 --- a/src/Cat/Instances/Graphs/Exponentials.lagda.md +++ b/src/Cat/Instances/Graphs/Exponentials.lagda.md @@ -60,6 +60,6 @@ Graphs-closed .has-exp A B .has-is-exp .ƛ m = record where Graphs-closed .has-exp A B .has-is-exp .commutes m = trivialᴳ! Graphs-closed .has-exp A B .has-is-exp .unique m' x = ext record where - node a b i = x i .node (a , b) - edge a i b = x i .edge (a , b) + node a b i = x (~ i) .node (a , b) + edge a i b = x (~ i) .edge (a , b) ``` diff --git a/src/Cat/Instances/Graphs/Limits.lagda.md b/src/Cat/Instances/Graphs/Limits.lagda.md index 3b2b2d93a..d75001b9d 100644 --- a/src/Cat/Instances/Graphs/Limits.lagda.md +++ b/src/Cat/Instances/Graphs/Limits.lagda.md @@ -108,8 +108,8 @@ Graphs-products a b .has-is-product .π₁∘⟨⟩ = trivialᴳ! Graphs-products a b .has-is-product .π₂∘⟨⟩ = trivialᴳ! Graphs-products a b .has-is-product .unique p q = ext record where - node x i = p i .node x , q i .node x - edge e i = p i .edge e , q i .edge e + node x i = p (~ i) .node x , q (~ i) .node x + edge e i = p (~ i) .edge e , q (~ i) .edge e Graphs-terminal : ∀ {o ℓ} → Terminal (Graphs o ℓ) Graphs-terminal .Terminal.top = ⊤ᴳ @@ -137,8 +137,8 @@ Graphs-pullbacks f g .has-is-pb .universal {p₁' = p₁'} {p₂'} α = record w Graphs-pullbacks f g .has-is-pb .p₁∘universal = trivialᴳ! Graphs-pullbacks f g .has-is-pb .p₂∘universal = trivialᴳ! Graphs-pullbacks f g .has-is-pb .unique α β = ext record where - node x = (λ i → α i .node x) ,ₚ (λ i → β i .node x) ,ₚ prop! - edge x = (λ i → α i .edge x) ,ₚ (λ i → β i .edge x) ,ₚ prop! + node x = (λ i → α (~ i) .node x) ,ₚ (λ i → β (~ i) .node x) ,ₚ prop! + edge x = (λ i → α (~ i) .edge x) ,ₚ (λ i → β (~ i) .edge x) ,ₚ prop! Graphs-finitely-complete : Finitely-complete (Graphs o ℓ) Graphs-finitely-complete = record diff --git a/src/Cat/Instances/MarkedGraphs.lagda.md b/src/Cat/Instances/MarkedGraphs.lagda.md index 2a7c5284c..6bec399cb 100644 --- a/src/Cat/Instances/MarkedGraphs.lagda.md +++ b/src/Cat/Instances/MarkedGraphs.lagda.md @@ -503,8 +503,8 @@ Marked-free-category G .Free-object.commute {Y = C} = where open Precategory (C .fst) Marked-free-category G .Free-object.unique {Y = C} F p = Marked-path-category-functor-path - (λ x i → p i .node x) - (λ e → to-pathp (from-pathp (λ i → p i .edge e) ∙ sym (idl _))) + (λ x i → p (~ i) .node x) + (λ e → to-pathp (ap (subst₂ Hom _ _) (idl _) ∙ from-pathp (λ i → p (~ i) .edge e))) where open Precategory (C .fst) ``` diff --git a/src/Cat/Instances/OFE/Coproduct.lagda.md b/src/Cat/Instances/OFE/Coproduct.lagda.md index 3f218b62a..bdf83ec6b 100644 --- a/src/Cat/Instances/OFE/Coproduct.lagda.md +++ b/src/Cat/Instances/OFE/Coproduct.lagda.md @@ -191,6 +191,6 @@ unique: but it suffices to reason at the level of sets. mk .has-is-coproduct .[]∘ι₁ = ext λ _ → refl mk .has-is-coproduct .[]∘ι₂ = ext λ _ → refl mk .has-is-coproduct .unique p q = ext λ where - (inl x) → p ·ₚ x - (inr x) → q ·ₚ x + (inl x) → sym p ·ₚ x + (inr x) → sym q ·ₚ x ``` diff --git a/src/Cat/Instances/OFE/Product.lagda.md b/src/Cat/Instances/OFE/Product.lagda.md index d6cb97b36..80e04d9c7 100644 --- a/src/Cat/Instances/OFE/Product.lagda.md +++ b/src/Cat/Instances/OFE/Product.lagda.md @@ -83,7 +83,7 @@ OFE-Product A B .has-is-product .⟨_,_⟩ f g .snd .pres-≈ p = OFE-Product A B .has-is-product .π₁∘⟨⟩ = ext λ _ → refl OFE-Product A B .has-is-product .π₂∘⟨⟩ = ext λ _ → refl -OFE-Product A B .has-is-product .unique p q = ext λ x → p ·ₚ x ,ₚ q ·ₚ x +OFE-Product A B .has-is-product .unique p q = ext λ x → sym p ·ₚ x ,ₚ sym q ·ₚ x ``` diff --git a/src/Data/Set/Surjection.lagda.md b/src/Data/Set/Surjection.lagda.md index 553ab8fee..292635098 100644 --- a/src/Data/Set/Surjection.lagda.md +++ b/src/Data/Set/Surjection.lagda.md @@ -82,8 +82,8 @@ surjectivity out of the way, we get what we wanted. ∥-∥-elim {P = λ e → go {F} e' p (f x) e ≡ e' x} (λ x → hlevel 1) (λ e → p $ₚ (e .fst , x , e .snd)) (surj (f x)) coeqs .unique {F} {e'} {p} {colim} comm = funext λ a → - ∥-∥-elim {P = λ e → colim a ≡ go {F} e' p a e} (λ x → hlevel 1) - (λ x → ap colim (sym (x .snd)) ∙ comm $ₚ x .fst) + ∥-∥-elim {P = λ e → go {F} e' p a e ≡ colim a} (λ x → hlevel 1) + (λ x → sym comm ·ₚ x .fst ∙ ap colim (x .snd)) (surj a) ``` diff --git a/src/Order/Instances/Coproduct.lagda.md b/src/Order/Instances/Coproduct.lagda.md index a30ccd82f..bd095418d 100644 --- a/src/Order/Instances/Coproduct.lagda.md +++ b/src/Order/Instances/Coproduct.lagda.md @@ -133,8 +133,8 @@ Posets-has-coproducts P Q .has-is-coproduct .is-coproduct.[_,_] = matchᵖ Posets-has-coproducts P Q .has-is-coproduct .[]∘ι₁ = ext λ _ → refl Posets-has-coproducts P Q .has-is-coproduct .[]∘ι₂ = ext λ _ → refl Posets-has-coproducts P Q .has-is-coproduct .unique α β = ext λ where - (inl x) → α ·ₚ x - (inr x) → β ·ₚ x + (inl x) → sym α ·ₚ x + (inr x) → sym β ·ₚ x ``` As a related fact, we can show that the empty poset is the [[initial diff --git a/src/Order/Instances/Disjoint.lagda.md b/src/Order/Instances/Disjoint.lagda.md index bab546918..43a972eb4 100644 --- a/src/Order/Instances/Disjoint.lagda.md +++ b/src/Order/Instances/Disjoint.lagda.md @@ -109,7 +109,7 @@ Posets-has-set-indexed-coproducts I F = mk where mk .ι = injᵖ mk .has-is-ic .match = matchᵖ mk .has-is-ic .commute = ext λ _ → refl - mk .has-is-ic .unique f p = ext λ i x → p i ·ₚ x + mk .has-is-ic .unique f p = ext λ i x → sym (p i) ·ₚ x ``` ## Binary coproducts are a special case of indexed coproducts diff --git a/src/Order/Instances/Lower/Cocompletion.lagda.md b/src/Order/Instances/Lower/Cocompletion.lagda.md index 5eb15ae3c..a49c5aedc 100644 --- a/src/Order/Instances/Lower/Cocompletion.lagda.md +++ b/src/Order/Instances/Lower/Cocompletion.lagda.md @@ -144,8 +144,8 @@ reveals that $f'$ must agree with $\widehat{f}$. → ( ∀ {I : Type o} (F : I → Lower-set A) → f~ · Lub.lub (Lower-sets-cocomplete A F) ≡ ⋃ (λ i → f~ · (F i)) ) → (∀ x → f~ · ↓ A x ≡ f · x) - → f~ ≡ Lan↓ - Lan↓-unique f~ f~-cocont f~-comm = ext λ i → + → Lan↓ ≡ f~ + Lan↓-unique f~ f~-cocont f~-comm = sym $ ext λ i → f~ · i ≡⟨ ap· f~ (↓Coyoneda.lower-set-∫ A i) ⟩ f~ · Lub.lub (Lower-sets-cocomplete A (↓Coyoneda.diagram A i)) ≡⟨ f~-cocont (↓Coyoneda.diagram A i) ⟩ ⋃ (λ j → f~ · (↓Coyoneda.diagram A i j)) ≡⟨ ap ⋃ (funext λ j → f~-comm (j .fst) ∙ sym (Lan↓-commutes (j .fst))) ⟩ diff --git a/src/Order/Instances/Pointwise.lagda.md b/src/Order/Instances/Pointwise.lagda.md index ef609b320..0013901aa 100644 --- a/src/Order/Instances/Pointwise.lagda.md +++ b/src/Order/Instances/Pointwise.lagda.md @@ -113,7 +113,7 @@ Posets-has-indexed-products F = mk where mk .π = prjᵖ mk .has-is-ip .tuple = tupleᵖ mk .has-is-ip .commute = ext λ _ → refl - mk .has-is-ip .unique f g = ext λ y i → g i ·ₚ y + mk .has-is-ip .unique f g = ext λ y i → sym (g i) ·ₚ y ``` ## Binary products are a special case of indexed products diff --git a/src/Order/Instances/Product.lagda.md b/src/Order/Instances/Product.lagda.md index 164b03bba..9d300bc81 100644 --- a/src/Order/Instances/Product.lagda.md +++ b/src/Order/Instances/Product.lagda.md @@ -89,7 +89,7 @@ Posets-has-products P Q .has-is-product .⟨_,_⟩ = pairᵖ Posets-has-products P Q .has-is-product .π₁∘⟨⟩ = ext λ _ → refl Posets-has-products P Q .has-is-product .π₂∘⟨⟩ = ext λ _ → refl Posets-has-products P Q .has-is-product .unique α β = - ext λ x → α ·ₚ x ,ₚ β ·ₚ x + ext λ x → sym α ·ₚ x ,ₚ sym β ·ₚ x ``` As a related observation, we can show that the unique partial order on diff --git a/src/Order/Semilattice/Free.lagda.md b/src/Order/Semilattice/Free.lagda.md index 5d138d115..5fc10296a 100644 --- a/src/Order/Semilattice/Free.lagda.md +++ b/src/Order/Semilattice/Free.lagda.md @@ -232,9 +232,9 @@ elements of $P$, which is the same join used to compute the extension of $f$. ```agda -make-free-join-slat A .unique {B} {f} g p = ext λ P pfin → - sym $ lub-unique (fold-K.ε'.has-lub A B f P pfin) - (cast-is-lubᶠ (λ Q → p ·ₚ Q .fst) $ - pres-finitely-indexed-lub (g .witness) pfin _ _ $ - K-singleton-lub A _) +make-free-join-slat A .unique {B} {f} g p = ext λ P pfin → lub-unique + (fold-K.ε'.has-lub A B f P pfin) + (cast-is-lubᶠ (λ Q → p ·ₚ Q .fst) $ + pres-finitely-indexed-lub (g .witness) pfin _ _ $ + K-singleton-lub A _) ``` From d96352d05995e18c42bc96cafd655ac7646b173e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Fri, 17 Jul 2026 12:11:18 -0300 Subject: [PATCH 2/4] chore: display forms for Initial/Terminal --- src/Cat/Abelian/Base.lagda.md | 6 +++--- src/Cat/Abelian/Functor.lagda.md | 2 +- src/Cat/Diagram/Initial.lagda.md | 21 ++++++++++----------- src/Cat/Diagram/Limit/Finite.lagda.md | 9 +++++---- src/Cat/Diagram/Limit/Pullback.lagda.md | 7 ++++--- src/Cat/Diagram/Terminal.lagda.md | 21 ++++++++++----------- src/Cat/Diagram/Zero.lagda.md | 6 +++--- src/Cat/Functor/Adjoint.lagda.md | 16 +++++++++------- 8 files changed, 45 insertions(+), 43 deletions(-) diff --git a/src/Cat/Abelian/Base.lagda.md b/src/Cat/Abelian/Base.lagda.md index f85fe5c22..9a03fd51e 100644 --- a/src/Cat/Abelian/Base.lagda.md +++ b/src/Cat/Abelian/Base.lagda.md @@ -203,7 +203,7 @@ record is-additive {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ lsuc ℓ) where module ∅ = Zero ∅ 0m-unique : ∀ {A B} → ∅.zero→ {A} {B} ≡ 0m - 0m-unique = ap₂ _∘_ (∅.has⊥ _ .paths _) refl ∙ ∘-zero-l + 0m-unique = ap₂ _∘_ (∅.¡-unique _) refl ∙ ∘-zero-l ``` Coincidence of finite products and finite coproducts leads to an object @@ -410,7 +410,7 @@ monomorphism]. path : f ∘ kernel f .Kernel.kernel ≡ f ∘ 0m path = Ker.equal f ∙∙ ∅.zero-∘r _ - ∙∙ ap₂ _∘_ (∅.has⊥ _ .paths 0m) refl + ∙∙ ap₂ _∘_ (∅.¡-unique 0m) refl ∙∙ ∘-zero-l ∙∙ sym ∘-zero-r ``` --> @@ -431,7 +431,7 @@ the canonical subobject inclusion $\ker(f) \to B$. path : ∅.zero→ ∘ proj' ≡ Coker.coeq f ∘ proj' path = Coker.unique₂ (Ker.kernel f) {e' = 0m} (∘-zero-r ∙ sym ∘-zero-l) - (pushl (∅.zero-∘r _) ∙ pulll ( ap₂ _∘_ refl (∅.has⊤ _ .paths 0m) + (pushl (∅.zero-∘r _) ∙ pulll ( ap₂ _∘_ refl (∅.!-unique 0m) ∙ ∘-zero-r) ∙ ∘-zero-l) (pullr (Coker.factors (Ker.kernel f)) ∙ sym (Coker.coequal _) diff --git a/src/Cat/Abelian/Functor.lagda.md b/src/Cat/Abelian/Functor.lagda.md index e60d17823..7cf6414b0 100644 --- a/src/Cat/Abelian/Functor.lagda.md +++ b/src/Cat/Abelian/Functor.lagda.md @@ -86,7 +86,7 @@ Ab-functor-pres-∅ Ab-functor-pres-∅ {A = A} {B = B} F ∅A = id-zero→zero B $ B.id ≡˘⟨ F.F-id ⟩ - F.₁ A.id ≡⟨ ap F.₁ (is-contr→is-prop (Zero.has⊤ ∅A (Zero.∅ ∅A)) _ _) ⟩ + F.₁ A.id ≡⟨ ap F.₁ (Zero.!-unique₂ ∅A _ _) ⟩ F.₁ A.0m ≡⟨ F.F-0m ⟩ B.0m ∎ where diff --git a/src/Cat/Diagram/Initial.lagda.md b/src/Cat/Diagram/Initial.lagda.md index 40aa8c28c..ecaad9a06 100644 --- a/src/Cat/Diagram/Initial.lagda.md +++ b/src/Cat/Diagram/Initial.lagda.md @@ -25,25 +25,24 @@ if there exists a _unique_ map to any other object: ```agda is-initial : Ob → Type _ is-initial ob = ∀ x → is-contr (Hom ob x) - - record Initial : Type (o ⊔ h) where - field - bot : Ob - has⊥ : is-initial bot ``` We refer to the centre of contraction as `¡`{.Agda}. Since it inhabits a contractible type, it is unique. ```agda - ¡ : ∀ {x} → Hom bot x - ¡ = has⊥ _ .centre + module is-initial {ob} (t : is-initial ob) where + module _ {x} where open is-contr (t x) renaming (centre to ¡ ; paths to ¡-unique) public - ¡-unique : ∀ {x} (h : Hom bot x) → ¡ ≡ h - ¡-unique = has⊥ _ .paths + ¡-unique₂ : ∀ {x} (f g : Hom ob x) → f ≡ g + ¡-unique₂ = is-contr→is-prop (t _) + + record Initial : Type (o ⊔ h) where + field + bot : Ob + has⊥ : is-initial bot - ¡-unique₂ : ∀ {x} (f g : Hom bot x) → f ≡ g - ¡-unique₂ = is-contr→is-prop (has⊥ _) + open is-initial has⊥ public open Initial ``` diff --git a/src/Cat/Diagram/Limit/Finite.lagda.md b/src/Cat/Diagram/Limit/Finite.lagda.md index 3a646ae9a..6c530ec97 100644 --- a/src/Cat/Diagram/Limit/Finite.lagda.md +++ b/src/Cat/Diagram/Limit/Finite.lagda.md @@ -274,8 +274,8 @@ object $*$. module Pb = is-pullback pb prod : is-product C p1 p2 - prod .is-product.⟨_,_⟩ p1' p2' = - Pb.universal {p₁' = p1'} {p₂' = p2'} (is-contr→is-prop (term _) _ _) + prod .is-product.⟨_,_⟩ p1' p2' = Pb.universal {p₁' = p1'} {p₂' = p2'} $ + is-contr→is-prop (term _) _ _ prod .is-product.π₁∘⟨⟩ = Pb.p₁∘universal prod .is-product.π₂∘⟨⟩ = Pb.p₂∘universal prod .is-product.unique p q = Pb.unique p q @@ -287,8 +287,9 @@ object $*$. with-pullbacks top pb = fc where module top = Terminal top mkprod : ∀ A B → Product C A B - mkprod A B = record { has-is-product = terminal-pullback→product top.has⊤ pb' } - where pb' = pb (top.has⊤ A .centre) (top.has⊤ B .centre) .Pullback.has-is-pb + mkprod A B = record where + has-is-product = terminal-pullback→product top.has⊤ $ + pb top.! top.! .Pullback.has-is-pb mkeq : ∀ {A B} (f g : Hom A B) → Equaliser C f g mkeq {A = A} {B} f g = eq where diff --git a/src/Cat/Diagram/Limit/Pullback.lagda.md b/src/Cat/Diagram/Limit/Pullback.lagda.md index 1ca43f3e4..508ef415f 100644 --- a/src/Cat/Diagram/Limit/Pullback.lagda.md +++ b/src/Cat/Diagram/Limit/Pullback.lagda.md @@ -69,14 +69,15 @@ Terminal-cone→Pullback → Pullback Cat (F .F₁ {cs-a} {cs-c} _) (F .F₁ {cs-b} {cs-c} _) Terminal-cone→Pullback {F = F} lim = pb where module lim = Terminal lim + pb : Pullback Cat _ _ pb .apex = lim.top .apex pb .p₁ = lim.top .ψ cs-a pb .p₂ = lim.top .ψ cs-b pb .has-is-pb .square = lim.top .commutes _ ∙ sym (lim.top .commutes {cs-b} {cs-c} _) - pb .has-is-pb .universal x = lim.has⊤ (Square→Cone _ _ x) .centre .map - pb .has-is-pb .p₁∘universal {p = p} = lim.has⊤ (Square→Cone _ _ p) .centre .com cs-a - pb .has-is-pb .p₂∘universal {p = p} = lim.has⊤ (Square→Cone _ _ p) .centre .com cs-b + pb .has-is-pb .universal x = lim.! {Square→Cone _ _ x} .map + pb .has-is-pb .p₁∘universal = lim.! .com cs-a + pb .has-is-pb .p₂∘universal = lim.! .com cs-b pb .has-is-pb .unique {p₁' = p₁'} {p₂'} {p} {lim'} a b = ap map (lim.has⊤ (Square→Cone _ _ p) .paths other) where diff --git a/src/Cat/Diagram/Terminal.lagda.md b/src/Cat/Diagram/Terminal.lagda.md index 5ab24f830..1a06022a4 100644 --- a/src/Cat/Diagram/Terminal.lagda.md +++ b/src/Cat/Diagram/Terminal.lagda.md @@ -28,25 +28,24 @@ if it admits a _unique_ map from any other object: ```agda is-terminal : Ob → Type _ is-terminal ob = ∀ x → is-contr (Hom x ob) - - record Terminal : Type (o ⊔ h) where - field - top : Ob - has⊤ : is-terminal top ``` We refer to the centre of contraction as `!`{.Agda}. Since it inhabits a contractible type, it is unique. ```agda - ! : ∀ {x} → Hom x top - ! = has⊤ _ .centre + module is-terminal {ob} (t : is-terminal ob) where + module _ {x} where open is-contr (t x) renaming (centre to ! ; paths to !-unique) public - !-unique : ∀ {x} (h : Hom x top) → ! ≡ h - !-unique = has⊤ _ .paths + !-unique₂ : ∀ {x} (f g : Hom x ob) → f ≡ g + !-unique₂ = is-contr→is-prop (t _) + + record Terminal : Type (o ⊔ h) where + field + top : Ob + has⊤ : is-terminal top - !-unique₂ : ∀ {x} (f g : Hom x top) → f ≡ g - !-unique₂ = is-contr→is-prop (has⊤ _) + open is-terminal has⊤ public open Terminal ``` diff --git a/src/Cat/Diagram/Zero.lagda.md b/src/Cat/Diagram/Zero.lagda.md index 0149f671d..8d958020b 100644 --- a/src/Cat/Diagram/Zero.lagda.md +++ b/src/Cat/Diagram/Zero.lagda.md @@ -31,6 +31,9 @@ coincide. When this occurs, we call the object a **zero object**. has-is-initial : is-initial C ob has-is-terminal : is-terminal C ob + open is-terminal C has-is-terminal public + open is-initial C has-is-initial public + record Zero : Type (o ⊔ h) where field ∅ : Ob @@ -43,9 +46,6 @@ coincide. When this occurs, we call the object a **zero object**. initial : Initial C initial = record { bot = ∅ ; has⊥ = has-is-initial } - - open Terminal terminal public hiding (top) - open Initial initial public hiding (bot) ``` ::: {.definition #zero-morphism} diff --git a/src/Cat/Functor/Adjoint.lagda.md b/src/Cat/Functor/Adjoint.lagda.md index f30390e03..38a68182f 100644 --- a/src/Cat/Functor/Adjoint.lagda.md +++ b/src/Cat/Functor/Adjoint.lagda.md @@ -880,17 +880,19 @@ module _ {o h o' h'} {C : Precategory o h} {D : Precategory o' h'} where Universal-morphism R X = Initial (X ↙ R) open Free-object - open Initial open ↓Obj open ↓Hom universal-map→free-object : ∀ {R X} → Universal-morphism R X → Free-object R X - universal-map→free-object x .free = _ - universal-map→free-object x .unit = x .bot .map - universal-map→free-object x .fold f = x .has⊥ (↓obj f) .centre .bot - universal-map→free-object x .commute = sym (x .has⊥ _ .centre .com) ∙ C.idr _ - universal-map→free-object x .unique g p = ap bot - (x .has⊥ _ .paths (↓hom (sym (p ∙ sym (C.idr _))))) + universal-map→free-object x = record where + module x = Initial x + free = _ + + unit = x.bot .map + fold f = x.¡ {↓obj f} .bot + + commute = sym (x.¡ .com) ∙ C.idr _ + unique g p = ap bot $ x.¡-unique (↓hom (sym (p ∙ sym (C.idr _)))) universal-maps→functor : ∀ {R} → (∀ X → Universal-morphism R X) → Functor C D universal-maps→functor u = free-objects→functor From 6f332edce8bc049d8f56332edc4183993e7f40b8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Fri, 17 Jul 2026 12:19:50 -0300 Subject: [PATCH 3/4] =?UTF-8?q?chore:=20simplify=20is-complete=E2=86=92fin?= =?UTF-8?q?itely?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lifed from #647 --- src/Cat/Diagram/Limit/Finite.lagda.md | 44 ++++++++------------------- 1 file changed, 12 insertions(+), 32 deletions(-) diff --git a/src/Cat/Diagram/Limit/Finite.lagda.md b/src/Cat/Diagram/Limit/Finite.lagda.md index 6c530ec97..1cded2c6e 100644 --- a/src/Cat/Diagram/Limit/Finite.lagda.md +++ b/src/Cat/Diagram/Limit/Finite.lagda.md @@ -3,6 +3,7 @@ open import Cat.Diagram.Pullback.Properties open import Cat.Instances.Shape.Parallel open import Cat.Diagram.Limit.Equaliser +open import Cat.Instances.Shape.Initial open import Cat.Diagram.Limit.Pullback open import Cat.Diagram.Limit.Terminal open import Cat.Diagram.Product.Finite @@ -46,8 +47,9 @@ every diagram with a [[finite|finite category]] shape. ```agda is-finitely-complete : Typeω - is-finitely-complete = ∀ {o ℓ} {D : Precategory o ℓ} → is-finite-precategory D - → (F : Functor D C) → Limit F + is-finitely-complete = + ∀ {o ℓ} {D : Precategory o ℓ} + → is-finite-precategory D → (F : Functor D C) → Limit F ``` Similarly to the case with [[arbitrary limits|complete category]], we can get away with @@ -384,8 +386,7 @@ is indeed the equaliser of $f$ and $g$. ```agda eq .has-is-eq .universal {e' = e'} p = - Pb.universal (Bb.unique₂ refl refl (sym p1) (sym p2)) - where + Pb.universal (Bb.unique₂ refl refl (sym p1) (sym p2)) where p1 : Bb.π₁ ∘ ⟨id,id⟩ ∘ f ∘ e' ≡ Bb.π₁ ∘ ⟨f,g⟩ ∘ e' p1 = Bb.π₁ ∘ ⟨id,id⟩ ∘ f ∘ e' ≡⟨ cancell Bb.π₁∘⟨⟩ ⟩ @@ -401,8 +402,7 @@ is indeed the equaliser of $f$ and $g$. eq .has-is-eq .factors = Pb.p₂∘universal eq .has-is-eq .unique {F} {e' = e'} {other = other} p₂∘l=e' = - Pb.unique path p₂∘l=e' - where + Pb.unique path p₂∘l=e' where path : Pb.p₁ ∘ other ≡ f ∘ e' path = Pb.p₁ ∘ other ≡⟨ insertl Bb.π₁∘⟨⟩ ⟩ @@ -438,32 +438,12 @@ Putting it all together into a record we get our proof of finite completeness: is-complete→finitely : ∀ {a b} → is-complete a b C → Finitely-complete - is-complete→finitely {a} {b} compl = with-pullbacks term' pb - where - pb : ∀ {x y z} (f : Hom x z) (g : Hom y z) → Pullback C f g - pb f g = Limit→Pullback C (compl (cospan→cospan-diagram _ _ f g)) - - idx : Precategory a b - idx = Lift-cat a b (Disc ⊥ λ x → absurd x) - - F : Functor idx C - F .Functor.F₀ () - F .Functor.F₁ {()} - F .Functor.F-id {()} - F .Functor.F-∘ {()} - - limF : Limit F - limF = compl F - open Terminal - open Cone-hom - open Cone - - term' : Terminal C - term' = record where - top = Limit.apex limF - has⊤ x = record where - centre = Limit.universal limF (λ ()) λ { {()} } - paths h = Limit.unique limF _ _ h λ () + is-complete→finitely {a} {b} compl = with-pullbacks term' pb where + pb : ∀ {x y z} (f : Hom x z) (g : Hom y z) → Pullback C f g + pb f g = Limit→Pullback C (compl (cospan→cospan-diagram _ _ f g)) + + term' : Terminal C + term' = Limit→Terminal C (is-complete-lower a b lzero lzero compl ¡F) ``` --> From 37a16db3d85f28d9053fa87881a16cfc60692ad0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Fri, 17 Jul 2026 16:30:57 -0300 Subject: [PATCH 4/4] defn: apd! --- 1lab.agda-lib | 1 + src/1Lab/Reflection.lagda.md | 45 ++++--- src/1Lab/Reflection/HLevel.agda | 2 +- src/1Lab/Reflection/Marker.agda | 122 ++++++++++++++++-- src/1Lab/Reflection/Regularity.agda | 2 +- src/Cat/Displayed/Functor.lagda.md | 12 +- .../Displayed/Functor/Adjoint/Total.lagda.md | 34 ++--- .../Displayed/Functor/Equivalence.lagda.md | 24 ++-- src/Cat/Displayed/Morphism.lagda.md | 2 +- src/Cat/Functor/Coherence.agda | 2 +- 10 files changed, 176 insertions(+), 70 deletions(-) diff --git a/1lab.agda-lib b/1lab.agda-lib index 5beab3325..2a1c4a9c3 100644 --- a/1lab.agda-lib +++ b/1lab.agda-lib @@ -9,3 +9,4 @@ flags: --postfix-projections -W noUnsupportedIndexedMatch --experimental-lazy-instances + --quote-metas diff --git a/src/1Lab/Reflection.lagda.md b/src/1Lab/Reflection.lagda.md index 29fe487a2..662534e1e 100644 --- a/src/1Lab/Reflection.lagda.md +++ b/src/1Lab/Reflection.lagda.md @@ -9,7 +9,7 @@ open import Data.String.Show open import Data.Bool.Base open import Data.List.Base open import Data.Dec.Base -open import Data.Vec.Base +open import Data.Vec.Base hiding (_++_) open import Meta.Append ``` @@ -394,21 +394,32 @@ extend-context* : ∀ {a} {A : Type a} → Telescope → TC A → TC A extend-context* [] a = a extend-context* ((nm , tm) ∷ xs) a = extend-context nm tm (extend-context* xs a) +record New-meta : Type where + constructor meta + field + new-meta : Meta + new-term : Term + ⦃ neu ⦄ : Has-neutrals.neutral auto new-term + +new-meta' : Term → TC New-meta +new-meta' ty = do + debugPrint "tactic.meta" 70 [ "new-meta'\n" , termErr ty ] + tm@(Term.meta mv _) ← check-type unknown ty + where what → do + debugPrint "tactic.meta" 70 + [ "check-type unknown returns\n" , termErr what ] + typeError "impossible new-meta'" + debugPrint "tactic.meta" 70 + [ "Created new meta\n " , termErr tm , "\nof type\n " , termErr ty ] + pure (meta mv tm) + new-meta : Term → TC Term new-meta ty = do mv ← check-type unknown ty debugPrint "tactic.meta" 70 - [ "Created new meta " , termErr mv , " of type " , termErr ty ] + [ "Created new meta\n " , termErr mv , "\nof type\n " , termErr ty ] pure mv -new-meta' : Term → TC (Meta × Term) -new-meta' ty = do - tm@(meta mv _) ← check-type unknown ty - where _ → typeError "impossible new-meta'" - debugPrint "tactic.meta" 70 - [ "Created new meta " , termErr tm , " of type " , termErr tm ] - pure (mv , tm) - block-on-meta : ∀ {a} {A : Type a} → Meta → TC A block-on-meta m = blockTC (blocker-meta m) @@ -509,12 +520,16 @@ unapply-path' false red@(def (quote PathP) (l h∷ T v∷ x v∷ y v∷ [])) = d pure (just (domain , x , y)) unapply-path' true tm = reduce tm >>= λ where - tm@(meta _ _) → do - (Tmv , T) ← new-meta' (pi (argN (quoteTerm I)) (abs "i" (def (quote Type) (unknown v∷ [])))) - l ← new-meta (meta Tmv (quoteTerm i0 v∷ [])) - r ← new-meta (meta Tmv (quoteTerm i1 v∷ [])) + tm@(meta _ cx) → do + meta Tmv T ← new-meta' $ pi (argN (quoteTerm I)) + (abs "i" (def (quote Type) (unknown v∷ []))) + + meta lmv l ← new-meta' (T ##ₙ quoteTerm i0) + meta rmv r ← new-meta' (T ##ₙ quoteTerm i1) + unify tm (def (quote PathP) (T v∷ l v∷ r v∷ [])) - traverse wait-for-type (l ∷ r ∷ []) + blockTC {A = ⊤} (blocker-all (blocker-meta lmv ∷ blocker-meta rmv ∷ [])) + pure (just (T , l , r)) red@(def (quote PathP) (T v∷ l v∷ r v∷ [])) → do diff --git a/src/1Lab/Reflection/HLevel.agda b/src/1Lab/Reflection/HLevel.agda index 951bacbe2..1f9213d4d 100644 --- a/src/1Lab/Reflection/HLevel.agda +++ b/src/1Lab/Reflection/HLevel.agda @@ -152,7 +152,7 @@ hlevel-proj A want goal = withNormalisation false do debugPrint "tactic.hlevel" 30 [ "H-Level: trying projections for term:\n " , termErr (def head args), "\nwith head symbol ", nameErr head ] projection ← resetting do - (mv , _) ← new-meta' (def (quote hlevel-projection) (argN (lit (name head)) ∷ [])) + meta mv _ ← new-meta' (def (quote hlevel-projection) (argN (lit (name head)) ∷ [])) get-instances mv >>= λ where [] → typeError [ "H-Level: There are no hints for treating the name " , nameErr head , " as a projection.\n" diff --git a/src/1Lab/Reflection/Marker.agda b/src/1Lab/Reflection/Marker.agda index 59b668243..6f74f7c87 100644 --- a/src/1Lab/Reflection/Marker.agda +++ b/src/1Lab/Reflection/Marker.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --allow-unsolved-metas #-} open import 1Lab.Reflection open import 1Lab.Path open import 1Lab.Type @@ -16,6 +17,15 @@ module 1Lab.Reflection.Marker where ⌜ x ⌝ = x {-# NOINLINE ⌜_⌝ #-} +-- A placeholder for terms that should be turned into metavariables when +-- abstracting. +-- This can be used with apd! to mark terms on which the type of a +-- marker depends, as long as the path that ¿? replaces can be inferred +-- from the type of the argument to apd!. +¿? : ∀ {ℓ} {A : Type ℓ} {x : A} → A +¿? {x = x} = x +{-# NOINLINE ¿? #-} + -- Abstract over the marked term(s). All marked terms refer to the same -- variable, so e.g. -- @@ -23,25 +33,25 @@ module 1Lab.Reflection.Marker where -- -- is (λ e → f e (λ _ → e)). The resulting term is open in precisely one -- variable: that variable is what substitutes the marked terms. -abstract-marker : Term → Maybe Term -abstract-marker = go 0 where +abstract-marker : Nat → Term → Maybe Term +abstract-marker base = go 0 where go : Nat → Term → Maybe Term go* : Nat → List (Arg Term) → Maybe (List (Arg Term)) - go k (var j args) = var j' <$> go* k args - where - j' : Nat - j' with j < k - ... | false = suc j - ... | true = j + go k (var j args) = var j' <$> go* k args where + j' : Nat + j' with j < k + ... | false = base + j + ... | true = j go k (con c args) = con c <$> go* k args go k (def f args) with f ... | quote ⌜_⌝ = pure (var k []) - -- ^ This is the one interesting case. Any application of the marker + -- ^ This is the first interesting case. Any application of the marker -- gets replaced with the 'k'th variable. Initially k = 0, so this is -- the variable bound by the lambda. But as we encounter further -- binders, we must increment this, since the marked term gets farther -- and farther away in the context. + ... | quote ¿? = pure unknown ... | x = def f <$> go* k args go k (lam v (abs x t)) = lam v ∘ abs x <$> go (suc k) t go k (pat-lam cs args) = nothing @@ -88,9 +98,9 @@ private ap-worker : ∀ {ℓ} {A : Type ℓ} (x : A) → Term → TC ⊤ ap-worker x goal = withNormalisation false do `x ← wait-for-type =<< quoteTC x - case abstract-marker `x of λ where + case abstract-marker 1 `x of λ where (just l) → do - debugPrint "1lab.marked-ap" 10 + debugPrint "tactic.marked-ap" 10 [ "original " , termErr `x , "\n" , "abstracted" , termErr (lam visible (abs "x" l)) ] @@ -129,3 +139,93 @@ module _ {ℓ} {A : Type ℓ} {x y : A} {p : x ≡ y} {f : A → (A → A) → A r = f ⌜ y ⌝ (λ _ → ⌜ y ⌝) ≡˘⟨ ap¡ p ⟩ f x (λ _ → x) ∎ + +private + -- In addition to supporting ¿? to mark explicit problematic + -- dependencies, we also remove all implicit arguments when + -- abstracting over the path. + censor : Term → Term + censor* : List (Arg Term) → List (Arg Term) + + censor (var x args) = var x (censor* args) + censor (con c args) = con c (censor* args) + censor (def f args) = def f (censor* args) + censor (lam v (abs n tm)) = lam v (abs n (censor tm)) + censor (pat-lam cs args) = pat-lam cs (censor* args) + censor (pi (arg i x) (abs n y)) = pi (arg i (censor x)) (abs n (censor y)) + censor (agda-sort s) = agda-sort s + censor (lit l) = lit l + censor (meta m args) = unknown + censor unknown = unknown + + censor* [] = [] + censor* (t v∷ ts) = censor t v∷ censor* ts + censor* (t h∷ ts) = censor* ts + censor* (t i∷ ts) = censor* ts + + macro + apd-worker : ∀ {ℓ} {A : Type ℓ} → A → Term → Term → TC ⊤ + apd-worker endpoint what goal = withNormalisation false do + `endpoint ← wait-for-type =<< quoteTC endpoint + case abstract-marker 2 (censor `endpoint) of λ where + (just l) → do + let fn = lam visible (abs "i" (lam visible (abs "x" l))) + debugPrint "tactic.marked-ap" 10 + [ "original " , termErr `endpoint , "\n" + , "abstracted" , termErr fn + ] + unify goal (def₀ (quote apd) ##ₙ fn ##ₙ what) + nothing → typeError [ "apd!: Failed to abstract over marker in term\n " , termErr `endpoint ] + + -- The entry point for apd! can't use tactic arguments to have the + -- elaborator propagate the endpoint; it's just too circular. + -- + -- To prevent a performance blowup from quoting the entire type of the + -- goal, we take it apart by unifying against metavariables and + -- deferring to a different macro. The second macro application acts + -- like a "fence" for the blockTC primitive. + apd-wrapper : Bool → Term → Term → TC ⊤ + apd-wrapper right what goal = do + meta Tmv T ← new-meta' $ pi (argN (quoteTerm I)) + (abs "i" (def (quote Type) (unknown v∷ []))) + + l ← new-meta (T ##ₙ quoteTerm i0) + r ← new-meta (T ##ₙ quoteTerm i1) + + g' ← check-type goal (def₀ (quote PathP) ##ₙ T ##ₙ l ##ₙ r) + + unify goal (def₀ (quote apd-worker) ##ₙ (if right then r else l) ##ₙ what) + +macro + -- Generalised apd. Automatically generates the function to apply to + -- by abstracting over any markers in the LEFT ENDPOINT of the path. + -- Use with _≡[]⟨_⟩_. + apd! : Term → Term → TC ⊤ + apd! = apd-wrapper false + + -- Generalised apd. Automatically generates the function to apply to + -- by abstracting over any markers in the RIGHT ENDPOINT of the path. + -- Use with _≡[]˘⟨_⟩_. + apd¡ : Term → Term → TC ⊤ + apd¡ = apd-wrapper true + +module + _ {ℓ ℓ' ℓ''} {A : Type ℓ} {x y : A} {p : x ≡ y} {B : A → Type ℓ'} + {α : B x} {β : B y} (q : PathP (λ i → B (p i)) α β) + {C : (x : A) → B x → Type ℓ''} + (f : {x : A} (y : B x) → C x y) + (g : (x : A) (y : B x) → C x y) + where + + -- test that needs 'censor' + _ : PathP (λ i → C (p i) (q i)) (f ⌜ α ⌝) (f β) + _ = apd! q + + -- test that needs an explicit placeholder + _ : PathP (λ i → C (p i) (q i)) (g ¿? ⌜ α ⌝) (g y β) + _ = apd! q + + -- test that the tactic works with goals. + -- this needs --quote-metas + _ : PathP (λ i → C (p i) (q i)) (f ⌜ α ⌝) (f β) + _ = apd! {! !} diff --git a/src/1Lab/Reflection/Regularity.agda b/src/1Lab/Reflection/Regularity.agda index 1539ebe81..a1d0e4959 100644 --- a/src/1Lab/Reflection/Regularity.agda +++ b/src/1Lab/Reflection/Regularity.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas -vtactic:10 #-} +{-# OPTIONS --allow-unsolved-metas #-} open import 1Lab.Reflection.HLevel open import 1Lab.Reflection.Subst open import 1Lab.Reflection diff --git a/src/Cat/Displayed/Functor.lagda.md b/src/Cat/Displayed/Functor.lagda.md index 9e7467ded..bcf58420e 100644 --- a/src/Cat/Displayed/Functor.lagda.md +++ b/src/Cat/Displayed/Functor.lagda.md @@ -258,13 +258,13 @@ module (F' F∘' G') .F₀' x = F' .F₀' (G' .F₀' x) (F' F∘' G') .F₁' f = F' .F₁' (G' .F₁' f) (F' F∘' G') .F-id' = begin[] - F' .F₁' (G' .F₁' ℰ.id') ℋ.≡[]⟨ apd (λ i → F' .F₁') (G' .F-id') ⟩ - F' .F₁' ℱ.id' ℋ.≡[]⟨ F' .F-id' ⟩ - ℋ.id' ∎[] + F' .F₁' ⌜ G' .F₁' ℰ.id' ⌝ ℋ.≡[]⟨ apd! (G' .F-id') ⟩ + F' .F₁' ℱ.id' ℋ.≡[]⟨ F' .F-id' ⟩ + ℋ.id' ∎[] (F' F∘' G') .F-∘' {f = f} {g = g} {f' = f'} {g' = g'} = begin[] - F' .F₁' (G' .F₁' (f' ℰ.∘' g')) ℋ.≡[]⟨ apd (λ i → F' .F₁') (G' .F-∘') ⟩ - F₁' F' (G' .F₁' f' ℱ.∘' G' .F₁' g') ℋ.≡[]⟨ F' .F-∘' ⟩ - F' .F₁' (G' .F₁' f') ℋ.∘' F' .F₁' (G' .F₁' g') ∎[] + F' .F₁' ⌜ G' .F₁' (f' ℰ.∘' g') ⌝ ℋ.≡[]⟨ apd! (G' .F-∘') ⟩ + F₁' F' (G' .F₁' f' ℱ.∘' G' .F₁' g') ℋ.≡[]⟨ F' .F-∘' ⟩ + F' .F₁' (G' .F₁' f') ℋ.∘' F' .F₁' (G' .F₁' g') ∎[] ``` The composite of two fibred functors is a fibred functor. diff --git a/src/Cat/Displayed/Functor/Adjoint/Total.lagda.md b/src/Cat/Displayed/Functor/Adjoint/Total.lagda.md index 2152f6320..e0d4d8b29 100644 --- a/src/Cat/Displayed/Functor/Adjoint/Total.lagda.md +++ b/src/Cat/Displayed/Functor/Adjoint/Total.lagda.md @@ -74,26 +74,16 @@ taking care of the extra identity morphisms due to `∫ᶠ∘`{.Agda} and `∫ᶠId'≅Id`{.Agda}. ```agda -∫⊣ .zig {x , x'} = ∫Hom-path ℱ - ( (B.id B.∘ L⊣R.ε (₀ L x) B.∘ B.id) B.∘ ₁ L (A.id A.∘ L⊣R.η x A.∘ A.id) ≡⟨ ap (B._∘ ₁ L (A.id A.∘ L⊣R.η x A.∘ A.id)) (B.idlr (L⊣R.ε (₀ L x))) ⟩ - L⊣R .ε (₀ L x) B.∘ ₁ L (A.id A.∘ L⊣R.η x A.∘ A.id) ≡⟨ ap (λ f → L⊣R.ε (F₀ L x) B.∘ ₁ L f) (A.idlr (L⊣R.η x)) ⟩ - L⊣R .ε (₀ L x) B.∘ ₁ L (L⊣R .η x) ≡⟨ L⊣R.zig ⟩ - B.id ∎) - $ ℱ.begin[] - (ℱ.id' ℱ.∘' L'⊣R'.counit'.ε' (₀' L' x') ℱ.∘' ℱ.id') - ℱ.∘' ₁' L' (ℰ.id' ℰ.∘' L'⊣R'.unit'.η' x' ℰ.∘' ℰ.id') ℱ.≡[]⟨ apd (λ i → ℱ._∘' ₁' L' (ℰ.id' ℰ.∘' L'⊣R'.unit'.η' x' ℰ.∘' ℰ.id')) (ℱ.idlr' (L'⊣R'.counit'.ε' (₀' L' x'))) ⟩ - L'⊣R'.counit'.ε' (₀' L' x') ℱ.∘' ₁' L' (ℰ.id' ℰ.∘' L'⊣R'.unit'.η' x' ℰ.∘' ℰ.id') ℱ.≡[]⟨ apd (λ i f' → L'⊣R'.counit'.ε' (₀' L' x') ℱ.∘' ₁' L' f') (ℰ.idlr' (L'⊣R'.unit'.η' x')) ⟩ - L'⊣R'.counit'.ε' (₀' L' x') ℱ.∘' ₁' L' (L'⊣R'.unit'.η' x') ℱ.≡[]⟨ L'⊣R'.zig' ⟩ - ℱ.id' ℱ.∎[] -∫⊣ .zag {x , x'} = ∫Hom-path ℰ - ( ₁ R (B.id B.∘ L⊣R.ε x B.∘ B.id) A.∘ A.id A.∘ L⊣R.η (₀ R x) A.∘ A.id ≡⟨ ap (₁ R (B.id B.∘ L⊣R.ε x B.∘ B.id) A.∘_) (A.idlr (L⊣R.η (₀ R x))) ⟩ - ₁ R (B.id B.∘ L⊣R.ε x B.∘ B.id) A.∘ L⊣R.η (₀ R x) ≡⟨ ap (λ f → ₁ R f A.∘ L⊣R.η (F₀ R x)) (B.idlr (L⊣R.ε x)) ⟩ - ₁ R (L⊣R.ε x) A.∘ L⊣R.η (₀ R x) ≡⟨ L⊣R.zag ⟩ - A.id ∎) - $ ℰ.begin[] - ₁' R' (ℱ.id' ℱ.∘' L'⊣R'.counit'.ε' x' ℱ.∘' ℱ.id') - ℰ.∘' ℰ.id' ℰ.∘' L'⊣R'.unit'.η' (₀' R' x') ℰ.∘' ℰ.id' ℰ.≡[]⟨ apd (λ i → ₁' R' (ℱ.id' ℱ.∘' L'⊣R'.counit'.ε' x' ℱ.∘' ℱ.id') ℰ.∘'_) (ℰ.idlr' (L'⊣R'.unit'.η' (₀' R' x'))) ⟩ - ₁' R' (ℱ.id' ℱ.∘' L'⊣R'.counit'.ε' x' ℱ.∘' ℱ.id') ℰ.∘' L'⊣R'.unit'.η' (₀' R' x') ℰ.≡[]⟨ apd (λ i f → ₁' R' f ℰ.∘' L'⊣R'.unit'.η' (₀' R' x')) (ℱ.idlr' (L'⊣R'.counit'.ε' x')) ⟩ - ₁' R' (L'⊣R'.counit'.ε' x') ℰ.∘' L'⊣R'.unit'.η' (₀' R' x') ℰ.≡[]⟨ L'⊣R'.zag' ⟩ - ℰ.id' ℰ.∎[] +∫⊣ .zig {x , x'} = ∫Hom-path ℱ _ $ ℱ.begin + ⌜ ℱ.id' ℱ.∘' L'⊣R'.counit'.ε' (₀' L' x') ℱ.∘' ℱ.id' ⌝ + ℱ.∘' ₁' L' (ℰ.id' ℰ.∘' L'⊣R'.unit'.η' x' ℰ.∘' ℰ.id') ℱ.≡[]⟨ apd! (ℱ.idlr' (L'⊣R'.counit'.ε' (₀' L' x'))) ⟩ + L'⊣R'.counit'.ε' (₀' L' x') ℱ.∘' ₁' L' ⌜ ℰ.id' ℰ.∘' L'⊣R'.unit'.η' x' ℰ.∘' ℰ.id' ⌝ ℱ.≡[]⟨ apd! (ℰ.idlr' (L'⊣R'.unit'.η' x')) ⟩ + L'⊣R'.counit'.ε' (₀' L' x') ℱ.∘' ₁' L' (L'⊣R'.unit'.η' x') ℱ.≡[]⟨ L'⊣R'.zig' ⟩ + ℱ.id' ℱ.∎[] +∫⊣ .zag {x , x'} = ∫Hom-path ℰ _ $ ℰ.begin + ₁' R' (ℱ.id' ℱ.∘' L'⊣R'.counit'.ε' x' ℱ.∘' ℱ.id') + ℰ.∘' ⌜ ℰ.id' ℰ.∘' L'⊣R'.unit'.η' (₀' R' x') ℰ.∘' ℰ.id' ⌝ ℰ.≡[]⟨ apd! (ℰ.idlr' (L'⊣R'.unit'.η' (₀' R' x'))) ⟩ + ₁' R' ⌜ ℱ.id' ℱ.∘' L'⊣R'.counit'.ε' x' ℱ.∘' ℱ.id' ⌝ ℰ.∘' L'⊣R'.unit'.η' (₀' R' x') ℰ.≡[]⟨ apd! (ℱ.idlr' (L'⊣R'.counit'.ε' x')) ⟩ + ₁' R' (L'⊣R'.counit'.ε' x') ℰ.∘' L'⊣R'.unit'.η' (₀' R' x') ℰ.≡[]⟨ L'⊣R'.zag' ⟩ + ℰ.id' ℰ.∎[] ``` diff --git a/src/Cat/Displayed/Functor/Equivalence.lagda.md b/src/Cat/Displayed/Functor/Equivalence.lagda.md index 8b972b277..a1dee069d 100644 --- a/src/Cat/Displayed/Functor/Equivalence.lagda.md +++ b/src/Cat/Displayed/Functor/Equivalence.lagda.md @@ -239,11 +239,11 @@ surjectivity to define `F'⁻¹`{.Agda}: ffy' = f*y'-iso .ℱ.from' F'⁻¹ .F-id' {x} {x'} = ℰ.begin[] - ff'⁻¹ (ffx' ℱ.∘' ℱ.id' ℱ.∘' ftx') ℰ.≡[]⟨ apd (λ _ f' → ff'⁻¹ (ffx' ℱ.∘' f')) (ℱ.idl' ftx') ⟩ - ff'⁻¹ (ffx' ℱ.∘' ftx') ℰ.≡[]⟨ apd (λ _ → ff'⁻¹) (f*x'-iso.invr') ⟩ - ff'⁻¹ ℱ.id' ℰ.≡[]˘⟨ apd (λ _ → ff'⁻¹) (F' .F-id') ⟩ - ff'⁻¹ (F'.₁' ℰ.id') ℰ.≡[]⟨ η[] ℰ.id' ⟩ - ℰ.id' ℰ.∎[] + ff'⁻¹ (ffx' ℱ.∘' ⌜ ℱ.id' ℱ.∘' ftx' ⌝) ℰ.≡[]⟨ apd! (ℱ.idl' ftx') ⟩ + ff'⁻¹ ⌜ ffx' ℱ.∘' ftx' ⌝ ℰ.≡[]⟨ apd! (f*x'-iso.invr') ⟩ + ff'⁻¹ ⌜ ℱ.id' ⌝ ℰ.≡[]˘⟨ apd¡ (F' .F-id') ⟩ + ff'⁻¹ (F'.₁' ℰ.id') ℰ.≡[]⟨ η[] ℰ.id' ⟩ + ℰ.id' ℰ.∎[] where open Σ (eso' x') renaming (fst to f*x' ; snd to f*x'-iso) module f*x'-iso = ℱ._≅[_]_ f*x'-iso @@ -253,14 +253,14 @@ surjectivity to define `F'⁻¹`{.Agda}: F'⁻¹ .F-∘' {a' = x'} {y'} {z'} {f'} {g'} = ff[]→faithful[] F' ff' $ ℱ.begin[] F'.₁' (ff'⁻¹ (ffz' ℱ.∘' (f' ℱ.∘' g') ℱ.∘' ftx')) ℱ.≡[]⟨ ε[] (ffz' ℱ.∘' (f' ℱ.∘' g') ℱ.∘' ftx') ⟩ - ffz' ℱ.∘' (f' ℱ.∘' g') ℱ.∘' ftx' ℱ.≡[]˘⟨ apd (λ _ → ffz' ℱ.∘'_) (ℱ.assoc' f' g' ftx') ⟩ - ffz' ℱ.∘' f' ℱ.∘' g' ℱ.∘' ftx' ℱ.≡[]˘⟨ apd (λ _ h' → ffz' ℱ.∘' f' ℱ.∘' h') (ℱ.idl' (g' ℱ.∘' ftx')) ⟩ - ffz' ℱ.∘' f' ℱ.∘' ℱ.id' ℱ.∘' g' ℱ.∘' ftx' ℱ.≡[]˘⟨ apd (λ _ h' → ffz' ℱ.∘' f' ℱ.∘' h' ℱ.∘' g' ℱ.∘' ftx') (f*y'-iso .ℱ.invl') ⟩ - ffz' ℱ.∘' f' ℱ.∘' (fty' ℱ.∘' ffy') ℱ.∘' g' ℱ.∘' ftx' ℱ.≡[]˘⟨ apd (λ _ h' → ffz' ℱ.∘' f' ℱ.∘' h') (ℱ.assoc' fty' ffy' (g' ℱ.∘' ftx')) ⟩ - ffz' ℱ.∘' f' ℱ.∘' fty' ℱ.∘' (ffy' ℱ.∘' g' ℱ.∘' ftx') ℱ.≡[]⟨ apd (λ _ → ffz' ℱ.∘'_) (ℱ.assoc' f' fty' (ffy' ℱ.∘' g' ℱ.∘' ftx'))⟩ + ffz' ℱ.∘' ⌜ (f' ℱ.∘' g') ℱ.∘' ftx' ⌝ ℱ.≡[]˘⟨ apd¡ (ℱ.assoc' f' g' ftx') ⟩ + ffz' ℱ.∘' f' ℱ.∘' ⌜ g' ℱ.∘' ftx' ⌝ ℱ.≡[]˘⟨ apd¡ (ℱ.idl' (g' ℱ.∘' ftx')) ⟩ + ffz' ℱ.∘' f' ℱ.∘' ⌜ ℱ.id' ⌝ ℱ.∘' g' ℱ.∘' ftx' ℱ.≡[]˘⟨ apd¡ (f*y'-iso .ℱ.invl') ⟩ + ffz' ℱ.∘' f' ℱ.∘' ⌜ (fty' ℱ.∘' ffy') ℱ.∘' g' ℱ.∘' ftx' ⌝ ℱ.≡[]˘⟨ apd¡ (ℱ.assoc' fty' ffy' (g' ℱ.∘' ftx')) ⟩ + ffz' ℱ.∘' ⌜ f' ℱ.∘' fty' ℱ.∘' (ffy' ℱ.∘' g' ℱ.∘' ftx') ⌝ ℱ.≡[]⟨ apd! (ℱ.assoc' f' fty' (ffy' ℱ.∘' g' ℱ.∘' ftx'))⟩ ffz' ℱ.∘' (f' ℱ.∘' fty') ℱ.∘' (ffy' ℱ.∘' g' ℱ.∘' ftx') ℱ.≡[]⟨ ℱ.assoc' ffz' (f' ℱ.∘' fty') (ffy' ℱ.∘' g' ℱ.∘' ftx') ⟩ - (ffz' ℱ.∘' f' ℱ.∘' fty') ℱ.∘' (ffy' ℱ.∘' g' ℱ.∘' ftx') ℱ.≡[]˘⟨ apd (λ _ → ℱ._∘' (ffy' ℱ.∘' g' ℱ.∘' ftx')) (ε[] (ffz' ℱ.∘' f' ℱ.∘' fty')) ⟩ - F'.₁' (ff'⁻¹ (ffz' ℱ.∘' f' ℱ.∘' fty')) ℱ.∘' (ffy' ℱ.∘' g' ℱ.∘' ftx') ℱ.≡[]˘⟨ apd (λ _ → F'.₁' (ff'⁻¹ (ffz' ℱ.∘' f' ℱ.∘' fty')) ℱ.∘'_) (ε[] (ffy' ℱ.∘' g' ℱ.∘' ftx')) ⟩ + ⌜ ffz' ℱ.∘' f' ℱ.∘' fty' ⌝ ℱ.∘' (ffy' ℱ.∘' g' ℱ.∘' ftx') ℱ.≡[]˘⟨ apd¡ (ε[] (ffz' ℱ.∘' f' ℱ.∘' fty')) ⟩ + F'.₁' (ff'⁻¹ (ffz' ℱ.∘' f' ℱ.∘' fty')) ℱ.∘' ⌜ ffy' ℱ.∘' g' ℱ.∘' ftx' ⌝ ℱ.≡[]˘⟨ apd¡ (ε[] (ffy' ℱ.∘' g' ℱ.∘' ftx')) ⟩ F'.₁' (ff'⁻¹ (ffz' ℱ.∘' f' ℱ.∘' fty')) ℱ.∘' F'.₁' (ff'⁻¹ (ffy' ℱ.∘' g' ℱ.∘' ftx')) ℱ.≡[]˘⟨ F' .F-∘' {f' = (ff'⁻¹ (ffz' ℱ.∘' f' ℱ.∘' fty'))} {g' = (ff'⁻¹ (ffy' ℱ.∘' g' ℱ.∘' ftx'))}⟩ F'.₁' (ff'⁻¹ (ffz' ℱ.∘' f' ℱ.∘' fty') ℰ.∘' ff'⁻¹ (ffy' ℱ.∘' g' ℱ.∘' ftx')) ℱ.∎[] where diff --git a/src/Cat/Displayed/Morphism.lagda.md b/src/Cat/Displayed/Morphism.lagda.md index 2ce1e4b34..c073f638a 100644 --- a/src/Cat/Displayed/Morphism.lagda.md +++ b/src/Cat/Displayed/Morphism.lagda.md @@ -733,7 +733,7 @@ abstract → f' .from' ≡[ inverse-unique₀ f g r ] g' .from' inverse-unique₀' f' g' r' = begin[] f' .from' ≡[]˘⟨ apd (λ _ → f' .from' ∘'_) (g' .invl') ∙[] idr' _ ⟩ - f' .from' ∘' g' .to' ∘' g' .from' ≡[]⟨ assoc' (f' .from') (g' .to') (g' .from') ⟩ + f' .from' ∘' g' .to' ∘' g' .from' ≡[]⟨ assoc' (f' .from') (g' .to') (g' .from') ⟩ (f' .from' ∘' g' .to') ∘' g' .from' ≡[]⟨ (apd (λ _ → _∘' g' .from') (apd (λ _ → f' .from' ∘'_) (symP r') ∙[] f' .invr')) ∙[] idl' _ ⟩ g' .from' ∎[] ``` diff --git a/src/Cat/Functor/Coherence.agda b/src/Cat/Functor/Coherence.agda index 80eb8f5d1..73e642023 100644 --- a/src/Cat/Functor/Coherence.agda +++ b/src/Cat/Functor/Coherence.agda @@ -43,7 +43,7 @@ instance private get-dual : Term → TC Name get-dual T = resetting do - (mv , _) ← new-meta' (def (quote Dualises) [ argN T ]) + meta mv _ ← new-meta' (def (quote Dualises) [ argN T ]) (qn ∷ []) ← get-instances mv where _ → typeError [ "Don't know how to dualise type " , termErr T ] unquoteTC =<< normalise (def (quote dualiser) [ argN qn ])