diff --git a/src/1Lab/Extensionality.agda b/src/1Lab/Extensionality.agda index de49a0498..cc7edf85f 100644 --- a/src/1Lab/Extensionality.agda +++ b/src/1Lab/Extensionality.agda @@ -149,12 +149,30 @@ Extensional-Π ⦃ sb ⦄ .reflᵉ f x = reflᵉ sb (f x) Extensional-Π ⦃ sb ⦄ .idsᵉ .to-path h = funext λ i → sb .idsᵉ .to-path (h i) Extensional-Π ⦃ sb ⦄ .idsᵉ .to-path-over h = funextP λ i → sb .idsᵉ .to-path-over (h i) +Extensional-Π' + : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'} + → ⦃ sb : ∀ {x} → Extensional (B x) ℓr ⦄ + → Extensional ({x : A} → B x) (ℓ ⊔ ℓr) +Extensional-Π' ⦃ sb ⦄ .Pathᵉ f g = ∀ {x} → Pathᵉ sb (f {x}) (g {x}) +Extensional-Π' ⦃ sb ⦄ .reflᵉ f = reflᵉ sb f +Extensional-Π' ⦃ sb ⦄ .idsᵉ .to-path h i {x} = sb .idsᵉ .to-path (h {x}) i +Extensional-Π' ⦃ sb ⦄ .idsᵉ .to-path-over h i {x} = sb .idsᵉ .to-path-over (h {x}) i + Extensional-→ : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'} → ⦃ sb : Extensional B ℓr ⦄ → Extensional (A → B) (ℓ ⊔ ℓr) Extensional-→ ⦃ sb ⦄ = Extensional-Π ⦃ λ {_} → sb ⦄ +Extensional-uncurry + : ∀ {ℓ ℓ' ℓ'' ℓr} {A : Type ℓ} {B : A → Type ℓ'} {C : Type ℓ''} + → ⦃ sb : Extensional ((x : A) → B x → C) ℓr ⦄ + → Extensional (Σ A B → C) ℓr +Extensional-uncurry ⦃ sb ⦄ .Pathᵉ f g = sb .Pathᵉ (curry f) (curry g) +Extensional-uncurry ⦃ sb ⦄ .reflᵉ f = sb .reflᵉ (curry f) +Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path h i (a , b) = sb .idsᵉ .to-path h i a b +Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path-over h = sb .idsᵉ .to-path-over h + Extensional-× : ∀ {ℓ ℓ' ℓr ℓs} {A : Type ℓ} {B : Type ℓ'} → ⦃ sa : Extensional A ℓr ⦄ @@ -175,11 +193,21 @@ instance → Extensionality (A → B) extensionality-fun = record { lemma = quote Extensional-→ } + extensionality-uncurry + : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : Type ℓ''} + → Extensionality (Σ A B → C) + extensionality-uncurry = record { lemma = quote Extensional-uncurry } + extensionality-Π : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → Extensionality ((x : A) → B x) extensionality-Π = record { lemma = quote Extensional-Π } + extensionality-Π' + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} + → Extensionality ({x : A} → B x) + extensionality-Π' = record { lemma = quote Extensional-Π' } + extensionality-× : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → Extensionality (A × B) diff --git a/src/1Lab/Underlying.agda b/src/1Lab/Underlying.agda index 9111dd97e..a92ce2f9e 100644 --- a/src/1Lab/Underlying.agda +++ b/src/1Lab/Underlying.agda @@ -127,3 +127,10 @@ instance Funlike-Fun = record { _#_ = _$_ } + +-- Generalised "sections" (e.g. of a presheaf) notation. +_ʻ_ + : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {F : A → B → Type ℓ''} + → ⦃ _ : Funlike F ⦄ {a : A} {b : B} ⦃ _ : Underlying ⌞ b ⌟ ⦄ + → F a b → ⌞ a ⌟ → Type _ +F ʻ x = ⌞ F # x ⌟ diff --git a/src/Algebra/Group/Ab/Abelianisation.lagda.md b/src/Algebra/Group/Ab/Abelianisation.lagda.md index 6741fd9fe..eaa3194fe 100644 --- a/src/Algebra/Group/Ab/Abelianisation.lagda.md +++ b/src/Algebra/Group/Ab/Abelianisation.lagda.md @@ -222,5 +222,5 @@ make-free-abelian {ℓ} = go where go .universal f .preserves .is-group-hom.pres-⋆ = Coeq-elim-prop₂ (λ _ _ → hlevel!) λ _ _ → f .preserves .is-group-hom.pres-⋆ _ _ go .commutes f = trivial! - go .unique p = ext (Coeq-elim-prop (λ _ → hlevel!) (λ x → p #ₚ x)) + go .unique p = ext (p #ₚ_) ``` diff --git a/src/Algebra/Group/Subgroup.lagda.md b/src/Algebra/Group/Subgroup.lagda.md index d39bfc81b..b3fbffa01 100644 --- a/src/Algebra/Group/Subgroup.lagda.md +++ b/src/Algebra/Group/Subgroup.lagda.md @@ -578,8 +578,8 @@ predicate $\rm{inc}(x) = \rm{inc}(0)$ recovers the subgroup $H$; And from .hom (x , p) = x , quot (subst (_∈ H) (sym idr ∙ ap (_ ⋆_) (sym inv-unit)) p) from .preserves .is-group-hom.pres-⋆ _ _ = Σ-prop-path (λ _ → squash _ _) refl - il = ext λ x → Σ-prop-path (λ _ → H _ .is-tr) refl - ir = ext λ x → Σ-prop-path (λ _ → squash _ _) refl + il = ext λ x x∈H → Σ-prop-path! refl + ir = ext λ x x∈H → Σ-prop-path! refl ``` To show that these are equal as subgroups of $G$, we must show that the diff --git a/src/Cat/Base.lagda.md b/src/Cat/Base.lagda.md index d08d5a383..9bd50827e 100644 --- a/src/Cat/Base.lagda.md +++ b/src/Cat/Base.lagda.md @@ -5,6 +5,7 @@ open import 1Lab.Reflection.Record open import 1Lab.HLevel.Retracts open import 1Lab.HLevel.Universe open import 1Lab.Extensionality +open import 1Lab.Underlying open import 1Lab.Rewrite open import 1Lab.HLevel open import 1Lab.Equiv @@ -605,5 +606,11 @@ instance → Extensionality (F => G) extensionality-natural-transformation = record { lemma = quote Extensional-natural-transformation } + + Underlying-Precategory : ∀ {o ℓ} → Underlying (Precategory o ℓ) + Underlying-Precategory = record { ⌞_⌟ = Precategory.Ob } + + Funlike-Functor : ∀ {o ℓ o' ℓ'} → Funlike (Functor {o} {ℓ} {o'} {ℓ'}) + Funlike-Functor = record { _#_ = Functor.F₀ } ``` --> diff --git a/src/Cat/CartesianClosed/Instances/PSh.agda b/src/Cat/CartesianClosed/Instances/PSh.agda index 10a734907..709014c97 100644 --- a/src/Cat/CartesianClosed/Instances/PSh.agda +++ b/src/Cat/CartesianClosed/Instances/PSh.agda @@ -78,7 +78,7 @@ module _ {o ℓ κ} {C : Precategory o ℓ} where pb .p₁ .is-natural _ _ _ = refl pb .p₂ .η x (a , b , _) = b pb .p₂ .is-natural _ _ _ = refl - pb .has-is-pb .square = ext λ _ (_ , _ , p) → p + pb .has-is-pb .square = ext λ _ _ _ p → p pb .has-is-pb .universal path .η idx arg = _ , _ , (path ηₚ idx $ₚ arg) pb .has-is-pb .universal {p₁' = p₁'} {p₂'} path .is-natural x y f = funext λ x → pb-path (happly (p₁' .is-natural _ _ _) _) (happly (p₂' .is-natural _ _ _) _) @@ -197,9 +197,9 @@ module _ {κ} {C : Precategory κ κ} where F .F₁ f nt .η i (g , x) = nt .η i (f C.∘ g , x) F .F₁ f nt .is-natural x y g = funext λ o → ap (nt .η y) (Σ-pathp (C.assoc _ _ _) refl) ∙ happly (nt .is-natural _ _ _) _ - F .F-id = ext λ f i (g , x) → + F .F-id = ext λ f i g x → ap (f .η i) (Σ-pathp (C.idl _) refl) - F .F-∘ f g = ext λ h i (j , x) → + F .F-∘ f g = ext λ h i j x → ap (h .η i) (Σ-pathp (sym (C.assoc _ _ _)) refl) func : Functor (PSh κ C) (PSh κ C) @@ -217,13 +217,13 @@ module _ {κ} {C : Precategory κ κ} where funext λ _ → Σ-pathp (happly (x .F-∘ _ _) _) refl adj .unit .η x .is-natural _ _ _ = funext λ _ → Nat-path λ _ → funext λ _ → Σ-pathp (sym (happly (x .F-∘ _ _) _)) refl - adj .unit .is-natural x y f = ext λ _ _ _ _ → sym (f .is-natural _ _ _ $ₚ _) , refl + adj .unit .is-natural x y f = ext λ _ _ _ _ _ → sym (f .is-natural _ _ _ $ₚ _) , refl adj .counit .η _ .η _ x = x .fst .η _ (C.id , x .snd) adj .counit .η _ .is-natural x y f = funext λ h → ap (h .fst .η _) (Σ-pathp C.id-comm refl) ∙ happly (h .fst .is-natural _ _ _) _ adj .counit .is-natural x y f = Nat-path λ x → refl - adj .zig {A} = ext λ x _ → happly (F-id A) _ , refl - adj .zag {A} = ext λ _ x i (f , g) j → x .η i (C.idr f j , g) + adj .zig {A} = ext λ x _ _ → happly (F-id A) _ , refl + adj .zag {A} = ext λ _ x i f g j → x .η i (C.idr f j , g) cc : Cartesian-closed (PSh κ C) (PSh-products {C = C}) (PSh-terminal {C = C}) cc = product-adjoint→cartesian-closed (PSh κ C) diff --git a/src/Cat/Diagram/Coend/Sets.lagda.md b/src/Cat/Diagram/Coend/Sets.lagda.md index fa5e89d36..2c17377cf 100644 --- a/src/Cat/Diagram/Coend/Sets.lagda.md +++ b/src/Cat/Diagram/Coend/Sets.lagda.md @@ -75,7 +75,6 @@ taken the right coequaliser. ```agda Set-coend : Coend F Set-coend = coend where - universal-cowedge : Cowedge F universal-cowedge .nadir = el! (Coeq dimapl dimapr) universal-cowedge .ψ X Fxx = inc (X , Fxx) @@ -88,15 +87,16 @@ project out the bundled up object from the coend and feed that to the family associated to the cowedge `W`. ```agda + factoring : (W : Cowedge F) → Coeq dimapl dimapr → ⌞ W .nadir ⌟ + factoring W (inc (o , x)) = W .ψ o x + factoring W (glue (X , Y , f , Fxy) i) = W .extranatural f i Fxy + factoring W (squash x y p q i j) = W .nadir .is-tr (factoring W x) (factoring W y) (λ i → factoring W (p i)) (λ i → factoring W (q i)) i j + coend : Coend F coend .cowedge = universal-cowedge - coend .factor W = - Coeq-rec hlevel! (λ ∫F → W .ψ (∫F .fst) (∫F .snd)) λ where - (X , Y , f , Fxy) → happly (W .extranatural f) Fxy + coend .factor W = factoring W coend .commutes = refl - coend .unique {W = W} p = - funext $ Coeq-elim hlevel! (λ ∫F → happly p (∫F .snd)) λ where - (X , Y , f , Fxy) → is-set→squarep (λ _ _ → is-tr (W .nadir)) _ _ _ _ + coend .unique {W = W} p = ext λ X x → p #ₚ x ``` This construction is actually functorial! Given any functor @@ -118,14 +118,6 @@ module _ {o ℓ} {𝒞 : Precategory o ℓ} where (ap (λ ϕ → inc (X , ϕ)) $ happly (α .is-natural (X , Y) (X , X) (id , f)) Fxy) ·· glue (X , Y , f , α .η (X , Y) Fxy) ·· (sym $ ap (λ ϕ → inc (Y , ϕ)) $ happly (α .is-natural (X , Y) (Y , Y) (f , id)) Fxy) - Coends .F-id = - funext $ Coeq-elim - (λ _ → hlevel!) - (λ _ → refl) - (λ _ → is-set→squarep (λ _ _ → squash) _ _ _ _) - Coends .F-∘ f g = - funext $ Coeq-elim - (λ _ → hlevel!) - (λ _ → refl) - (λ _ → is-set→squarep (λ _ _ → squash) _ _ _ _) + Coends .F-id = trivial! + Coends .F-∘ f g = trivial! ``` diff --git a/src/Cat/Displayed/Doctrine/Logic.lagda.md b/src/Cat/Displayed/Doctrine/Logic.lagda.md index cfd1663dd..26a2612ff 100644 --- a/src/Cat/Displayed/Doctrine/Logic.lagda.md +++ b/src/Cat/Displayed/Doctrine/Logic.lagda.md @@ -6,7 +6,7 @@ open import Cat.Diagram.Pullback open import Cat.Diagram.Terminal open import Cat.Diagram.Product open import Cat.Displayed.Base -open import Cat.Prelude +open import Cat.Prelude hiding (_ʻ_) import Cat.Displayed.Reasoning as Disp import Cat.Reasoning as Cat diff --git a/src/Cat/Instances/Sets/CartesianClosed.lagda.md b/src/Cat/Instances/Sets/CartesianClosed.lagda.md index d3de9d03a..28c387f73 100644 --- a/src/Cat/Instances/Sets/CartesianClosed.lagda.md +++ b/src/Cat/Instances/Sets/CartesianClosed.lagda.md @@ -52,9 +52,9 @@ module _ {A B : Set ℓ} (func : ∣ A ∣ → ∣ B ∣) where diff --git a/src/Cat/Instances/Slice.lagda.md b/src/Cat/Instances/Slice.lagda.md index 4448fc17e..14b276095 100644 --- a/src/Cat/Instances/Slice.lagda.md +++ b/src/Cat/Instances/Slice.lagda.md @@ -567,11 +567,7 @@ dependent function is automatically a natural transformation. diff --git a/src/Cat/Instances/Slice/Presheaf.lagda.md b/src/Cat/Instances/Slice/Presheaf.lagda.md index e034ade7e..fbd481f48 100644 --- a/src/Cat/Instances/Slice/Presheaf.lagda.md +++ b/src/Cat/Instances/Slice/Presheaf.lagda.md @@ -153,7 +153,7 @@ without comment. rinv : is-right-inverse inv (F₁ slice→total) rinv nt = ext λ where - o (z , p) → Σ-prop-path (λ _ → P.₀ _ .is-tr _ _) + o z p → Σ-prop-path (λ _ → P.₀ _ .is-tr _ _) (λ i → nt .η (elem (o .ob) (p i)) (z , (λ j → p (i ∧ j))) .fst) linv : is-left-inverse inv (F₁ slice→total) diff --git a/src/Cat/Monoidal/Instances/Day.lagda.md b/src/Cat/Monoidal/Instances/Day.lagda.md new file mode 100644 index 000000000..d076058a1 --- /dev/null +++ b/src/Cat/Monoidal/Instances/Day.lagda.md @@ -0,0 +1,357 @@ + + +```agda +module Cat.Monoidal.Instances.Day + {ℓ} {C : Precategory ℓ ℓ} (cmon : Monoidal-category C) + where +``` + +```agda +open Monoidal-category cmon +private module ⊗ = Fr -⊗- + +open make-natural-iso +open Cowedge +open Functor +open Cat C +open _=>_ +``` + +# The Day convolution product + +```agda +module Day (X Y : ⌞ PSh ℓ C ⌟) where + Day-diagram : Ob → Functor ((C ×ᶜ C) ^op ×ᶜ (C ×ᶜ C)) (Sets ℓ) + ∣ Day-diagram c .F₀ ((c₁⁻ , c₂⁻) , c₁⁺ , c₂⁺) ∣ = Hom c (c₁⁺ ⊗ c₂⁺) × (X ʻ c₁⁻) × (Y ʻ c₂⁻) + Day-diagram c .F₀ ((c₁⁻ , c₂⁻) , c₁⁺ , c₂⁺) .is-tr = hlevel! + + Day-diagram c .F₁ ((f⁻ , g⁻) , f⁺ , g⁺) (h , x , y) = (f⁺ ⊗₁ g⁺) ∘ h , X .F₁ f⁻ x , Y .F₁ g⁻ y + + Day-diagram c .F-id = ext λ h x y → eliml (-⊗- .F-id) , X .F-id #ₚ x , Y .F-id #ₚ y + Day-diagram c .F-∘ f g = ext λ h x y → pushl (-⊗- .F-∘ _ _) , X .F-∘ _ _ #ₚ _ , Y .F-∘ _ _ #ₚ _ + + opaque + Day-coend : (c : Ob) → Coend (Day-diagram c) + Day-coend c = Set-coend (Day-diagram c) + + private module Day c = Coend (Day-coend c) + open Day using (nadir) public + + opaque + unfolding Day-coend + + day : {i a b : Ob} (h : Hom i (a ⊗ b)) (x : X ʻ a) (y : Y ʻ b) → ⌞ Day.nadir i ⌟ + day h x y = inc ((_ , _) , h , x , y) + + day-ap + : {i a b : Ob} {h h' : Hom i (a ⊗ b)} {x x' : X ʻ a} {y y' : Y ʻ b} + → h ≡ h' → x ≡ x' → y ≡ y' → day h x y ≡ day h' x' y' + day-ap {a = a} {b} p q r i = inc ((a , b) , p i , q i , r i) + + day-apₘ : ∀ {i a b} {h h' : Hom i (a ⊗ b)} {x y} → h ≡ h' → day h x y ≡ day h' x y + day-apₘ p = day-ap p refl refl + + day-glue + : {i a b a' b' : Ob} {f : Hom a' a} {g : Hom b' b} {h : Hom i (a' ⊗ b')} {x : X ʻ a} {y : Y ʻ b} + → {fgh : Hom i (a ⊗ b)} (p : fgh ≡ (f ⊗₁ g) ∘ h) + → day fgh x y ≡ day h (X .F₁ f x) (Y .F₁ g y) + day-glue {i} {a} {b} {a'} {b'} {f} {g} {h} {x} {y} {fgh} p = + inc ((a , b) , fgh , x , y) ≡⟨ day-ap p (sym (X .F-id) #ₚ x) (sym (Y .F-id) #ₚ y) ⟩ + inc ((a , b) , (f ⊗₁ g) ∘ h , X .F₁ id x , Y .F₁ id y) ≡⟨ Coeq.glue {f = dimapl (Day-diagram i)} {g = dimapr (Day-diagram i)} ((a , b) , (a' , b') , (f , g) , h , x , y) ⟩ + inc ((a' , b') , (id ⊗₁ id) ∘ h , X .F₁ f x , Y .F₁ g y) ≡⟨ day-apₘ (eliml ⊗.F-id) ⟩ + inc ((a' , b') , h , X .F₁ f x , Y .F₁ g y) ∎ + + factor : ∀ {i} (W : Cowedge (Day-diagram i)) → ⌞ Day.nadir i ⌟ → ⌞ W .nadir ⌟ + factor W = Day.factor _ W + + factor-day + : ∀ {i a b} {W : Cowedge (Day-diagram i)} {h : Hom i (a ⊗ b)} {x : X ʻ a} {y : Y ʻ b} + → factor W (day h x y) ≡rw W .ψ (a , b) (h , x , y) + factor-day = idrw + + {-# REWRITE factor-day #-} + + Extensional-day-map + : ∀ {i ℓ' ℓr} {C : Type ℓ'} {@(tactic hlevel-tactic-worker) c-set : is-set C} + → ⦃ sf : ∀ {a b} → Extensional ((h : Hom i (a ⊗ b)) (x : X ʻ a) (y : Y ʻ b) → C) ℓr ⦄ + → Extensional (⌞ Day.nadir i ⌟ → C) (ℓ ⊔ ℓr) + Extensional-day-map {i} {C = C} {c-set} ⦃ sf ⦄ = done where + instance + _ : H-Level C 2 + _ = basic-instance 2 c-set + + T : Type _ + T = {a b : Ob} (h : Hom i (a ⊗ b)) (x : X ʻ a) (y : Y ʻ b) → C + + unday : (⌞ Day.nadir i ⌟ → C) → T + unday f h x y = f (day h x y) + + opaque + unfolding Day-coend day + + to-p : ∀ {f g} → Path T (unday f) (unday g) → f ≡ g + to-p p = ext λ (a , b) h x y i → p i {a} {b} h x y + + done : Extensional (⌞ Day.nadir i ⌟ → C) _ + done = injection→extensional (hlevel 2) to-p (Extensional-Π' ⦃ Extensional-Π' ⦃ sf ⦄ ⦄) + + private instance + _ : ∀ {i ℓ'} {C : Type ℓ'} → Extensionality (⌞ Day.nadir i ⌟ → C) + _ = record { lemma = quote Extensional-day-map } + + day-swap + : ∀ {i a b a' b'} {f : Hom a' a} {g : Hom b' b} {h : Hom i (a' ⊗ b')} + {a'' b''} {f' : Hom a'' a} {g' : Hom b'' b} {h' : Hom i (a'' ⊗ b'')} + {x : X ʻ a} {y : Y ʻ b} + → (f ⊗₁ g) ∘ h ≡ (f' ⊗₁ g') ∘ h' + → day h (X .F₁ f x) (Y .F₁ g y) ≡ day h' (X .F₁ f' x) (Y .F₁ g' y) + day-swap p = sym (day-glue refl) ·· day-apₘ p ·· day-glue refl + + Day-cowedge : ∀ {x} {y} → Hom y x → Cowedge (Day-diagram x) + Day-cowedge {y = y} h .nadir = Day.nadir y + Day-cowedge h .ψ (a , b) (f , x , y) = day (f ∘ h) x y + Day-cowedge h .extranatural {a , b} {a' , b'} (f , g) = funext λ (i , x , y) → + day (((f ⊗₁ g) ∘ i) ∘ h) (X .F₁ id x) (Y .F₁ id y) ≡⟨ day-ap refl (X .F-id #ₚ x) (Y .F-id #ₚ y) ⟩ + day (((f ⊗₁ g) ∘ i) ∘ h) x y ≡⟨ day-glue (sym (assoc _ _ _)) ⟩ + day (i ∘ h) (X .F₁ f x) (Y .F₁ g y) ≡⟨ day-apₘ (introl ⊗.F-id ∙ assoc _ _ _) ⟩ + day (((id ⊗₁ id) ∘ i) ∘ h) (X .F₁ f x) (Y .F₁ g y) ∎ + + Day : ⌞ PSh ℓ C ⌟ + Day .F₀ c = Day.nadir c + Day .F₁ {x} {y} h v = factor (Day-cowedge h) v + Day .F-id = ext λ h x y → day-apₘ (idr h) + Day .F-∘ f g = ext λ h x y → day-apₘ (assoc h g f) + + +module _ {X Y} where + open Day X Y + using (day ; day-ap ; day-apₘ ; day-swap ; Extensional-day-map ; day-glue) + renaming (factor to Day-rec) + public + +instance + extensionality-day-map + : ∀ {X Y i ℓ'} {C : Type ℓ'} → Extensionality (⌞ Day.nadir X Y i ⌟ → C) + extensionality-day-map = record { lemma = quote Extensional-day-map } + +open Day using (Day ; Day-diagram) + +Day-bifunctor-cowedge + : ∀ {X Y X' Y' : ⌞ PSh ℓ C ⌟} {i} + → X => X' + → Y => Y' + → Cowedge (Day-diagram X Y i) +Day-bifunctor-cowedge {X} {Y} {X'} {Y'} {i} F G = go where + private module D = Day X' Y' + go : Cowedge (Day-diagram X Y i) + go .nadir = D.nadir i + go .ψ c (h , x , y) = D.day h (F .η _ x) (G .η _ y) + go .extranatural (f , g) = ext λ h x y → + D.day ((f ⊗₁ g) ∘ h) (F .η _ (X .F₁ id x)) (G .η _ (Y .F₁ id y)) ≡⟨ D.day-ap refl (F .is-natural _ _ id #ₚ _) (G .is-natural _ _ id #ₚ _) ⟩ + D.day ((f ⊗₁ g) ∘ h) (X' .F₁ id (F .η _ x)) (Y' .F₁ id (G .η _ y)) ≡⟨ D.day-swap (extendl (eliml ⊗.F-id ∙ intror ⊗.F-id)) ⟩ + D.day ((id ⊗₁ id) ∘ h) (X' .F₁ f (F .η _ x)) (Y' .F₁ g (G .η _ y)) ≡˘⟨ D.day-ap refl (F .is-natural _ _ f #ₚ _) (G .is-natural _ _ g #ₚ _) ⟩ + D.day ((id ⊗₁ id) ∘ h) (F .η _ (X .F₁ f x)) (G .η _ (Y .F₁ g y)) ∎ + +Day-map : ∀ {X X' Y Y'} (F : X => X') (G : Y => Y') → Day X Y => Day X' Y' +Day-map F G .η i = Day-rec (Day-bifunctor-cowedge F G) +Day-map F G .is-natural x y f = trivial! + +Day-bifunctor : Functor (PSh ℓ C ×ᶜ PSh ℓ C) (PSh ℓ C) +Day-bifunctor .F₀ (X , Y) = Day X Y +Day-bifunctor .F₁ (F , G) = Day-map F G +Day-bifunctor .F-id = trivial! +Day-bifunctor .F-∘ f g = trivial! + +module _ (X : ⌞ PSh ℓ C ⌟) where + idr-to-cowedge : ∀ x → Cowedge (Day-diagram X (よ₀ C Unit) x) + idr-to-cowedge i .nadir = X # i + idr-to-cowedge i .ψ (a , b) (h , x , y) = X .F₁ (ρ← ∘ (id ⊗₁ y) ∘ h) x + idr-to-cowedge i .extranatural {a , b} {a' , b'} (f , g) = ext λ h x y → + X .F₁ (ρ← ∘ (id ⊗₁ y ∘ id) ∘ (f ⊗₁ g) ∘ h) (X .F₁ id x) ≡⟨ ap₂ (X .F₁) (ap (ρ← ∘_) (⊗.pulll (ap₂ _,_ (idl f) (ap (_∘ g) (idr y))))) refl ⟩ + X .F₁ (ρ← ∘ (f ⊗₁ y ∘ g) ∘ h) (X .F₁ id x) ≡⟨ ap₂ (X .F₁) (ap (ρ← ∘_) (⊗.pushl (ap₂ _,_ (intror refl) (introl refl)))) refl ⟩ + X .F₁ (ρ← ∘ (f ⊗₁ id) ∘ (id ⊗₁ y ∘ g) ∘ h) (X .F₁ id x) ≡⟨ ap₂ (X .F₁) (extendl (unitor-r .Isoⁿ.from .is-natural a a' f)) refl ⟩ + X .F₁ (f ∘ ρ← ∘ (id ⊗₁ y ∘ g) ∘ h) (X .F₁ id x) ≡⟨ X .F-∘ _ _ #ₚ _ ⟩ + X .F₁ (ρ← ∘ (id ⊗₁ y ∘ g) ∘ h) (X .F₁ f (X .F₁ id x)) ≡⟨ ap₂ (X .F₁) (ap (ρ← ∘_) (ap₂ _∘_ refl (introl ⊗.F-id))) (ap (X .F₁ f) (X .F-id #ₚ x)) ⟩ + X .F₁ (ρ← ∘ (id ⊗₁ y ∘ g) ∘ (id ⊗₁ id) ∘ h) (X .F₁ f x) ∎ + + Day-idr : Day X (よ₀ C Unit) ≅ⁿ X + Day-idr = to-natural-iso mk where + mk : make-natural-iso (Day X (よ₀ C Unit)) X + mk .eta x = Day-rec (idr-to-cowedge x) + mk .inv x a = day ρ→ a id + mk .eta∘inv x = ext λ a → ap₂ (X .F₁) (ap (ρ← ∘_) (eliml ⊗.F-id) ∙ unitor-r .Isoⁿ.invr ηₚ _) refl ∙ (X .F-id #ₚ a) + mk .inv∘eta i = ext λ h x y → + day ρ→ (X .F₁ (ρ← ∘ (id ⊗₁ y) ∘ h) x) id ≡⟨ day-ap refl refl (introl refl) ⟩ + day ρ→ (X .F₁ (ρ← ∘ (id ⊗₁ y) ∘ h) x) (id ∘ id) ≡⟨ day-swap (sym (unitor-r .Isoⁿ.to .is-natural _ _ _) ∙ cancell (unitor-r .Isoⁿ.invl ηₚ _)) ⟩ + day h (X .F₁ id x) (id ∘ y) ≡⟨ day-ap refl (X .F-id #ₚ x) (idl y) ⟩ + day h x y ∎ + mk .natural x y f = ext λ h x y → + X .F₁ f (X .F₁ (ρ← ∘ (id ⊗₁ y) ∘ h) x) ≡⟨ sym (X .F-∘ _ _) #ₚ _ ⟩ + X .F₁ ((ρ← ∘ (id ⊗₁ y) ∘ h) ∘ f) x ≡⟨ ap₂ (X .F₁) (pullr (pullr refl)) refl ⟩ + X .F₁ (ρ← ∘ (id ⊗₁ y) ∘ h ∘ f) x ∎ + +module _ (Y : ⌞ PSh ℓ C ⌟) where + idl-to-cowedge : ∀ x → Cowedge (Day-diagram (よ₀ C Unit) Y x) + idl-to-cowedge i .nadir = Y # i + idl-to-cowedge i .ψ (a , b) (h , x , y) = Y .F₁ (λ← ∘ (x ⊗₁ id) ∘ h) y + idl-to-cowedge i .extranatural {a , b} {a' , b'} (f , g) = ext λ h x y → + ap₂ (Y .F₁) (ap (λ← ∘_) (⊗.extendl (ap₂ _,_ (ap (_∘ f) (idr x) ∙ introl refl) id-comm-sym)) ∙ extendl (unitor-l .Isoⁿ.from .is-natural _ _ _)) (Y .F-id #ₚ y) + ·· (Y .F-∘ _ _ #ₚ y) + ·· ap₂ (Y .F₁) (ap (λ← ∘_) (ap₂ _∘_ refl (introl ⊗.F-id))) refl + + Day-idl : Day (よ₀ C Unit) Y ≅ⁿ Y + Day-idl = to-natural-iso mk where + mk : make-natural-iso (Day (よ₀ C Unit) Y) Y + mk .eta x = Day-rec (idl-to-cowedge x) + mk .inv x a = day λ→ id a + mk .eta∘inv x = ext λ a → ap₂ (Y .F₁) (ap (λ← ∘_) (eliml ⊗.F-id) ∙ unitor-l .Isoⁿ.invr ηₚ _) refl ∙ (Y .F-id #ₚ a) + mk .inv∘eta i = ext λ h x y → + day λ→ id (Y .F₁ (λ← ∘ (x ⊗₁ id) ∘ h) y) ≡⟨ day-ap refl (introl refl) refl ⟩ + day λ→ (id ∘ id) (Y .F₁ (λ← ∘ (x ⊗₁ id) ∘ h) y) ≡⟨ day-swap (sym (unitor-l .Isoⁿ.to .is-natural _ _ _) ∙ cancell (unitor-l .Isoⁿ.invl ηₚ _)) ⟩ + day h (id ∘ x) (Y .F₁ id y) ≡⟨ day-ap refl (idl x) (Y .F-id #ₚ y) ⟩ + day h x y ∎ + mk .natural = λ x y f → ext λ h x y → + Y .F₁ f (Y .F₁ (λ← ∘ (x ⊗₁ id) ∘ h) y) ≡˘⟨ Y .F-∘ _ _ #ₚ _ ⟩ + Y .F₁ ((λ← ∘ (x ⊗₁ id) ∘ h) ∘ f) y ≡⟨ ap₂ (Y .F₁) (pullr (pullr refl)) refl ⟩ + Y .F₁ (λ← ∘ (x ⊗₁ id) ∘ h ∘ f) y ∎ + +module _ (X Y Z : ⌞ PSh ℓ C ⌟) where + assoc-to₀ : ∀ i {a b} (h : Hom i (a ⊗ b)) (z : Z ʻ b) → Cowedge (Day-diagram X Y a) + assoc-to₀ i h z .nadir = Day.nadir X (Day Y Z) i + assoc-to₀ i h z .ψ (a' , b') (h' , x , y) = day (α→ _ _ _ ∘ (h' ⊗₁ id) ∘ h) x (day id y z) + assoc-to₀ i h z .extranatural (f , g) = ext λ h' x y → + day (α→ _ _ _ ∘ ((f ⊗₁ g) ∘ h' ⊗₁ id) ∘ h) (X .F₁ id x) (day id (Y .F₁ id y) z) ≡⟨ day-ap (ap (α→ _ _ _ ∘_) (⊗.pushl (ap₂ _,_ refl (introl refl)))) (X .F-id #ₚ x) (day-ap refl (Y .F-id #ₚ y) refl) ⟩ + day (α→ _ _ _ ∘ ((f ⊗₁ g) ⊗₁ id) ∘ (h' ⊗₁ id) ∘ h) x (day id y z) ≡⟨ day-apₘ (extendl (associator .Isoⁿ.to .is-natural _ _ _)) ⟩ + day ((f ⊗₁ (g ⊗₁ id)) ∘ α→ _ _ _ ∘ (h' ⊗₁ id) ∘ h) x (day id y z) ≡⟨ day-glue refl ⟩ + day (α→ _ _ _ ∘ (h' ⊗₁ id) ∘ h) (X .F₁ f x) (day (id ∘ (g ⊗₁ id)) y z) ≡⟨ day-ap (ap (α→ _ _ _ ∘_) (ap (_∘ h) (ap₂ _⊗₁_ (introl ⊗.F-id) refl))) refl (day-apₘ id-comm-sym ·· day-glue refl ·· day-ap refl refl (Z .F-id #ₚ z)) ⟩ + day (α→ _ _ _ ∘ ((id ⊗₁ id) ∘ h' ⊗₁ id) ∘ h) (X .F₁ f x) (day id (Y .F₁ g y) z) ∎ + + assoc-to-cowedge : ∀ i → Cowedge (Day-diagram (Day X Y) Z i) + assoc-to-cowedge i .nadir = Day.nadir X (Day Y Z) i + assoc-to-cowedge i .ψ (a , b) (h , x , y) = Day-rec (assoc-to₀ i h y) x + assoc-to-cowedge i .extranatural (f , g) = ext λ h h' x y z → + day (α→ _ _ _ ∘ (h' ∘ id ⊗₁ id) ∘ (f ⊗₁ g) ∘ h) x (day id y (Z .F₁ id z)) ≡⟨ day-ap (ap (α→ _ _ _ ∘_) (⊗.extendl (ap₂ _,_ (ap (_∘ f) (idr h') ∙ introl ⊗.F-id) id-comm-sym))) refl (day-ap refl refl (Z .F-id #ₚ z)) ⟩ + day (α→ _ _ _ ∘ ((id ⊗₁ id) ⊗₁ g) ∘ (h' ∘ f ⊗₁ id) ∘ h) x (day id y z) ≡⟨ day-apₘ (extendl (associator .Isoⁿ.to .is-natural _ _ _)) ⟩ + day ((id ⊗₁ (id ⊗₁ g)) ∘ α→ _ _ _ ∘ (h' ∘ f ⊗₁ id) ∘ h) x (day id y z) ≡⟨ day-glue refl ⟩ + day (α→ _ _ _ ∘ (h' ∘ f ⊗₁ id) ∘ h) (X .F₁ id x) (day (id ∘ (id ⊗₁ g)) y z) ≡⟨ day-ap (ap (α→ _ _ _ ∘_) (ap₂ _∘_ refl (introl ⊗.F-id))) (X .F-id #ₚ x) (day-glue id-comm-sym ∙ day-ap refl (Y .F-id #ₚ y) refl) ⟩ + day (α→ _ _ _ ∘ (h' ∘ f ⊗₁ id) ∘ (id ⊗₁ id) ∘ h) x (day id y (Z .F₁ g z)) ∎ + + assoc-from₀ : ∀ i {a b} (h : Hom i (a ⊗ b)) (x : X ʻ a) → Cowedge (Day-diagram Y Z b) + assoc-from₀ i h x .nadir = Day.nadir (Day X Y) Z i + assoc-from₀ i h x .ψ (a' , b') (h' , y , z) = day (α← _ _ _ ∘ (id ⊗₁ h') ∘ h) (day id x y) z + assoc-from₀ i h x .extranatural (f , g) = ext λ h' y z → + day (α← _ _ _ ∘ (id ⊗₁ ((f ⊗₁ g) ∘ h')) ∘ h) (day id x (Y .F₁ id y)) (Z .F₁ id z) ≡⟨ day-ap (extendl (pushr (ap₂ _⊗₁_ (introl refl) refl ∙ ⊗.F-∘ _ _) ·· pullr refl ·· extendl (associator .Isoⁿ.from .is-natural _ _ _))) (day-ap refl refl (Y .F-id #ₚ y)) (Z .F-id #ₚ z) ⟩ + day (((id ⊗₁ f) ⊗₁ g) ∘ (α← _ _ _ ∘ (id ⊗₁ h')) ∘ h) (day id x y) z ≡⟨ day-glue refl ⟩ + day ((α← _ _ _ ∘ (id ⊗₁ h')) ∘ h) (day (id ∘ (id ⊗₁ f)) x y) (Z .F₁ g z) ≡⟨ day-ap (pullr (ap (_∘ h) (ap₂ _⊗₁_ refl (introl ⊗.F-id)))) (day-glue id-comm-sym ∙ day-ap refl (X .F-id #ₚ x) refl) refl ⟩ + day (α← _ _ _ ∘ (id ⊗₁ ((id ⊗₁ id) ∘ h')) ∘ h) (day id x (Y .F₁ f y)) (Z .F₁ g z) ∎ + + assoc-from-cowedge : ∀ i → Cowedge (Day-diagram X (Day Y Z) i) + assoc-from-cowedge i .nadir = Day.nadir (Day X Y) Z i + assoc-from-cowedge i .ψ (a , b) (h , x , y) = Day-rec (assoc-from₀ i h x) y + assoc-from-cowedge i .extranatural (f , g) = ext λ h x h' y z → + day (α← _ _ _ ∘ (id ⊗₁ h' ∘ id) ∘ (f ⊗₁ g) ∘ h) (day id (X .F₁ id x) y) z ≡⟨ day-ap (ap (α← _ _ _ ∘_) (⊗.extendl (ap₂ _,_ id-comm-sym (ap (_∘ g) (idr h') ∙ introl ⊗.F-id)))) (day-ap refl (X .F-id #ₚ _) refl) refl ⟩ + day (α← _ _ _ ∘ (f ⊗₁ (id ⊗₁ id)) ∘ (id ⊗₁ h' ∘ g) ∘ h) (day id x y) z ≡⟨ day-apₘ (extendl (associator .Isoⁿ.from .is-natural _ _ _)) ⟩ + day (((f ⊗₁ id) ⊗₁ id) ∘ α← _ _ _ ∘ (id ⊗₁ h' ∘ g) ∘ h) (day id x y) z ≡⟨ day-glue refl ⟩ + day (α← _ _ _ ∘ (id ⊗₁ h' ∘ g) ∘ h) (day (id ∘ (f ⊗₁ id)) x y) (Z .F₁ id z) ≡⟨ day-ap (ap (α← _ _ _ ∘_) (ap₂ _∘_ refl (introl ⊗.F-id))) (day-glue id-comm-sym ∙ day-ap refl refl (Y .F-id #ₚ y)) (Z .F-id #ₚ z) ⟩ + day (α← _ _ _ ∘ (id ⊗₁ h' ∘ g) ∘ (id ⊗₁ id) ∘ h) (day id (X .F₁ f x) y) z ∎ + + Day-assoc : Day (Day X Y) Z ≅ⁿ Day X (Day Y Z) + Day-assoc = to-natural-iso mk where + mk : make-natural-iso (Day (Day X Y) Z) (Day X (Day Y Z)) + mk .eta x = Day-rec (assoc-to-cowedge x) + mk .inv x = Day-rec (assoc-from-cowedge x) + mk .eta∘inv x = ext λ h x h' y z → + day (α→ _ _ _ ∘ (id ⊗₁ id) ∘ α← _ _ _ ∘ (id ⊗₁ h') ∘ h) x (day id y z) ≡⟨ day-apₘ (pulll (elimr ⊗.F-id) ∙ cancell (associator .Isoⁿ.invl ηₚ _)) ⟩ + day ((id ⊗₁ h') ∘ h) x (day id y z) ≡⟨ day-glue refl ⟩ + day h (X .F₁ id x) (day (id ∘ h') y z) ≡⟨ day-ap refl (X .F-id #ₚ x) (day-apₘ (idl h')) ⟩ + day h x (day h' y z) ∎ + mk .inv∘eta x = ext λ h h' x y z → + day (α← _ _ _ ∘ (id ⊗₁ id) ∘ α→ _ _ _ ∘ (h' ⊗₁ id) ∘ h) (day id x y) z ≡⟨ day-apₘ (pulll (elimr ⊗.F-id) ∙ cancell (associator .Isoⁿ.invr ηₚ _)) ⟩ + day ((h' ⊗₁ id) ∘ h) (day id x y) z ≡⟨ day-glue refl ⟩ + day h (day (id ∘ h') x y) (Z .F₁ id z) ≡⟨ day-ap refl (day-apₘ (idl h')) (Z .F-id #ₚ z) ⟩ + day h (day h' x y) z ∎ + mk .natural x y f = ext λ h h' x y z → + day ((α→ _ _ _ ∘ (h' ⊗₁ id) ∘ h) ∘ f) x (day id y z) ≡⟨ day-ap (pullr (pullr refl)) refl refl ⟩ + day (α→ _ _ _ ∘ (h' ⊗₁ id) ∘ h ∘ f) x (day id y z) ∎ + +private module M = Monoidal-category + +abstract + day-triangle : ∀ {A B : ⌞ PSh ℓ C ⌟} → Day-map (Day-idr A .Isoⁿ.to) idnt ∘nt Day-assoc A (よ₀ C Unit) B .Isoⁿ.from ≡ Day-map idnt (Day-idl B .Isoⁿ.to) + day-triangle {A} {B} = ext λ i h x h' y z → + day (α← _ _ _ ∘ (id ⊗₁ h') ∘ h) (A .F₁ (ρ← ∘ (id ⊗₁ y) ∘ id) x) z ≡⟨ day-ap refl (ap₂ (A .F₁) (ap (ρ← ∘_) (idr _)) refl) (sym (B .F-id #ₚ z)) ⟩ + day (α← _ _ _ ∘ (id ⊗₁ h') ∘ h) (A .F₁ (ρ← ∘ (id ⊗₁ y)) x) (B .F₁ id z) ≡⟨ sym (day-glue refl) ⟩ + day ((ρ← ∘ (id ⊗₁ y) ⊗₁ id) ∘ α← _ _ _ ∘ (id ⊗₁ h') ∘ h) x z ≡⟨ day-apₘ (⊗.pushl (ap₂ _,_ refl (introl refl))) ⟩ + day ((ρ← ⊗₁ id) ∘ ((id ⊗₁ y) ⊗₁ id) ∘ α← _ _ _ ∘ (id ⊗₁ h') ∘ h) x z ≡⟨ day-apₘ (ap₂ _∘_ refl (extendl (sym (associator .Isoⁿ.from .is-natural _ _ _)))) ⟩ + day ((ρ← ⊗₁ id) ∘ α← _ _ _ ∘ (id ⊗₁ (y ⊗₁ id)) ∘ (id ⊗₁ h') ∘ h) x z ≡⟨ day-apₘ (pulll triangle) ⟩ + day ((id ⊗₁ λ←) ∘ (id ⊗₁ (y ⊗₁ id)) ∘ (id ⊗₁ h') ∘ h) x z ≡⟨ day-apₘ (pulll (sym (⊗.F-∘ _ _)) ∙ pulll (sym (⊗.F-∘ _ _)) ∙ ap (_∘ h) (ap₂ _⊗₁_ (eliml (eliml refl)) (pullr refl))) ⟩ + day ((id ⊗₁ (λ← ∘ (y ⊗₁ id) ∘ h')) ∘ h) x z ≡⟨ day-glue refl ⟩ + day h (A .F₁ id x) (B .F₁ (λ← ∘ (y ⊗₁ id) ∘ h') z) ≡⟨ day-ap refl (A .F-id #ₚ x) refl ⟩ + day h x (B .F₁ (λ← ∘ (y ⊗₁ id) ∘ h') z) ∎ + + day-pentagon + : ∀ {A B C D : ⌞ PSh ℓ C ⌟} + → Day-map (Day-assoc A B C .Isoⁿ.from) idnt + ∘nt Day-assoc A (Day B C) D .Isoⁿ.from + ∘nt Day-map idnt (Day-assoc B C D .Isoⁿ.from) + ≡ Day-assoc (Day A B) C D .Isoⁿ.from + ∘nt Day-assoc A B (Day C D) .Isoⁿ.from + day-pentagon {D = D} = ext λ i h a h' b h'' c d → + let + it = + (α← _ _ _ ⊗₁ id) ∘ α← _ _ _ ∘ (id ⊗₁ α← _ _ _ ∘ (id ⊗₁ h'') ∘ h') ∘ h ≡⟨ ap₂ _∘_ refl (ap₂ _∘_ refl (⊗.pushl (ap₂ _,_ (intror refl) refl))) ⟩ + (α← _ _ _ ⊗₁ id) ∘ α← _ _ _ ∘ (id ⊗₁ α← _ _ _) ∘ (id ⊗₁ (id ⊗₁ h'') ∘ h') ∘ h ≡⟨ pulll refl ∙ extendl (pullr refl ∙ pentagon) ⟩ + α← _ _ _ ∘ α← _ _ _ ∘ (id ⊗₁ (id ⊗₁ h'') ∘ h') ∘ h ≡⟨ ap₂ _∘_ refl (ap₂ _∘_ refl (⊗.pushl (ap₂ _,_ (intror refl) refl))) ⟩ + α← _ _ _ ∘ α← _ _ _ ∘ (id ⊗₁ (id ⊗₁ h'')) ∘ (id ⊗₁ h') ∘ h ≡⟨ ap₂ _∘_ refl (extendl (associator .Isoⁿ.from .is-natural _ _ _)) ⟩ + α← _ _ _ ∘ ((id ⊗₁ id) ⊗₁ h'') ∘ α← _ _ _ ∘ (id ⊗₁ h') ∘ h ≡⟨ ap₂ _∘_ refl (ap₂ _∘_ (ap (_⊗₁ h'') ⊗.F-id) refl) ⟩ + (α← _ _ _ ∘ (id ⊗₁ h'') ∘ α← _ _ _ ∘ (id ⊗₁ h') ∘ h) ∎ + in + day (α← _ _ _ ∘ (id ⊗₁ (α← _ _ _) ∘ (id ⊗₁ h'') ∘ h') ∘ h) (day (α← _ _ _ ∘ (id ⊗₁ id) ∘ id) (day id a b) c) d ≡⟨ day-ap refl (day-ap (elimr (eliml ⊗.F-id) ∙ introl refl) refl refl) (sym (D .F-id #ₚ d)) ⟩ + day (α← _ _ _ ∘ (id ⊗₁ (α← _ _ _) ∘ (id ⊗₁ h'') ∘ h') ∘ h) (day (id ∘ α← _ _ _) (day id a b) c) (D .F₁ id d) ≡⟨ sym (day-glue refl) ⟩ + day ((α← _ _ _ ⊗₁ id) ∘ α← _ _ _ ∘ (id ⊗₁ (α← _ _ _) ∘ (id ⊗₁ h'') ∘ h') ∘ h) (day id (day id a b) c) d ≡⟨ day-apₘ it ⟩ + day (α← _ _ _ ∘ (id ⊗₁ h'') ∘ α← _ _ _ ∘ (id ⊗₁ h') ∘ h) (day id (day id a b) c) d ∎ + +Day-monoidal : Monoidal-category (PSh ℓ C) +Day-monoidal .M.-⊗- = Day-bifunctor +Day-monoidal .M.Unit = よ₀ C Unit +Day-monoidal .M.unitor-l = to-natural-iso mk-λ where + mk-λ : make-natural-iso _ _ + mk-λ .eta x = Day-idl x .Isoⁿ.from + mk-λ .inv x = Day-idl x .Isoⁿ.to + mk-λ .eta∘inv x = Day-idl x .Isoⁿ.invr + mk-λ .inv∘eta x = Day-idl x .Isoⁿ.invl + mk-λ .natural x y f = trivial! +Day-monoidal .M.unitor-r = to-natural-iso mk-ρ where + mk-ρ : make-natural-iso _ _ + mk-ρ .eta x = Day-idr x .Isoⁿ.from + mk-ρ .inv x = Day-idr x .Isoⁿ.to + mk-ρ .eta∘inv x = Day-idr x .Isoⁿ.invr + mk-ρ .inv∘eta x = Day-idr x .Isoⁿ.invl + mk-ρ .natural x y f = trivial! +Day-monoidal .M.associator = to-natural-iso mk-α where + mk-α : make-natural-iso _ _ + mk-α .eta (x , y , z) = Day-assoc x y z .Isoⁿ.to + mk-α .inv (x , y , z) = Day-assoc x y z .Isoⁿ.from + mk-α .eta∘inv (x , y , z) = Day-assoc x y z .Isoⁿ.invl + mk-α .inv∘eta (x , y , z) = Day-assoc x y z .Isoⁿ.invr + mk-α .natural x y f = trivial! +Day-monoidal .M.triangle {A} {B} = day-triangle +Day-monoidal .M.pentagon {A} {B} {C} {D} = day-pentagon +``` diff --git a/src/Data/Set/Coequaliser.lagda.md b/src/Data/Set/Coequaliser.lagda.md index 99d5d5651..728d89e67 100644 --- a/src/Data/Set/Coequaliser.lagda.md +++ b/src/Data/Set/Coequaliser.lagda.md @@ -533,3 +533,24 @@ is a set, that means it's an equivalence. (y , p) ← inc-is-surjective x pure (f y , ap g₁ (squash (surj (f y)) (inc (y , refl))) ∙ p) ``` + + diff --git a/src/Order/Instances/Disjoint.lagda.md b/src/Order/Instances/Disjoint.lagda.md index ad84ab15d..43ec06b9e 100644 --- a/src/Order/Instances/Disjoint.lagda.md +++ b/src/Order/Instances/Disjoint.lagda.md @@ -157,7 +157,7 @@ Posets-has-set-indexed-coproducts I F = mk where mk .ι = injᵖ mk .has-is-ic .match = matchᵖ mk .has-is-ic .commute = trivial! - mk .has-is-ic .unique f p = ext λ (i , x) → p i #ₚ x + mk .has-is-ic .unique f p = ext λ i x → p i #ₚ x ``` ## Binary coproducts are a special case of indexed coproducts @@ -168,8 +168,8 @@ Posets-has-set-indexed-coproducts I F = mk where .to → match⊎ᵖ (injᵖ true) (injᵖ false) .from → matchᵖ (Bool-elim _ inlᵖ inrᵖ) .inverses .invl → ext λ where - (true , x) → refl - (false , x) → refl + true x → refl + false x → refl .inverses .invr → ext λ where (inl x) → refl (inr x) → refl diff --git a/src/Order/Instances/Pointwise.lagda.md b/src/Order/Instances/Pointwise.lagda.md index 3ba29759b..5fa7ffe55 100644 --- a/src/Order/Instances/Pointwise.lagda.md +++ b/src/Order/Instances/Pointwise.lagda.md @@ -126,5 +126,5 @@ Posets-has-indexed-products F = mk where .inverses .invl → ext λ where x true → refl x false → refl - .inverses .invr → ext λ _ → refl , refl + .inverses .invr → ext λ x y → refl , refl ``` diff --git a/src/Order/Semilattice/Free.lagda.md b/src/Order/Semilattice/Free.lagda.md index 57a9b65c4..f96259b68 100644 --- a/src/Order/Semilattice/Free.lagda.md +++ b/src/Order/Semilattice/Free.lagda.md @@ -231,9 +231,9 @@ elements of $P$, which is the same join used to compute the extension of $f$. ```agda -make-free-join-slat .unique {A} {B} {f} {g} p = ext λ P → lub-unique - (fold-K.ε'.has-lub A B f (P .fst) (P .snd)) +make-free-join-slat .unique {A} {B} {f} {g} p = ext λ P pfin → lub-unique + (fold-K.ε'.has-lub A B f P pfin) (cast-is-lubᶠ (λ Q → sym (p #ₚ Q .fst)) $ - pres-finitely-indexed-lub (g .witness) (P .snd) _ _ $ + pres-finitely-indexed-lub (g .witness) pfin _ _ $ K-singleton-lub A _) ```