From 65edb884c9d27805b0b4488506a9416e0a387137 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 3 May 2023 13:39:46 -0700 Subject: [PATCH 01/10] def: avoid transports in diagram fibration --- src/Cat/Displayed/Instances/Diagrams.lagda.md | 100 +++++++++++++++--- 1 file changed, 88 insertions(+), 12 deletions(-) diff --git a/src/Cat/Displayed/Instances/Diagrams.lagda.md b/src/Cat/Displayed/Instances/Diagrams.lagda.md index d9bbebbfb..825e05d92 100644 --- a/src/Cat/Displayed/Instances/Diagrams.lagda.md +++ b/src/Cat/Displayed/Instances/Diagrams.lagda.md @@ -53,21 +53,39 @@ liftings along a constant functor $\Delta_{x} : \cJ \to \cB$, we get a diagram in $\cE$ that lies entirely in the fibre $\cE_{x}$: a fibrewise diagram! -This allows us to concisely define the fibration of fibrewise diagrams +we could concisely define the fibration of fibrewise diagrams as the base change of $\cE \to \cB$ along the functor $\cB \to [\cJ, -\cB]$ that takes an object to the constant diagram on that object. +\cB]$ that takes an object to the constant diagram on that object, but +this runs into some annoying issues with transports. Therefore, we +unfold the definition instead. [fibration of liftings]: Cat.Displayed.Instances.Lifting.html + + ```agda Diagrams : ∀ {oj ℓj} (J : Precategory oj ℓj) → Displayed B _ _ -Diagrams J = Change-of-base ConstD (Liftings E J) +Diagrams J .Ob[_] b = Lifting {J = J} E (Const b) +Diagrams J .Hom[_] u F G = F =[ const-nt u ]=>l G +Diagrams J .Hom[_]-set _ _ _ = Nat-lift-is-set +Diagrams J .id′ .η′ _ = id′ +Diagrams J .id′ .is-natural′ _ _ _ = + cast[] $ idl′ _ ∙[] symP (idr′ _) +Diagrams J ._∘′_ α β .η′ j = α .η′ j ∘′ β .η′ j +Diagrams J ._∘′_ α β .is-natural′ x y f = + cast[] $ pullr[] _ (β .is-natural′ x y f) ∙[] extendl[] _ (α .is-natural′ x y f) +Diagrams J .idr′ α = Nat-lift-pathp λ _ → idr′ _ +Diagrams J .idl′ α = Nat-lift-pathp λ _ → idl′ _ +Diagrams J .assoc′ α β γ = Nat-lift-pathp λ _ → assoc′ _ _ _ ``` -When $\cE$ is a fibration, then so is the fibration of diagrams. - +## As a fibration + +We begin by characterizing the cartesian maps in the diagram fibration. +Like the fibration of liftings, these are the pointwise cartesian maps. +This proof is identical to `pointwise-cartesian→Liftings-cartesian`{.Agda}, +but we are off by some definitional equalities, so we have to unfold +some things. + +```agda + pointwise-cartesian→Diagram-cartesian + : ∀ {x y : Ob} {F : Lifting E (Const x)} {G : Lifting E (Const y)} + → {u : Hom x y} {α : F =[ const-nt u ]=>l G} + → (∀ j → is-cartesian E u (α .η′ j)) + → is-cartesian (Diagrams J) u α + pointwise-cartesian→Diagram-cartesian {u = u} {α = α} pointwise = cart where + module pointwise x = is-cartesian (pointwise x) + + cart : is-cartesian (Diagrams J) u α + cart .is-cartesian.universal m β .η′ x = + pointwise.universal x m (β .η′ x) + cart .is-cartesian.universal m β .is-natural′ x y f = + pointwise.uniquep₂ _ _ _ _ _ _ + (pulll[] _ (pointwise.commutes _ _ _) ∙[] β .is-natural′ _ _ _) + (pulll[] _ (α .is-natural′ x y f) + ∙[] pullr[] _ (pointwise.commutes _ _ _)) + cart .is-cartesian.commutes m β = + Nat-lift-pathp (λ _ → pointwise.commutes _ _ _) + cart .is-cartesian.unique β' p = + Nat-lift-pathp (λ x → pointwise.unique _ _ λ i → p i .η′ x) +``` + +We can use the previous fact to show that the fibration of diagrams is +actually a fibration. Luckily, we get to re-use a lot of the proof +that the fibration of liftings is a fibration. + ```agda Diagram-fibration : Cartesian-fibration E → Cartesian-fibration (Diagrams J) - Diagram-fibration fib = - Change-of-base-fibration ConstD (Liftings E _) - (Liftings-fibration E _ fib) + Diagram-fibration fib .Cartesian-fibration.has-lift f F = cart-lift where + module fib = Cartesian-fibration.has-lift fib + open Cartesian-fibration (Liftings-fibration E J fib) + + cart-lift : Cartesian-lift _ f F + cart-lift .Cartesian-lift.x′ = has-lift.x′ (const-nt f) F + cart-lift .Cartesian-lift.lifting = has-lift.lifting (const-nt f) F + cart-lift .Cartesian-lift.cartesian = + pointwise-cartesian→Diagram-cartesian (λ _ → fib.cartesian _ _) ``` ## The constant fibrewise diagram functor @@ -116,9 +175,26 @@ of shape $\cJ$, which takes an $x'$ to the constant diagram. ConstFibD .Vertical-functor.F₀′ = ConstL ConstFibD .Vertical-functor.F₁′ = const-ntl ConstFibD .Vertical-functor.F-id′ = - Nat-lift-pathp (λ x → sym (transport-refl _)) + Nat-lift-pathp (λ x → refl) ConstFibD .Vertical-functor.F-∘′ = - Nat-lift-pathp (λ x → sym (transport-refl _)) + Nat-lift-pathp (λ x → refl) +``` + +Furthermore, this functor is fibred. + +```agda + ConstFibD-fibred : is-vertical-fibred ConstFibD + ConstFibD-fibred f′ cart = + pointwise-cartesian→Diagram-cartesian (λ _ → cart) +``` + +We will use the fibred version of this functor quite a bit, so we give +it a nice short name. + +```agda + Δd : Vertical-fibred-functor E (Diagrams J) + Δd .Vertical-fibred-functor.vert = ConstFibD + Δd .Vertical-fibred-functor.F-cartesian = ConstFibD-fibred ``` Next, we note that liftings of the constant functor correspond with @@ -186,8 +262,8 @@ functor categories $[\cJ, \cE_x]$. Fibrewise-diagram : ∀ {x} → Functor Cat[ J , Fibre E x ] (Fibre (Diagrams J) x) Fibrewise-diagram .F₀ = Diagram→ConstL Fibrewise-diagram .F₁ = Diagram-nat→ConstL-natl - Fibrewise-diagram .F-id = Nat-lift-pathp λ _ → sym Regularity.reduce! - Fibrewise-diagram .F-∘ _ _ = Nat-lift-pathp λ _ → sym Regularity.reduce! + Fibrewise-diagram .F-id = Nat-lift-pathp λ _ → refl + Fibrewise-diagram .F-∘ _ _ = Nat-lift-pathp λ _ → sym (Regularity.reduce!) ``` Again, this isomorphism is *almost* definitional. From 7f765421b88a8f357c125cccbe9cf9378d95bc54 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 3 May 2023 15:17:36 -0700 Subject: [PATCH 02/10] def: restriction of vertical functors/natural transformations --- src/Cat/Displayed/Functor.lagda.md | 80 ++++++++++++++++++++++++++++++ 1 file changed, 80 insertions(+) diff --git a/src/Cat/Displayed/Functor.lagda.md b/src/Cat/Displayed/Functor.lagda.md index 5617f5ca5..d39c3e164 100644 --- a/src/Cat/Displayed/Functor.lagda.md +++ b/src/Cat/Displayed/Functor.lagda.md @@ -2,6 +2,7 @@ ```agda open import Cat.Displayed.Cartesian open import Cat.Displayed.Base +open import Cat.Displayed.Fibre open import Cat.Prelude import Cat.Displayed.Reasoning as DR @@ -528,6 +529,50 @@ module _ IdVf = Fibred→Vertical-fibred Idf′ ``` +### Restriction of vertical functors + +Vertical functors restrict to functors between fibre categories. + + + +```agda + Restrict↓ : Vertical-functor ℰ ℱ → ∀ x → Functor (Fibre ℰ x) (Fibre ℱ x) + Restrict↓ F' _ .Functor.F₀ = F' .F₀′ + Restrict↓ F' _ .Functor.F₁ = F' .F₁′ + Restrict↓ F' _ .Functor.F-id = F' .F-id′ +``` + +As per usual, transports get in our way. This `comp`{.Agda} really is +the best way to handle this. + +```agda + Restrict↓ F' _ .Functor.F-∘ {x} {y} {z} f g i = + comp (λ j → ℱ.Hom[ idl id j ] (F' .F₀′ x) (F' .F₀′ z)) (∂ i) λ where + j (i = i0) → + F' .F₁′ (transp (λ i → ℰ.Hom[ idl id (i ∧ j) ] x z) (~ j) (f ℰ.∘′ g)) + j (i = i1) → + transp (λ i → ℱ.Hom[ idl id (i ∧ j) ] (F' .F₀′ x) (F' .F₀′ z)) (~ j) + (F' .F₁′ f ℱ.∘′ F' .F₁′ g) + j (j = i0) → F' .F-∘′ {f′ = f} {g′ = g} i + + Restrict↓f : Vertical-fibred-functor ℰ ℱ → ∀ x → Functor (Fibre ℰ x) (Fibre ℱ x) + Restrict↓f F' = Restrict↓ (Vertical-fibred-functor.vert F') +``` + + ## Displayed Natural Transformations Just like we have defined a [displayed functor][disfct] @@ -632,3 +677,38 @@ to be preserved. F′ =>f↓ G′ = F′ .vert =>↓ G′ .vert where open Vertical-fibred-functor ``` + +Vertical natural transformations restrict to natural transformations +between restrictions of vertical functors (what a mouthful!). + + + +```agda + Vert-nat-restrict + : ∀ {F′ G′ : Vertical-functor ℰ ℱ} + → F′ =>↓ G′ → ∀ x → Restrict↓ F′ x => Restrict↓ G′ x + Vert-nat-restrict α′ x .η x′ = α′ .η′ x′ + Vert-nat-restrict {F′ = F′} {G′ = G′} α′ x .is-natural x′ y′ f′ i = + comp (λ j → ℱ.Hom[ hom-filler i j ] (F′ .F₀′ x′) (G′ .F₀′ y′)) (∂ i) λ where + j (i = i0) → + transp (λ i → ℱ.Hom[ idl id (i ∧ j) ] (F′ .F₀′ x′) (G′ .F₀′ y′)) (~ j) + (α′ .η′ y′ ℱ.∘′ F′ .F₁′ f′) + j (i = i1) → + transp (λ i → ℱ.Hom[ idl id (i ∧ j) ] (F′ .F₀′ x′) (G′ .F₀′ y′)) (~ j) + (G′ .F₁′ f′ ℱ.∘′ α′ .η′ x′) + j (j = i0) → α′ .is-natural′ x′ y′ f′ i + where + hom-filler : I → I → Hom x x + hom-filler i j = + is-set→squarep (λ i j → Hom-set x x) (idl id) id-comm-sym refl (idl id) j i + + Vert-fib-nat-restrict + : ∀ {F′ G′ : Vertical-fibred-functor ℰ ℱ} + → F′ =>f↓ G′ → ∀ x → Restrict↓f F′ x => Restrict↓f G′ x + Vert-fib-nat-restrict α′ x = Vert-nat-restrict α′ x +``` From 10f5dde59aa2c6cbe01c644586dedf87ec7a385d Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 4 May 2023 16:32:07 -0700 Subject: [PATCH 03/10] chore: rexport Displayed from Displayed.Reasoning --- src/Cat/Displayed/Cartesian.lagda.md | 10 +- src/Cat/Displayed/Cartesian/Identity.lagda.md | 1 - src/Cat/Displayed/Cartesian/Indexing.lagda.md | 1 - src/Cat/Displayed/Cartesian/Right.lagda.md | 1 - src/Cat/Displayed/Cartesian/Weak.lagda.md | 1 - src/Cat/Displayed/Cocartesian.lagda.md | 1 - .../Displayed/Cocartesian/Indexing.lagda.md | 1 - src/Cat/Displayed/Cocartesian/Weak.lagda.md | 1 - src/Cat/Displayed/Fibre.lagda.md | 1 - src/Cat/Displayed/Instances/Diagrams.lagda.md | 1 - .../Instances/DisplayedFamilies.lagda.md | 1 - src/Cat/Displayed/Instances/Lifting.lagda.md | 3 - src/Cat/Displayed/InternalSum.lagda.md | 2 +- src/Cat/Displayed/Morphism.lagda.md | 1 - src/Cat/Displayed/Morphism/Duality.lagda.md | 1 - src/Cat/Displayed/Reasoning.lagda.md | 251 +++++++++--------- src/Cat/Displayed/Solver.agda | 2 - .../Displayed/Univalence/Reasoning.lagda.md | 1 - src/Cat/Functor/Hom/Displayed.lagda.md | 1 - 19 files changed, 137 insertions(+), 145 deletions(-) diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md index 870ea8050..65d764694 100644 --- a/src/Cat/Displayed/Cartesian.lagda.md +++ b/src/Cat/Displayed/Cartesian.lagda.md @@ -3,7 +3,7 @@ open import Cat.Displayed.Base open import Cat.Prelude -import Cat.Displayed.Reasoning as DR +import Cat.Displayed.Reasoning import Cat.Displayed.Morphism import Cat.Reasoning ``` @@ -13,11 +13,15 @@ import Cat.Reasoning module Cat.Displayed.Cartesian {o ℓ o′ ℓ′} {B : Precategory o ℓ} (E : Displayed B o′ ℓ′) where +``` + + # Cartesian morphisms and Fibrations diff --git a/src/Cat/Displayed/Cartesian/Identity.lagda.md b/src/Cat/Displayed/Cartesian/Identity.lagda.md index 985ede495..03bdc12b0 100644 --- a/src/Cat/Displayed/Cartesian/Identity.lagda.md +++ b/src/Cat/Displayed/Cartesian/Identity.lagda.md @@ -33,7 +33,6 @@ private open Cat.Displayed.Univalence.Reasoning E open Cat.Displayed.Univalence E open Cat.Displayed.Morphism E -open Displayed E open Dr E open _≅[_]_ ``` diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md index 999b645ba..e4d4a989f 100644 --- a/src/Cat/Displayed/Cartesian/Indexing.lagda.md +++ b/src/Cat/Displayed/Cartesian/Indexing.lagda.md @@ -30,7 +30,6 @@ open Cartesian-fibration cartesian open Cat.Displayed.Reasoning E open Cat.Reasoning B open Cartesian-lift -open Displayed E open is-cartesian open Functor ``` diff --git a/src/Cat/Displayed/Cartesian/Right.lagda.md b/src/Cat/Displayed/Cartesian/Right.lagda.md index 2a7fee03f..2ed392ccd 100644 --- a/src/Cat/Displayed/Cartesian/Right.lagda.md +++ b/src/Cat/Displayed/Cartesian/Right.lagda.md @@ -24,7 +24,6 @@ module Cat.Displayed.Cartesian.Right where open Cat.Reasoning ℬ -open Displayed ℰ open Cat.Displayed.Cartesian ℰ open Cat.Displayed.Morphism ℰ open Cat.Displayed.Reasoning ℰ diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md index 22c413897..40dfd649a 100644 --- a/src/Cat/Displayed/Cartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cartesian/Weak.lagda.md @@ -31,7 +31,6 @@ module Cat.Displayed.Cartesian.Weak @@ -164,7 +163,6 @@ module _ private module J = Precategory J open Cat.Reasoning B - open Displayed E open Cat.Displayed.Reasoning E open Lifting ``` @@ -308,7 +306,6 @@ module _ private module J = Precategory J open Cat.Reasoning B - open Displayed E open Cat.Displayed.Reasoning E open Lifting open _=[_]=>l_ diff --git a/src/Cat/Displayed/InternalSum.lagda.md b/src/Cat/Displayed/InternalSum.lagda.md index 10d937baa..4d75ea691 100644 --- a/src/Cat/Displayed/InternalSum.lagda.md +++ b/src/Cat/Displayed/InternalSum.lagda.md @@ -43,5 +43,5 @@ record Internal-sum : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) no-eta-equality field ∐ : Vertical-fibred-functor (Disp-family E) E - adjunction : ∐ ⊣↓ ConstDispFamVf E + adjunction : ∐ ⊣f↓ ConstDispFamVf E ``` diff --git a/src/Cat/Displayed/Morphism.lagda.md b/src/Cat/Displayed/Morphism.lagda.md index 97cc15086..2b5273052 100644 --- a/src/Cat/Displayed/Morphism.lagda.md +++ b/src/Cat/Displayed/Morphism.lagda.md @@ -18,7 +18,6 @@ module Cat.Displayed.Morphism @@ -45,10 +43,10 @@ shorthand syntax for that here. You can think of this as being an abbreviation for `subst`{.Agda} because... that's what it is. ```agda -hom[_] : ∀ {a b x y} {f g : B.Hom a b} → f ≡ g → E.Hom[ f ] x y → E.Hom[ g ] x y -hom[ p ] f′ = subst (λ h → E.Hom[ h ] _ _) p f′ +hom[_] : ∀ {a b x y} {f g : Hom a b} → f ≡ g → Hom[ f ] x y → Hom[ g ] x y +hom[ p ] f′ = subst (λ h → Hom[ h ] _ _) p f′ -hom[_]⁻ : ∀ {a b x y} {f g : B.Hom a b} → g ≡ f → E.Hom[ f ] x y → E.Hom[ g ] x y +hom[_]⁻ : ∀ {a b x y} {f g : Hom a b} → g ≡ f → Hom[ f ] x y → Hom[ g ] x y hom[ p ]⁻ f′ = hom[ sym p ] f′ ``` @@ -57,17 +55,17 @@ adjust the path we're transporting over to get something more convenient. ```agda reindex - : ∀ {a b x y} {f g : B.Hom a b} (p q : f ≡ g) {f′ : E.Hom[ f ] x y} + : ∀ {a b x y} {f g : Hom a b} (p q : f ≡ g) {f′ : Hom[ f ] x y} → hom[ p ] f′ ≡ hom[ q ] f′ -reindex p q {f′} = ap (λ e → hom[ e ] f′) (B.Hom-set _ _ _ _ p q) +reindex p q {f′} = ap (λ e → hom[ e ] f′) (Hom-set _ _ _ _ p q) cast[] - : ∀ {a b x y} {f g : B.Hom a b} {f′ : E.Hom[ f ] x y} {g′ : E.Hom[ g ] x y} + : ∀ {a b x y} {f g : Hom a b} {f′ : Hom[ f ] x y} {g′ : Hom[ g ] x y} → {p q : f ≡ g} - → f′ E.≡[ p ] g′ - → f′ E.≡[ q ] g′ + → f′ ≡[ p ] g′ + → f′ ≡[ q ] g′ cast[] {f = f} {g = g} {f′ = f′} {g′ = g′} {p = p} {q = q} r = - coe0→1 (λ i → f′ E.≡[ B.Hom-set _ _ f g p q i ] g′) r + coe0→1 (λ i → f′ ≡[ Hom-set _ _ f g p q i ] g′) r ``` @@ -79,14 +77,14 @@ composite unchanged. ```agda hom[]-∙ - : ∀ {a b x y} {f g h : B.Hom a b} (p : f ≡ g) (q : g ≡ h) - {f′ : E.Hom[ f ] x y} + : ∀ {a b x y} {f g h : Hom a b} (p : f ≡ g) (q : g ≡ h) + {f′ : Hom[ f ] x y} → hom[ q ] (hom[ p ] f′) ≡ hom[ p ∙ q ] f′ -hom[]-∙ p q = sym (subst-∙ (λ h → E.Hom[ h ] _ _) _ _ _) +hom[]-∙ p q = sym (subst-∙ (λ h → Hom[ h ] _ _) _ _ _) duplicate - : ∀ {a b x y} {f f' g : B.Hom a b} (p : f ≡ g) (q : f' ≡ g) (r : f ≡ f') - {f′ : E.Hom[ f ] x y} + : ∀ {a b x y} {f f' g : Hom a b} (p : f ≡ g) (q : f' ≡ g) (r : f ≡ f') + {f′ : Hom[ f ] x y} → hom[ p ] f′ ≡ hom[ q ] (hom[ r ] f′) duplicate p q r = reindex _ _ ∙ sym (hom[]-∙ r q) ``` @@ -105,42 +103,42 @@ we can't just get rid of the transport $p^*(-)$. ```agda whisker-r - : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′} - {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′} + : ∀ {a b c} {f : Hom b c} {g g' : Hom a b} {a′ b′ c′} + {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′} → (p : g ≡ g') - → f′ E.∘′ hom[ p ] g′ ≡ hom[ ap (f B.∘_) p ] (f′ E.∘′ g′) + → f′ ∘′ hom[ p ] g′ ≡ hom[ ap (f ∘_) p ] (f′ ∘′ g′) whisker-r {f = f} {a′ = a′} {_} {c′} {f′} {g′} p i = - comp (λ j → E.Hom[ f B.∘ p (i ∨ j) ] a′ c′) (∂ i) λ where - j (i = i0) → f′ E.∘′ transport-filler (λ i → E.Hom[ p i ] _ _) g′ j - j (i = i1) → hom[ ap (f B.∘_) p ] (f′ E.∘′ g′) - j (j = i0) → transport-filler (λ i → E.Hom[ f B.∘ p i ] _ _) (f′ E.∘′ g′) i + comp (λ j → Hom[ f ∘ p (i ∨ j) ] a′ c′) (∂ i) λ where + j (i = i0) → f′ ∘′ transport-filler (λ i → Hom[ p i ] _ _) g′ j + j (i = i1) → hom[ ap (f ∘_) p ] (f′ ∘′ g′) + j (j = i0) → transport-filler (λ i → Hom[ f ∘ p i ] _ _) (f′ ∘′ g′) i whisker-l - : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {a′ b′ c′} - {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′} + : ∀ {a b c} {f f' : Hom b c} {g : Hom a b} {a′ b′ c′} + {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′} → (p : f ≡ f') - → hom[ p ] f′ E.∘′ g′ ≡ hom[ ap (B._∘ g) p ] (f′ E.∘′ g′) + → hom[ p ] f′ ∘′ g′ ≡ hom[ ap (_∘ g) p ] (f′ ∘′ g′) whisker-l {g = g} {a′} {_} {c′} {f′ = f′} {g′ = g′} p i = - comp (λ j → E.Hom[ p (i ∨ j) B.∘ g ] a′ c′) (∂ i) λ where - j (i = i0) → transport-filler (λ i → E.Hom[ p i ] _ _) f′ j E.∘′ g′ - j (i = i1) → hom[ ap (B._∘ g) p ] (f′ E.∘′ g′) - j (j = i0) → transport-filler (λ i → E.Hom[ p i B.∘ g ] _ _) (f′ E.∘′ g′) i + comp (λ j → Hom[ p (i ∨ j) ∘ g ] a′ c′) (∂ i) λ where + j (i = i0) → transport-filler (λ i → Hom[ p i ] _ _) f′ j ∘′ g′ + j (i = i1) → hom[ ap (_∘ g) p ] (f′ ∘′ g′) + j (j = i0) → transport-filler (λ i → Hom[ p i ∘ g ] _ _) (f′ ∘′ g′) i ``` @@ -150,67 +148,67 @@ lemmas above: ```agda smashr - : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {h : B.Hom a c} {a′ b′ c′} - {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′} - → (p : g ≡ g') (q : f B.∘ g' ≡ h) - → hom[ q ] (f′ E.∘′ hom[ p ] g′) ≡ hom[ ap (f B.∘_) p ∙ q ] (f′ E.∘′ g′) + : ∀ {a b c} {f : Hom b c} {g g' : Hom a b} {h : Hom a c} {a′ b′ c′} + {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′} + → (p : g ≡ g') (q : f ∘ g' ≡ h) + → hom[ q ] (f′ ∘′ hom[ p ] g′) ≡ hom[ ap (f ∘_) p ∙ q ] (f′ ∘′ g′) smashr p q = ap hom[ q ] (whisker-r p) ∙ hom[]-∙ _ _ smashl - : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {h : B.Hom a c} {a′ b′ c′} - {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′} - → (p : f ≡ f') (q : f' B.∘ g ≡ h) - → hom[ q ] (hom[ p ] f′ E.∘′ g′) ≡ hom[ ap (B._∘ g) p ∙ q ] (f′ E.∘′ g′) + : ∀ {a b c} {f f' : Hom b c} {g : Hom a b} {h : Hom a c} {a′ b′ c′} + {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′} + → (p : f ≡ f') (q : f' ∘ g ≡ h) + → hom[ q ] (hom[ p ] f′ ∘′ g′) ≡ hom[ ap (_∘ g) p ∙ q ] (f′ ∘′ g′) smashl p q = ap hom[ q ] (whisker-l p) ∙ hom[]-∙ _ _ expandl - : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {h : B.Hom a c} {a′ b′ c′} - {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′} - → (p : f ≡ f') (q : f B.∘ g ≡ h) - → hom[ q ] (f′ E.∘′ g′) ≡ hom[ ap (B._∘ g) (sym p) ∙ q ] (hom[ p ] f′ E.∘′ g′) + : ∀ {a b c} {f f' : Hom b c} {g : Hom a b} {h : Hom a c} {a′ b′ c′} + {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′} + → (p : f ≡ f') (q : f ∘ g ≡ h) + → hom[ q ] (f′ ∘′ g′) ≡ hom[ ap (_∘ g) (sym p) ∙ q ] (hom[ p ] f′ ∘′ g′) expandl p q = reindex q _ ∙ (sym $ smashl _ _) expandr - : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {h : B.Hom a c} {a′ b′ c′} - {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′} - → (p : g ≡ g') (q : f B.∘ g ≡ h) - → hom[ q ] (f′ E.∘′ g′) ≡ hom[ ap (f B.∘_) (sym p) ∙ q ] (f′ E.∘′ hom[ p ] g′) + : ∀ {a b c} {f : Hom b c} {g g' : Hom a b} {h : Hom a c} {a′ b′ c′} + {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′} + → (p : g ≡ g') (q : f ∘ g ≡ h) + → hom[ q ] (f′ ∘′ g′) ≡ hom[ ap (f ∘_) (sym p) ∙ q ] (f′ ∘′ hom[ p ] g′) expandr p q = reindex q _ ∙ (sym $ smashr _ _) yank : ∀ {a b c d} - {f : B.Hom c d} {g : B.Hom b c} {h : B.Hom a b} {i : B.Hom a c} {j : B.Hom b d} + {f : Hom c d} {g : Hom b c} {h : Hom a b} {i : Hom a c} {j : Hom b d} {a′ b′ c′ d′} - {f′ : E.Hom[ f ] c′ d′} {g′ : E.Hom[ g ] b′ c′} {h′ : E.Hom[ h ] a′ b′} - (p : g B.∘ h ≡ i) (q : f B.∘ g ≡ j) (r : f B.∘ i ≡ j B.∘ h) - → (f′ E.∘′ hom[ p ](g′ E.∘′ h′)) E.≡[ r ] hom[ q ] (f′ E.∘′ g′) E.∘′ h′ + {f′ : Hom[ f ] c′ d′} {g′ : Hom[ g ] b′ c′} {h′ : Hom[ h ] a′ b′} + (p : g ∘ h ≡ i) (q : f ∘ g ≡ j) (r : f ∘ i ≡ j ∘ h) + → (f′ ∘′ hom[ p ](g′ ∘′ h′)) ≡[ r ] hom[ q ] (f′ ∘′ g′) ∘′ h′ yank {f′ = f′} {g′ = g′} {h′ = h′} p q r = to-pathp $ - hom[ r ] (f′ E.∘′ hom[ p ] (g′ E.∘′ h′)) ≡⟨ smashr p r ⟩ - hom[ ap (B._∘_ _) p ∙ r ] (f′ E.∘′ g′ E.∘′ h′) ≡⟨ ap hom[ _ ] (sym (from-pathp λ i → E.assoc′ f′ g′ h′ (~ i))) ⟩ - hom[ ap (B._∘_ _) p ∙ r ] (hom[ sym (B.assoc _ _ _) ] ((f′ E.∘′ g′) E.∘′ h′)) ≡⟨ hom[]-∙ _ _ ⟩ - hom[ sym (B.assoc _ _ _) ∙ (ap (B .Precategory._∘_ _) p ∙ r)] ((f′ E.∘′ g′) E.∘′ h′) ≡⟨ reindex _ _ ⟩ - hom[ (ap (B._∘ _) q) ] ((f′ E.∘′ g′) E.∘′ h′) ≡˘⟨ whisker-l q ⟩ - hom[ q ] (f′ E.∘′ g′) E.∘′ h′ ∎ + hom[ r ] (f′ ∘′ hom[ p ] (g′ ∘′ h′)) ≡⟨ smashr p r ⟩ + hom[ ap (_∘_ _) p ∙ r ] (f′ ∘′ g′ ∘′ h′) ≡⟨ ap hom[ _ ] (sym (from-pathp λ i → assoc′ f′ g′ h′ (~ i))) ⟩ + hom[ ap (_∘_ _) p ∙ r ] (hom[ sym (assoc _ _ _) ] ((f′ ∘′ g′) ∘′ h′)) ≡⟨ hom[]-∙ _ _ ⟩ + hom[ sym (assoc _ _ _) ∙ (ap (B .Precategory._∘_ _) p ∙ r)] ((f′ ∘′ g′) ∘′ h′) ≡⟨ reindex _ _ ⟩ + hom[ (ap (_∘ _) q) ] ((f′ ∘′ g′) ∘′ h′) ≡˘⟨ whisker-l q ⟩ + hom[ q ] (f′ ∘′ g′) ∘′ h′ ∎ cancel - : ∀ {a b} {f g : B.Hom a b} (p q : f ≡ g) {a′ b′} - {f′ : E.Hom[ f ] a′ b′} {g′ : E.Hom[ g ] a′ b′} - → PathP (λ i → E.Hom[ q i ] a′ b′) f′ g′ + : ∀ {a b} {f g : Hom a b} (p q : f ≡ g) {a′ b′} + {f′ : Hom[ f ] a′ b′} {g′ : Hom[ g ] a′ b′} + → PathP (λ i → Hom[ q i ] a′ b′) f′ g′ → hom[ p ] f′ ≡ g′ cancel p q r = reindex p q ∙ from-pathp r kill₁ - : ∀ {a b} {a′ b′} {f g h : B.Hom a b} {h₁′ : E.Hom[ f ] a′ b′} {h₂′ : E.Hom[ g ] a′ b′} + : ∀ {a b} {a′ b′} {f g h : Hom a b} {h₁′ : Hom[ f ] a′ b′} {h₂′ : Hom[ g ] a′ b′} → (p : f ≡ g) (q : g ≡ h) - → PathP (λ i → E.Hom[ p i ] a′ b′) h₁′ h₂′ + → PathP (λ i → Hom[ p i ] a′ b′) h₁′ h₂′ → hom[ p ∙ q ] h₁′ ≡ hom[ q ] h₂′ kill₁ p q r = sym (hom[]-∙ _ _) ∙ ap hom[ q ] (from-pathp r) -revive₁ : ∀ {a b} {f g h : B.Hom a b} - {a′ b′} {f′ : E.Hom[ f ] a′ b′} {g′ : E.Hom[ g ] a′ b′} +revive₁ : ∀ {a b} {f g h : Hom a b} + {a′ b′} {f′ : Hom[ f ] a′ b′} {g′ : Hom[ g ] a′ b′} → {p : f ≡ g} {q : f ≡ h} - → f′ E.≡[ p ] g′ + → f′ ≡[ p ] g′ → hom[ q ] f′ ≡ hom[ sym p ∙ q ] g′ revive₁ {f′ = f′} {g′ = g′} {p = p} {q = q} p′ = hom[ q ] f′ ≡⟨ reindex _ _ ⟩ @@ -221,93 +219,93 @@ revive₁ {f′ = f′} {g′ = g′} {p = p} {q = q} p′ = -- something. We combine the reindexing to fix the association and -- killing the first parameter to "weave" here. weave - : ∀ {a b} {a′ b′} {f g h : B.Hom a b} {h₁′ : E.Hom[ f ] a′ b′} {h₂′ : E.Hom[ g ] a′ b′} + : ∀ {a b} {a′ b′} {f g h : Hom a b} {h₁′ : Hom[ f ] a′ b′} {h₂′ : Hom[ g ] a′ b′} → (p : f ≡ h) (p′ : f ≡ g) (q : g ≡ h) - → PathP (λ i → E.Hom[ p′ i ] a′ b′) h₁′ h₂′ + → PathP (λ i → Hom[ p′ i ] a′ b′) h₁′ h₂′ → hom[ p ] h₁′ ≡ hom[ q ] h₂′ weave p p′ q s = reindex p (p′ ∙ q) ∙ kill₁ p′ q s split - : ∀ {a b c} {f f' : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′} - {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′} + : ∀ {a b c} {f f' : Hom b c} {g g' : Hom a b} {a′ b′ c′} + {f′ : Hom[ f ] b′ c′} {g′ : Hom[ g ] a′ b′} (p : f ≡ f') (q : g ≡ g') - → hom[ ap₂ B._∘_ p q ] (f′ E.∘′ g′) ≡ hom[ p ] f′ E.∘′ hom[ q ] g′ + → hom[ ap₂ _∘_ p q ] (f′ ∘′ g′) ≡ hom[ p ] f′ ∘′ hom[ q ] g′ split p q = - reindex _ (ap₂ B._∘_ p refl ∙ ap₂ B._∘_ refl q) + reindex _ (ap₂ _∘_ p refl ∙ ap₂ _∘_ refl q) ·· sym (hom[]-∙ _ _) ·· ap hom[ _ ] (sym (whisker-l p)) ∙ sym (whisker-r q) liberate - : ∀ {a b x y} {f : B.Hom a b} {f′ : E.Hom[ f ] x y} + : ∀ {a b x y} {f : Hom a b} {f′ : Hom[ f ] x y} (p : f ≡ f) → hom[ p ] f′ ≡ f′ liberate p = reindex p refl ∙ transport-refl _ hom[]⟩⟨_ - : ∀ {a b} {f f' : B.Hom a b} {a′ b′} {p : f ≡ f'} - {f′ g′ : E.Hom[ f ] a′ b′} + : ∀ {a b} {f f' : Hom a b} {a′ b′} {p : f ≡ f'} + {f′ g′ : Hom[ f ] a′ b′} → f′ ≡ g′ → hom[ p ] f′ ≡ hom[ p ] g′ hom[]⟩⟨_ = ap hom[ _ ] _⟩∘′⟨_ - : ∀ {a b c} {f f' : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′} - {f₁′ : E.Hom[ f ] b′ c′} {f₂′ : E.Hom[ f' ] b′ c′} - {g₁′ : E.Hom[ g ] a′ b′} {g₂′ : E.Hom[ g' ] a′ b′} + : ∀ {a b c} {f f' : Hom b c} {g g' : Hom a b} {a′ b′ c′} + {f₁′ : Hom[ f ] b′ c′} {f₂′ : Hom[ f' ] b′ c′} + {g₁′ : Hom[ g ] a′ b′} {g₂′ : Hom[ g' ] a′ b′} {p : f ≡ f'} {q : g ≡ g'} - → PathP (λ i → E.Hom[ p i ] b′ c′) f₁′ f₂′ - → PathP (λ i → E.Hom[ q i ] a′ b′) g₁′ g₂′ - → hom[ p ] f₁′ E.∘′ hom[ q ] g₁′ ≡ f₂′ E.∘′ g₂′ -p ⟩∘′⟨ q = ap₂ E._∘′_ (from-pathp p) (from-pathp q) + → PathP (λ i → Hom[ p i ] b′ c′) f₁′ f₂′ + → PathP (λ i → Hom[ q i ] a′ b′) g₁′ g₂′ + → hom[ p ] f₁′ ∘′ hom[ q ] g₁′ ≡ f₂′ ∘′ g₂′ +p ⟩∘′⟨ q = ap₂ _∘′_ (from-pathp p) (from-pathp q) _⟩∘′⟨refl - : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {a′ b′ c′} - {f₁′ : E.Hom[ f ] b′ c′} {f₂′ : E.Hom[ f' ] b′ c′} {g′ : E.Hom[ g ] a′ b′} + : ∀ {a b c} {f f' : Hom b c} {g : Hom a b} {a′ b′ c′} + {f₁′ : Hom[ f ] b′ c′} {f₂′ : Hom[ f' ] b′ c′} {g′ : Hom[ g ] a′ b′} {p : f ≡ f'} - → PathP (λ i → E.Hom[ p i ] b′ c′) f₁′ f₂′ - → hom[ p ] f₁′ E.∘′ g′ ≡ f₂′ E.∘′ g′ -p ⟩∘′⟨refl = ap₂ E._∘′_ (from-pathp p) refl + → PathP (λ i → Hom[ p i ] b′ c′) f₁′ f₂′ + → hom[ p ] f₁′ ∘′ g′ ≡ f₂′ ∘′ g′ +p ⟩∘′⟨refl = ap₂ _∘′_ (from-pathp p) refl refl⟩∘′⟨_ - : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′} - {f′ : E.Hom[ f ] b′ c′} - {g₁′ : E.Hom[ g ] a′ b′} {g₂′ : E.Hom[ g' ] a′ b′} + : ∀ {a b c} {f : Hom b c} {g g' : Hom a b} {a′ b′ c′} + {f′ : Hom[ f ] b′ c′} + {g₁′ : Hom[ g ] a′ b′} {g₂′ : Hom[ g' ] a′ b′} {q : g ≡ g'} - → PathP (λ i → E.Hom[ q i ] a′ b′) g₁′ g₂′ - → f′ E.∘′ hom[ q ] g₁′ ≡ f′ E.∘′ g₂′ -refl⟩∘′⟨ p = ap₂ E._∘′_ refl (from-pathp p) + → PathP (λ i → Hom[ q i ] a′ b′) g₁′ g₂′ + → f′ ∘′ hom[ q ] g₁′ ≡ f′ ∘′ g₂′ +refl⟩∘′⟨ p = ap₂ _∘′_ refl (from-pathp p) split⟩⟨_ - : ∀ {a b c} {f f' : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′} - {f₁′ : E.Hom[ f ] b′ c′} {f₂′ : E.Hom[ f' ] b′ c′} - {g₁′ : E.Hom[ g ] a′ b′} {g₂′ : E.Hom[ g' ] a′ b′} + : ∀ {a b c} {f f' : Hom b c} {g g' : Hom a b} {a′ b′ c′} + {f₁′ : Hom[ f ] b′ c′} {f₂′ : Hom[ f' ] b′ c′} + {g₁′ : Hom[ g ] a′ b′} {g₂′ : Hom[ g' ] a′ b′} {p : f ≡ f'} {q : g ≡ g'} - → hom[ p ] f₁′ E.∘′ hom[ q ] g₁′ ≡ f₂′ E.∘′ g₂′ - → hom[ ap₂ B._∘_ p q ] (f₁′ E.∘′ g₁′) ≡ f₂′ E.∘′ g₂′ + → hom[ p ] f₁′ ∘′ hom[ q ] g₁′ ≡ f₂′ ∘′ g₂′ + → hom[ ap₂ _∘_ p q ] (f₁′ ∘′ g₁′) ≡ f₂′ ∘′ g₂′ split⟩⟨ p = split _ _ ∙ p infixr 5 _⟩∘′⟨_ refl⟩∘′⟨_ _⟩∘′⟨refl infixl 4 split⟩⟨_ hom[]⟩⟨_ -hom[] : ∀ {a b x y} {f g : B.Hom a b} {p : f ≡ g} → E.Hom[ f ] x y → E.Hom[ g ] x y +hom[] : ∀ {a b x y} {f g : Hom a b} {p : f ≡ g} → Hom[ f ] x y → Hom[ g ] x y hom[] {p = p} f′ = hom[ p ] f′ pulll-indexr - : ∀ {a b c d} {f : B.Hom c d} {g : B.Hom b c} {h : B.Hom a b} {ac : B.Hom a c} - {a′ : E.Ob[ a ]} {b′ : E.Ob[ b ]} {c′ : E.Ob[ c ]} {d′ : E.Ob[ d ]} - {f′ : E.Hom[ f ] c′ d′} - {g′ : E.Hom[ g ] b′ c′} - {h′ : E.Hom[ h ] a′ b′} - {fg′ : E.Hom[ f B.∘ g ] b′ d′} - → (p : g B.∘ h ≡ ac) - → (f′ E.∘′ g′ ≡ fg′) - → f′ E.∘′ hom[ p ] (g′ E.∘′ h′) ≡ hom[ B.pullr p ] (fg′ E.∘′ h′) + : ∀ {a b c d} {f : Hom c d} {g : Hom b c} {h : Hom a b} {ac : Hom a c} + {a′ : Ob[ a ]} {b′ : Ob[ b ]} {c′ : Ob[ c ]} {d′ : Ob[ d ]} + {f′ : Hom[ f ] c′ d′} + {g′ : Hom[ g ] b′ c′} + {h′ : Hom[ h ] a′ b′} + {fg′ : Hom[ f ∘ g ] b′ d′} + → (p : g ∘ h ≡ ac) + → (f′ ∘′ g′ ≡ fg′) + → f′ ∘′ hom[ p ] (g′ ∘′ h′) ≡ hom[ pullr p ] (fg′ ∘′ h′) pulll-indexr p q = whisker-r _ ∙ - sym ( reindex _ (sym (B.assoc _ _ _) ∙ ap (_ B.∘_) p) ·· sym (hom[]-∙ _ _) - ·· ap hom[] ( ap hom[] (ap (E._∘′ _) (sym q)) - ∙ from-pathp (symP (E.assoc′ _ _ _)))) + sym ( reindex _ (sym (assoc _ _ _) ∙ ap (_ ∘_) p) ·· sym (hom[]-∙ _ _) + ·· ap hom[] ( ap hom[] (ap (_∘′ _) (sym q)) + ∙ from-pathp (symP (assoc′ _ _ _)))) ``` Using these tools, we can define displayed versions of the usual category @@ -315,9 +313,6 @@ reasoning combinators. diff --git a/src/Cat/Functor/Hom/Displayed.lagda.md b/src/Cat/Functor/Hom/Displayed.lagda.md index 6a40d160e..44b3d3708 100644 --- a/src/Cat/Functor/Hom/Displayed.lagda.md +++ b/src/Cat/Functor/Hom/Displayed.lagda.md @@ -20,7 +20,6 @@ module Cat.Functor.Hom.Displayed + +```agda +module Cat.Displayed.Functor.VerticalReasoning + {ob ℓb oe ℓe of ℓf} + {B : Precategory ob ℓb} + {ℰ : Displayed B oe ℓe} {ℱ : Displayed B of ℓf} + (F : Vertical-functor ℰ ℱ) + where +``` + + + +```agda +F-∘[] + : ∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y} {h : Hom x z} + → {p : f ∘ g ≡ h} + → (f′ : ℰ.Hom[ f ] y′ z′) (g′ : ℰ.Hom[ g ] x′ y′) + → F₁′ (ℰ.hom[ p ] (f′ ℰ.∘′ g′)) ≡ ℱ.hom[ p ] (F₁′ f′ ℱ.∘′ F₁′ g′) +F-∘[] {x′ = x′} {z′ = z′} {p = p} f′ g′ i = + comp (λ j → ℱ.Hom[ p j ] (F₀′ x′) (F₀′ z′)) (∂ i) λ where + j (i = i0) → + F₁′ (transp (λ i → ℰ.Hom[ p (i ∧ j) ] x′ z′) (~ j) (f′ ℰ.∘′ g′)) + j (i = i1) → + transp (λ i → ℱ.Hom[ p (i ∧ j) ] (F₀′ x′) (F₀′ z′)) (~ j) + (F₁′ f′ ℱ.∘′ F₁′ g′) + j (j = i0) → F-∘′ {f′ = f′} {g′ = g′} i +``` + +```agda +collapse′ + : ∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y} {h : Hom x z} + → {f′ : ℰ.Hom[ f ] y′ z′} {g′ : ℰ.Hom[ g ] x′ y′} {h′ : ℰ.Hom[ h ] x′ z′} + → {p : f ∘ g ≡ h} + → f′ ℰ.∘′ g′ ℰ.≡[ p ] h′ + → F₁′ f′ ℱ.∘′ F₁′ g′ ℱ.≡[ p ] F₁′ h′ +collapse′ q = ℱ.cast[] (symP F-∘′ ℱ.∙[] (λ i → F₁′ (q i))) +``` From 411c580515b2017ca00919fb6bc83fc4ee3bdf2a Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 4 May 2023 17:21:35 -0700 Subject: [PATCH 05/10] def: vertical adjuncts, all right vertical adjoints are fibred --- src/Cat/Displayed/Adjoint.lagda.md | 233 +++++++++++++++++++++++++++-- 1 file changed, 222 insertions(+), 11 deletions(-) diff --git a/src/Cat/Displayed/Adjoint.lagda.md b/src/Cat/Displayed/Adjoint.lagda.md index 1233ad61e..e39f2dbeb 100644 --- a/src/Cat/Displayed/Adjoint.lagda.md +++ b/src/Cat/Displayed/Adjoint.lagda.md @@ -1,11 +1,18 @@ @@ -103,10 +110,10 @@ module _ {ℱ : Displayed B of ℓf} where private - open Precategory B - module ℰ = Displayed ℰ - module ℱ = Displayed ℱ - open Vertical-fibred-functor + open Cat.Reasoning B + module ℱ = Cat.Displayed.Reasoning ℱ + module ℰ = Cat.Displayed.Reasoning ℰ + open Vertical-functor lvl : Level lvl = ob ⊔ ℓb ⊔ oe ⊔ ℓe ⊔ of ⊔ ℓf @@ -117,13 +124,13 @@ module _ ```agda record _⊣↓_ - (L : Vertical-fibred-functor ℰ ℱ) - (R : Vertical-fibred-functor ℱ ℰ) + (L : Vertical-functor ℰ ℱ) + (R : Vertical-functor ℱ ℰ) : Type lvl where no-eta-equality field - unit′ : IdVf =>f↓ R Vf∘ L - counit′ : L Vf∘ R =>f↓ IdVf + unit′ : IdV =>↓ R V∘ L + counit′ : L V∘ R =>↓ IdV module unit′ = _=>↓_ unit′ module counit′ = _=>↓_ counit′ renaming (η′ to ε′) @@ -133,4 +140,208 @@ module _ → counit′.ε′ (L .F₀′ x′) ℱ.∘′ L .F₁′ (unit′.η′ x′) ℱ.≡[ idl id ] ℱ.id′ zag′ : ∀ {x} {x′ : ℱ.Ob[ x ]} → R .F₁′ (counit′.ε′ x′) ℰ.∘′ unit′.η′ (R .F₀′ x′) ℰ.≡[ idl id ] ℰ.id′ + + _⊣f↓_ : Vertical-fibred-functor ℰ ℱ → Vertical-fibred-functor ℱ ℰ → Type _ + L ⊣f↓ R = Vertical-fibred-functor.vert L ⊣↓ Vertical-fibred-functor.vert R ``` + +## Vertical Adjuncts + +If $L \dashv R$ is a vertical adjunction, then we can define displayed +versions of [adjuncts]. The vertical assumption is critical here; it +allows us to keep morphisms displayed over the same base. + +[adjuncts]: Cat.Functor.Adjoint.html#adjuncts + + + +```agda + L-adjunct′ + : ∀ {x y x′ y′} {f : Hom x y} + → ℱ.Hom[ f ] (L.₀′ x′) y′ → ℰ.Hom[ f ] x′ (R.₀′ y′) + L-adjunct′ f′ = ℰ.hom[ idr _ ] (R.₁′ f′ ℰ.∘′ unit′.η′ _) + + R-adjunct′ + : ∀ {x y x′ y′} {f : Hom x y} + → ℰ.Hom[ f ] x′ (R.₀′ y′) → ℱ.Hom[ f ] (L.₀′ x′) y′ + R-adjunct′ f′ = ℱ.hom[ idl _ ] (counit′.ε′ _ ℱ.∘′ L.₁′ f′) +``` + +As in the 1-categorical case, we obtain an equivalence between hom-sets +$\hom(La,b)$ and $\hom(a,Rb)$ over $f$. + +```agda + L-R-adjunct′ + : ∀ {x y} {f : Hom x y} {x′ : ℰ.Ob[ x ]} {y′ : ℱ.Ob[ y ]} + → is-right-inverse (R-adjunct′ {x′ = x′} {y′} {f}) L-adjunct′ + L-R-adjunct′ f′ = + ℰ.hom[] (R.₁′ (ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ f′)) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.weave _ _ (idr _) (ap₂ ℰ._∘′_ (R.F-∘[] _ _) refl) ⟩ + ℰ.hom[] (ℰ.hom[] (R.₁′ (counit′.ε′ _) ℰ.∘′ R.₁′ (L.₁′ f′)) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.smashl _ _ ⟩ + ℰ.hom[] ((R.₁′ (counit′.ε′ _) ℰ.∘′ R.₁′ (L.₁′ f′)) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.weave _ _ (eliml (idl _)) (ℰ.extendr[] _ (symP $ unit′.is-natural′ _ _ _)) ⟩ + ℰ.hom[] ((R.₁′ (counit′.ε′ _) ℰ.∘′ unit′.η′ _) ℰ.∘′ f′) ≡⟨ ℰ.shiftl _ (ℰ.eliml[] _ zag′) ⟩ + f′ ∎ + + R-L-adjunct′ + : ∀ {x y} {f : Hom x y} {x′ : ℰ.Ob[ x ]} {y′ : ℱ.Ob[ y ]} + → is-left-inverse (R-adjunct′ {x′ = x′} {y′} {f}) L-adjunct′ + R-L-adjunct′ f′ = + ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ (ℰ.hom[] (R.₁′ f′ ℰ.∘′ unit′.η′ _))) ≡⟨ ℱ.weave _ _ (idl _) (ap₂ ℱ._∘′_ refl (L.F-∘[] _ _)) ⟩ + ℱ.hom[] (counit′.ε′ _ ℱ.∘′ ℱ.hom[] (L.₁′ (R.₁′ f′) ℱ.∘′ L.₁′ (unit′.η′ _))) ≡⟨ ℱ.smashr _ _ ⟩ + ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ (R.₁′ f′) ℱ.∘′ L.₁′ (unit′.η′ _)) ≡⟨ ℱ.weave _ _ (elimr (idl _)) (ℱ.extendl[] _ (counit′.is-natural′ _ _ _)) ⟩ + ℱ.hom[] (f′ ℱ.∘′ counit′.ε′ _ ℱ.∘′ L.₁′ (unit′.η′ _)) ≡⟨ ℱ.shiftl _ (ℱ.elimr[] _ zig′) ⟩ + f′ ∎ +``` + +This equivalence is natural. + +```agda + L-adjunct-naturall′ + : ∀ {x y z} {x′ : ℰ.Ob[ x ]} {y′ : ℰ.Ob[ y ]} {z′ : ℱ.Ob[ z ]} + → {f : Hom y z} {g : Hom x y} + → (f′ : ℱ.Hom[ f ] (L.₀′ y′) z′) (g′ : ℰ.Hom[ g ] x′ y′) + → L-adjunct′ (f′ ℱ.∘′ L.₁′ g′) ≡ L-adjunct′ f′ ℰ.∘′ g′ + L-adjunct-naturall′ {g = g} f′ g′ = + ℰ.hom[] (R.₁′ (f′ ℱ.∘′ L.₁′ g′) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.weave _ _ (idr _) (ap₂ ℰ._∘′_ R.F-∘′ refl) ⟩ + ℰ.hom[] ((R.₁′ f′ ℰ.∘′ R.₁′ (L.₁′ g′)) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.weave _ _ (ap (_∘ g) (idr _)) (ℰ.extendr[] _ (symP $ unit′.is-natural′ _ _ _)) ⟩ + ℰ.hom[] ((R.₁′ f′ ℰ.∘′ unit′.η′ _) ℰ.∘′ g′) ≡⟨ ℰ.unwhisker-l _ _ ⟩ + ℰ.hom[] (R.₁′ f′ ℰ.∘′ unit′.η′ _) ℰ.∘′ g′ ∎ + + L-adjunct-naturalr′ + : ∀ {x y z} {x′ : ℰ.Ob[ x ]} {y′ : ℱ.Ob[ y ]} {z′ : ℱ.Ob[ z ]} + → {f : Hom y z} {g : Hom x y} + → (f′ : ℱ.Hom[ f ] y′ z′) (g′ : ℱ.Hom[ g ] (L.₀′ x′) y′) + → L-adjunct′ (f′ ℱ.∘′ g′) ≡ R.₁′ f′ ℰ.∘′ L-adjunct′ g′ + L-adjunct-naturalr′ {f = f} f′ g′ = + ℰ.hom[] (R.₁′ (f′ ℱ.∘′ g′) ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.weave _ _ (ap (f ∘_) (idr _)) (ℰ.pushl[] _ R.F-∘′) ⟩ + ℰ.hom[] (R.₁′ f′ ℰ.∘′ R.₁′ g′ ℰ.∘′ unit′.η′ _) ≡⟨ ℰ.unwhisker-r _ _ ⟩ + R.₁′ f′ ℰ.∘′ ℰ.hom[] (R.₁′ g′ ℰ.∘′ unit′.η′ _) ∎ + + R-adjunct-naturall′ + : ∀ {x y z} {x′ : ℰ.Ob[ x ]} {y′ : ℰ.Ob[ y ]} {z′ : ℱ.Ob[ z ]} + → {f : Hom y z} {g : Hom x y} + → (f′ : ℰ.Hom[ f ] y′ (R.₀′ z′)) (g′ : ℰ.Hom[ g ] x′ y′) + → R-adjunct′ (f′ ℰ.∘′ g′) ≡ R-adjunct′ f′ ℱ.∘′ L.₁′ g′ + R-adjunct-naturall′ {g = g} f′ g′ = + ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ (f′ ℰ.∘′ g′)) ≡⟨ ℱ.weave _ _ (ap (_∘ g) (idl _)) (ℱ.pushr[] _ L.F-∘′) ⟩ + ℱ.hom[] ((counit′.ε′ _ ℱ.∘′ L.₁′ f′) ℱ.∘′ L.F₁′ g′) ≡⟨ ℱ.unwhisker-l _ _ ⟩ + ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ f′) ℱ.∘′ L.₁′ g′ ∎ + + R-adjunct-naturalr′ + : ∀ {x y z} {x′ : ℰ.Ob[ x ]} {y′ : ℱ.Ob[ y ]} {z′ : ℱ.Ob[ z ]} + → {f : Hom y z} {g : Hom x y} + → (f′ : ℱ.Hom[ f ] y′ z′) (g′ : ℰ.Hom[ g ] x′ (R.₀′ y′)) + → R-adjunct′ (R.₁′ f′ ℰ.∘′ g′) ≡ f′ ℱ.∘′ R-adjunct′ g′ + R-adjunct-naturalr′ {f = f} f′ g′ = + ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ (R.₁′ f′ ℰ.∘′ g′)) ≡⟨ ℱ.weave _ _ (idl _) (ap₂ ℱ._∘′_ refl L.F-∘′) ⟩ + ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ (R.₁′ f′) ℱ.∘′ L.₁′ g′) ≡⟨ ℱ.weave _ _ (ap (f ∘_) (idl _)) (ℱ.extendl[] _ (counit′.is-natural′ _ _ _)) ⟩ + ℱ.hom[] (f′ ℱ.∘′ counit′.ε′ _ ℱ.∘′ L.₁′ g′) ≡⟨ ℱ.unwhisker-r _ _ ⟩ + f′ ℱ.∘′ ℱ.hom[] (counit′.ε′ _ ℱ.∘′ L.₁′ g′) ∎ +``` + +## Vertical Right Adjoints are Fibred + +If $L \dashv R$ is a vertical adjunction, then $R$ is a fibred functor. + +```agda + Vert-right-adjoint-fibred + : {L : Vertical-functor ℰ ℱ} {R : Vertical-functor ℱ ℰ} + → L ⊣↓ R + → is-vertical-fibred R + Vert-right-adjoint-fibred {L = L} {R = R} adj {f = f} f′ cart = R-cart where + open is-cartesian + open _⊣↓_ adj + open _=>↓_ + module L = Cat.Displayed.Functor.VerticalReasoning L + module R = Cat.Displayed.Functor.VerticalReasoning R +``` + +Let $f : \cC(x,y)$ and $f' : \cF(x', y')_{f}$ be a cartesian morphism. +To show that $R$ is fibred, we need to show that $R(f')$ is cartesian. +Let $m : \cC(a, x)$, and $h' : \cE(a', y')_{f \circ m}$; we need to +construct a universal factorization of $h'$ through $R(f')$. + +As $f'$ is cartesian, we can perform the following factorization of +the left adjunct $\varepsilon \circ L(h')$ of $h$, yielding a map +$\hat{h} : \cF(a', x')$. + +~~~{.quiver} +\begin{tikzcd} + {a'} \\ + & {x'} && {y'} \\ + a \\ + & y && x + \arrow["{f'}", from=2-2, to=2-4] + \arrow["f", from=4-2, to=4-4] + \arrow[lies over, from=2-2, to=4-2] + \arrow[lies over, from=2-4, to=4-4] + \arrow["m", from=3-1, to=4-2] + \arrow["{\varepsilon \circ L(h')}", curve={height=-12pt}, from=1-1, to=2-4] + \arrow[lies over, from=1-1, to=3-1] + \arrow["{f \circ m}", curve={height=-12pt}, from=3-1, to=4-4] + \arrow["{\exists! \hat{h}}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=1-1, to=2-2] +\end{tikzcd} +~~~ + +We can then take the right adjunct $R(\hat{h}) \circ \eta$ of $\hat{h}$ +to obtain the desired factorization. + + +```agda + R-cart : is-cartesian ℰ f (R.F₁′ f′) + R-cart .universal m h′ = + L-adjunct′ adj (cart .universal m (R-adjunct′ adj h′)) +``` + +
+Showing that this factorization is universal is a matter of +pushing around the adjuncts. + + +```agda + R-cart .commutes m h′ = + (R.F₁′ f′ ℰ.∘′ L-adjunct′ adj (cart .universal m (R-adjunct′ adj h′))) ≡˘⟨ L-adjunct-naturalr′ adj _ _ ⟩ + L-adjunct′ adj (f′ ℱ.∘′ cart .universal m (R-adjunct′ adj h′)) ≡⟨ ap (L-adjunct′ adj) (cart .commutes _ _) ⟩ + L-adjunct′ adj (R-adjunct′ adj h′) ≡⟨ L-R-adjunct′ adj h′ ⟩ + h′ ∎ + R-cart .unique {m = m} {h′ = h′} m′ p = + m′ ≡˘⟨ L-R-adjunct′ adj m′ ⟩ + L-adjunct′ adj (R-adjunct′ adj m′) ≡⟨ ap (L-adjunct′ adj) (cart .unique _ (sym $ R-adjunct-naturalr′ adj _ _)) ⟩ + L-adjunct′ adj (cart .universal m (R-adjunct′ adj ⌜ R .F₁′ f′ ℰ.∘′ m′ ⌝)) ≡⟨ ap! p ⟩ + L-adjunct′ adj (cart .universal m (R-adjunct′ adj h′)) ∎ +``` +
+ +## Adjunctions between Fibre Categories + +Vertical adjunctions yield adjunctions between fibre categories. + +```agda + vertical-adjunction→fibre-adjunction + : ∀ {L : Vertical-functor ℰ ℱ} {R : Vertical-functor ℱ ℰ} + → L ⊣↓ R + → ∀ x → Restrict↓ L x ⊣ Restrict↓ R x + vertical-adjunction→fibre-adjunction {L = L} {R = R} vadj x = adj where + open _⊣↓_ vadj + open _⊣_ + open _=>_ + open _=>↓_ + + adj : Restrict↓ L x ⊣ Restrict↓ R x + adj .unit .η x = unit′ .η′ x + adj .unit .is-natural x′ y′ f′ = + Vert-nat-restrict {F′ = IdV} {G′ = R V∘ L} unit′ x .is-natural x′ y′ f′ + adj .counit .η x = counit′ .η′ x + adj .counit .is-natural x′ y′ f′ = + Vert-nat-restrict {F′ = L V∘ R} {G′ = IdV} counit′ x .is-natural x′ y′ f′ + adj .zig = from-pathp zig′ + adj .zag = from-pathp zag′ +``` + From a9b3726d9953684d7b8c4a4bf6821d633f538802 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 4 May 2023 17:46:58 -0700 Subject: [PATCH 06/10] def: vertical left adjoints are opfibred --- src/Cat/Displayed/Adjoint.lagda.md | 46 ++++++++++++++++++++++++++---- src/Cat/Displayed/Functor.lagda.md | 42 ++++++++++++++++++++++++++- 2 files changed, 81 insertions(+), 7 deletions(-) diff --git a/src/Cat/Displayed/Adjoint.lagda.md b/src/Cat/Displayed/Adjoint.lagda.md index e39f2dbeb..ee3be6edf 100644 --- a/src/Cat/Displayed/Adjoint.lagda.md +++ b/src/Cat/Displayed/Adjoint.lagda.md @@ -2,6 +2,7 @@ ```agda open import Cat.Displayed.Base open import Cat.Displayed.Cartesian +open import Cat.Displayed.Cocartesian open import Cat.Displayed.Fibre open import Cat.Displayed.Functor @@ -255,10 +256,8 @@ If $L \dashv R$ is a vertical adjunction, then $R$ is a fibred functor. : {L : Vertical-functor ℰ ℱ} {R : Vertical-functor ℱ ℰ} → L ⊣↓ R → is-vertical-fibred R - Vert-right-adjoint-fibred {L = L} {R = R} adj {f = f} f′ cart = R-cart where + Vert-right-adjoint-fibred {L = L} {R = R} adj {f = f} f′ cart = R-cart where open is-cartesian - open _⊣↓_ adj - open _=>↓_ module L = Cat.Displayed.Functor.VerticalReasoning L module R = Cat.Displayed.Functor.VerticalReasoning R ``` @@ -307,9 +306,9 @@ pushing around the adjuncts. ```agda R-cart .commutes m h′ = - (R.F₁′ f′ ℰ.∘′ L-adjunct′ adj (cart .universal m (R-adjunct′ adj h′))) ≡˘⟨ L-adjunct-naturalr′ adj _ _ ⟩ - L-adjunct′ adj (f′ ℱ.∘′ cart .universal m (R-adjunct′ adj h′)) ≡⟨ ap (L-adjunct′ adj) (cart .commutes _ _) ⟩ - L-adjunct′ adj (R-adjunct′ adj h′) ≡⟨ L-R-adjunct′ adj h′ ⟩ + R.F₁′ f′ ℰ.∘′ L-adjunct′ adj (cart .universal m (R-adjunct′ adj h′)) ≡˘⟨ L-adjunct-naturalr′ adj _ _ ⟩ + L-adjunct′ adj (f′ ℱ.∘′ cart .universal m (R-adjunct′ adj h′)) ≡⟨ ap (L-adjunct′ adj) (cart .commutes _ _) ⟩ + L-adjunct′ adj (R-adjunct′ adj h′) ≡⟨ L-R-adjunct′ adj h′ ⟩ h′ ∎ R-cart .unique {m = m} {h′ = h′} m′ p = m′ ≡˘⟨ L-R-adjunct′ adj m′ ⟩ @@ -319,6 +318,41 @@ pushing around the adjuncts. ``` +Dually, vertical left adjoints are opfibred. + +```agda + Vert-left-adjoint-opfibred + : {L : Vertical-functor ℰ ℱ} {R : Vertical-functor ℱ ℰ} + → L ⊣↓ R + → is-vertical-opfibred L +``` + +
+The proof is entirely dual to the one for right adjoints. + +```agda + Vert-left-adjoint-opfibred {L = L} {R = R} adj {f = f} f′ cocart = L-cocart where + open is-cocartesian + module L = Cat.Displayed.Functor.VerticalReasoning L + module R = Cat.Displayed.Functor.VerticalReasoning R + + L-cocart : is-cocartesian ℱ f (L.F₁′ f′) + L-cocart .universal m h′ = + R-adjunct′ adj (cocart .universal m (L-adjunct′ adj h′)) + L-cocart .commutes m h′ = + R-adjunct′ adj (cocart .universal m (L-adjunct′ adj h′)) ℱ.∘′ L.F₁′ f′ ≡˘⟨ R-adjunct-naturall′ adj _ _ ⟩ + R-adjunct′ adj (cocart .universal m (L-adjunct′ adj h′) ℰ.∘′ f′) ≡⟨ ap (R-adjunct′ adj) (cocart .commutes _ _) ⟩ + R-adjunct′ adj (L-adjunct′ adj h′) ≡⟨ R-L-adjunct′ adj h′ ⟩ + h′ ∎ + L-cocart .unique {m = m} {h′ = h′} m′ p = + m′ ≡˘⟨ R-L-adjunct′ adj m′ ⟩ + R-adjunct′ adj (L-adjunct′ adj m′) ≡⟨ ap (R-adjunct′ adj) (cocart .unique _ (sym $ L-adjunct-naturall′ adj _ _)) ⟩ + R-adjunct′ adj (cocart .universal m (L-adjunct′ adj ⌜ m′ ℱ.∘′ L .F₁′ f′ ⌝)) ≡⟨ ap! p ⟩ + R-adjunct′ adj (cocart .universal m (L-adjunct′ adj h′)) ∎ +``` +
+ + ## Adjunctions between Fibre Categories Vertical adjunctions yield adjunctions between fibre categories. diff --git a/src/Cat/Displayed/Functor.lagda.md b/src/Cat/Displayed/Functor.lagda.md index d39c3e164..d24562a35 100644 --- a/src/Cat/Displayed/Functor.lagda.md +++ b/src/Cat/Displayed/Functor.lagda.md @@ -1,6 +1,7 @@ @@ -158,8 +158,8 @@ allows us to keep morphisms displayed over the same base. ```agda module _ {L : Vertical-functor ℰ ℱ} {R : Vertical-functor ℱ ℰ} (adj : L ⊣↓ R) where private - module L = Cat.Displayed.Functor.VerticalReasoning L - module R = Cat.Displayed.Functor.VerticalReasoning R + module L = Cat.Displayed.Functor.Vertical.Reasoning L + module R = Cat.Displayed.Functor.Vertical.Reasoning R open _⊣↓_ adj ``` --> @@ -258,8 +258,8 @@ If $L \dashv R$ is a vertical adjunction, then $R$ is a fibred functor. → is-vertical-fibred R Vert-right-adjoint-fibred {L = L} {R = R} adj {f = f} f′ cart = R-cart where open is-cartesian - module L = Cat.Displayed.Functor.VerticalReasoning L - module R = Cat.Displayed.Functor.VerticalReasoning R + module L = Cat.Displayed.Functor.Vertical.Reasoning L + module R = Cat.Displayed.Functor.Vertical.Reasoning R ``` Let $f : \cC(x,y)$ and $f' : \cF(x', y')_{f}$ be a cartesian morphism. @@ -333,8 +333,8 @@ Dually, vertical left adjoints are opfibred. ```agda Vert-left-adjoint-opfibred {L = L} {R = R} adj {f = f} f′ cocart = L-cocart where open is-cocartesian - module L = Cat.Displayed.Functor.VerticalReasoning L - module R = Cat.Displayed.Functor.VerticalReasoning R + module L = Cat.Displayed.Functor.Vertical.Reasoning L + module R = Cat.Displayed.Functor.Vertical.Reasoning R L-cocart : is-cocartesian ℱ f (L.F₁′ f′) L-cocart .universal m h′ = diff --git a/src/Cat/Displayed/Functor/VerticalReasoning.lagda.md b/src/Cat/Displayed/Functor/Vertical/Reasoning.lagda.md similarity index 97% rename from src/Cat/Displayed/Functor/VerticalReasoning.lagda.md rename to src/Cat/Displayed/Functor/Vertical/Reasoning.lagda.md index 2c4e2ae56..b3f95e6bd 100644 --- a/src/Cat/Displayed/Functor/VerticalReasoning.lagda.md +++ b/src/Cat/Displayed/Functor/Vertical/Reasoning.lagda.md @@ -10,7 +10,7 @@ import Cat.Displayed.Reasoning --> ```agda -module Cat.Displayed.Functor.VerticalReasoning +module Cat.Displayed.Functor.Vertical.Reasoning {ob ℓb oe ℓe of ℓf} {B : Precategory ob ℓb} {ℰ : Displayed B oe ℓe} {ℱ : Displayed B of ℓf} diff --git a/src/index.lagda.md b/src/index.lagda.md index 4c33ee3b7..c5eb30e77 100644 --- a/src/index.lagda.md +++ b/src/index.lagda.md @@ -657,6 +657,9 @@ their higher groupoid structure: open import Cat.Displayed.Path open import Cat.Displayed.Functor open import Cat.Displayed.Adjoint + +open import Cat.Displayed.Functor.Vertical.Reasoning +-- Reasoning Combinators for vertical functors. ``` ### Cartesian fibrations From 401512aa974c154b4e8ddbb70ea4f5a7c079e3ea Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 4 May 2023 17:54:48 -0700 Subject: [PATCH 09/10] fix: fix link --- src/Cat/Displayed/Functor/Vertical/Reasoning.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cat/Displayed/Functor/Vertical/Reasoning.lagda.md b/src/Cat/Displayed/Functor/Vertical/Reasoning.lagda.md index b3f95e6bd..6ccafead2 100644 --- a/src/Cat/Displayed/Functor/Vertical/Reasoning.lagda.md +++ b/src/Cat/Displayed/Functor/Vertical/Reasoning.lagda.md @@ -23,7 +23,7 @@ module Cat.Displayed.Functor.Vertical.Reasoning This module provides versions of the [functor reasoning combinators][func] that have been adapted to work with vertical functors. -[func]: Cat.Functor.Reasoning +[func]: Cat.Functor.Reasoning.html