Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Right adjoint to Functor.Slice.Free #408

Draft
wants to merge 8 commits into
base: master
Choose a base branch
from
Draft

Right adjoint to Functor.Slice.Free #408

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
44363cc
First shot of other adjoint functor
Taneb Jan 9, 2024
56f4a35
Define adjoint
Taneb Jan 10, 2024
5559e74
Use cancel-r
Taneb Jan 24, 2024
0322606
Define first-cong and second-cong, use throughout
Taneb Jan 24, 2024
11dddb7
Make pullback-functorial less forgetful
Taneb Jan 27, 2024
bf07868
Rename slice functors
Taneb Jan 27, 2024
723fe77
Remove Functor.Slice.BaseChange
Taneb Jan 27, 2024
ce4a518
Remove accidentally added import
Taneb Jan 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
103 changes: 101 additions & 2 deletions src/Categories/Adjoint/Instance/Slice.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,18 @@ open import Categories.Category using (Category)
module Categories.Adjoint.Instance.Slice {o ℓ e} (C : Category o ℓ e) where

open import Categories.Adjoint using (_⊣_)
open import Categories.Category.Slice C using (SliceObj; Slice⇒; slicearr)
open import Categories.Functor.Slice C using (Forgetful; Free)
open import Categories.Category.BinaryProducts C
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.CartesianClosed using (CartesianClosed)
open import Categories.Category.Slice C using (SliceObj; sliceobj; Slice⇒; slicearr)
open import Categories.Functor.Slice C using (Forgetful; Free; Coforgetful)
open import Categories.Morphism.Reasoning C
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.Diagram.Pullback C hiding (swap)
open import Categories.Object.Product C
open import Categories.Object.Terminal C

open import Function.Base using (_$_)

open Category C
open HomReasoning
Expand Down Expand Up @@ -44,3 +52,94 @@ module _ {A : Obj} (product : ∀ {X} → Product A X) where
⟨ π₁ , π₂ ⟩ ≈⟨ η ⟩
id ∎
}

module _ {A : Obj} (ccc : CartesianClosed C) (pullback : ∀ {X} {Y} {Z} (h : X ⇒ Z) (i : Y ⇒ Z) → Pullback h i) where

open CartesianClosed ccc
open Cartesian cartesian
open Terminal terminal
open BinaryProducts products

Free⊣Coforgetful : Free {A = A} product ⊣ Coforgetful ccc pullback
Free⊣Coforgetful = record
{ unit = ntHelper record
{ η = λ X → p.universal (sliceobj π₁) (λ-unique₂′ (unit-pb X))
; commute = λ {S} {T} f → p.unique-diagram (sliceobj π₁) !-unique₂ $ begin
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For these longer proofs, best to put them either in where or named in a private block. Purely for efficiency.

p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ∘ f ≈⟨ pullˡ (p.p₂∘universal≈h₂ (sliceobj π₁)) ⟩
λg swap ∘ f ≈⟨ subst ⟩
λg (swap ∘ first f) ≈⟨ λ-cong swap∘⁂ ⟩
λg (second f ∘ swap) ≈˘⟨ λ-cong (∘-resp-≈ʳ β′) ⟩
λg (second f ∘ eval′ ∘ first (λg swap)) ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ (p.p₂∘universal≈h₂ (sliceobj π₁)) Equiv.refl))) ⟩
λg (second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _)) ≈˘⟨ λ-cong (pull-last first∘first) ⟩
λg ((second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ first (p.universal (sliceobj π₁) _)) ≈˘⟨ subst ⟩
λg (second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ p.universal (sliceobj π₁) _ ≈˘⟨ pullˡ (p.p₂∘universal≈h₂ (sliceobj π₁)) ⟩
p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ∘ p.universal (sliceobj π₁) _ ∎
}
; counit = ntHelper record
{ η = λ X → slicearr (counit-△ X)
; commute = λ {S} {T} f → begin
(eval′ ∘ first (p.p₂ T) ∘ swap) ∘ second (p.universal T _) ≈⟨ pull-last swap∘⁂ ⟩
eval′ ∘ first (p.p₂ T) ∘ first (p.universal T _) ∘ swap ≈⟨ refl⟩∘⟨ pullˡ first∘first ⟩
eval′ ∘ first (p.p₂ T ∘ p.universal T _) ∘ swap ≈⟨ refl⟩∘⟨ ⁂-cong₂ (p.p₂∘universal≈h₂ T) Equiv.refl ⟩∘⟨refl ⟩
eval′ ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S))) ∘ swap ≈⟨ pullˡ β′ ⟩
(h f ∘ eval′ ∘ first (p.p₂ S)) ∘ swap ≈⟨ assoc²' ⟩
h f ∘ eval′ ∘ first (p.p₂ S) ∘ swap ∎
}
; zig = λ {X} → begin
(eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ swap) ∘ second (p.universal (sliceobj π₁) _) ≈⟨ assoc²' ⟩
eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ swap ∘ second (p.universal (sliceobj π₁) _) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ swap∘⁂ ⟩
eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ first (p.universal (sliceobj π₁) _) ∘ swap ≈⟨ refl⟩∘⟨ pullˡ first∘first ⟩
eval′ ∘ first (p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _) ∘ swap ≈⟨ refl⟩∘⟨ ⁂-cong₂ (p.p₂∘universal≈h₂ (sliceobj π₁)) Equiv.refl ⟩∘⟨refl ⟩
eval′ ∘ first (λg swap) ∘ swap ≈⟨ pullˡ β′ ⟩
swap ∘ swap ≈⟨ swap∘swap ⟩
id ∎
; zag = λ {X} → p.unique-diagram X !-unique₂ $ begin
p.p₂ X ∘ p.universal X _ ∘ p.universal (sliceobj π₁) _ ≈⟨ pullˡ (p.p₂∘universal≈h₂ X) ⟩
λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ p.universal (sliceobj π₁) _ ≈˘⟨ pullˡ (subst ○ λ-cong assoc) ⟩
λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ≈⟨ refl⟩∘⟨ p.p₂∘universal≈h₂ (sliceobj π₁) ⟩
λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ λg swap ≈⟨ subst ⟩
λg (((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ first (λg swap)) ≈⟨ λ-cong (pullʳ β′) ⟩
λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ swap) ≈⟨ λ-cong (pull-last swap∘swap) ⟩
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

cancel-r ?

λg (eval′ ∘ first (p.p₂ X) ∘ id) ≈⟨ λ-cong (∘-resp-≈ʳ identityʳ) ⟩
λg (eval′ ∘ first (p.p₂ X)) ≈⟨ η-exp′ ⟩
p.p₂ X ≈˘⟨ identityʳ ⟩
p.p₂ X ∘ id ∎
}
where
p : (X : SliceObj A) → Pullback {X = ⊤} {Z = A ^ A} {Y = Y X ^ A} (λg π₂) (λg (arr X ∘ eval′))
p X = pullback (λg π₂) (λg (arr X ∘ eval′))
module p X = Pullback (p X)

abstract
unit-pb : ∀ (X : Obj) → eval′ ∘ first {A = X} {C = A} (λg π₂ ∘ !) ≈ eval′ ∘ first (λg (π₁ ∘ eval′) ∘ λg swap)
unit-pb X = begin
eval′ ∘ first (λg π₂ ∘ !) ≈˘⟨ refl⟩∘⟨ first∘first ⟩
eval′ ∘ first (λg π₂) ∘ first ! ≈⟨ pullˡ β′ ⟩
π₂ ∘ first ! ≈⟨ π₂∘⁂ ○ identityˡ ⟩
π₂ ≈˘⟨ project₁ ⟩
π₁ ∘ swap ≈˘⟨ refl⟩∘⟨ β′ ⟩
π₁ ∘ eval′ ∘ first (λg swap) ≈˘⟨ extendʳ β′ ⟩
eval′ ∘ first (λg (π₁ ∘ eval′)) ∘ first (λg swap) ≈⟨ refl⟩∘⟨ first∘first ⟩
eval′ ∘ first (λg (π₁ ∘ eval′) ∘ λg swap) ∎
-- A good chunk of the above, maybe all if you squint, is duplicated with F₁-lemma
-- eval′ ∘ first (λg π₂ ∘ !) ≈ eval′ ∘ first (λg (f ∘ eval′) ∘ first (λg g)
-- With f : X ⇒ Y and g : Z × Y ⇒ X. Not sure what conditions f and g need to have

-- Would it be better if Free used π₂ rather than π₁?
-- It would mean we could avoid this swap
counit-△ : ∀ X → arr X ∘ eval′ ∘ first (p.p₂ X) ∘ swap ≈ π₁
counit-△ X = begin
arr X ∘ eval′ ∘ first (p.p₂ X) ∘ swap ≈˘⟨ assoc² ⟩
((arr X ∘ eval′) ∘ first (p.p₂ X)) ∘ swap ≈⟨ lemma ⟩∘⟨refl ⟩
(π₂ ∘ first (p.p₁ X)) ∘ swap ≈⟨ (π₂∘⁂ ○ identityˡ) ⟩∘⟨refl ⟩
π₂ ∘ swap ≈⟨ project₂ ⟩
π₁ ∎
where
lemma : (arr X ∘ eval′) ∘ first (p.p₂ X) ≈ π₂ ∘ first (p.p₁ X)
lemma = λ-inj $ begin
λg ((arr X ∘ eval′) ∘ first (p.p₂ X)) ≈˘⟨ subst ⟩
λg (arr X ∘ eval′) ∘ p.p₂ X ≈˘⟨ p.commute X ⟩
λg π₂ ∘ p.p₁ X ≈⟨ subst ⟩
λg (π₂ ∘ first (p.p₁ X)) ∎


63 changes: 62 additions & 1 deletion src/Categories/Functor/Slice.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,16 +4,22 @@ open import Categories.Category using (Category)

module Categories.Functor.Slice {o ℓ e} (C : Category o ℓ e) where

open import Function using () renaming (id to id→)
open import Function.Base using (_$_) renaming (id to id→)

open import Categories.Category.BinaryProducts
open import Categories.Category.Cartesian
open import Categories.Category.CartesianClosed C
open import Categories.Diagram.Pullback C using (Pullback; unglue; Pullback-resp-≈)
open import Categories.Functor using (Functor)
open import Categories.Functor.Properties using ([_]-resp-∘)
open import Categories.Morphism.Reasoning C
open import Categories.Object.Exponential C
open import Categories.Object.Product C
open import Categories.Object.Terminal C

import Categories.Category.Slice as S
import Categories.Category.Construction.Pullbacks as Pbs
import Categories.Object.Product.Construction as ×C

open Category C
open HomReasoning
Expand Down Expand Up @@ -96,3 +102,58 @@ module _ {A : Obj} where
; F-resp-≈ = λ f≈g → ⟨⟩-cong₂ refl (∘-resp-≈ˡ f≈g)
}

-- This can and probably should be restricted
-- e.g. we only need exponential objects with A as domain
-- I don't think we need all products but I don't have a clear idea of what products we do need
module _ (ccc : CartesianClosed) (pullback : ∀ {X} {Y} {Z} (h : X ⇒ Z) (i : Y ⇒ Z) → Pullback h i) where

open CartesianClosed ccc
open Cartesian cartesian
open Terminal terminal
open BinaryProducts products

-- Needs better name!
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it does. Ask on the category theory Zulip? It feels like it ought to have a name. (Does the 1lab have this yet?)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

1lab calls this functor exponentiable→product, and what we call Free they call constant-family. I can't see a counterpart to our Forgetful but I've asked in their Discord.

I would like to, following Polynomial Functors and Polynomial Monads (the paper I'm slowly working towards formalize here), call Forgetful Σ, Free Δ, and Coforgetful Π, but those names are even less indicative of their function than what we currently have. Aspects of Topoi uses the same names for Forgetful and Coforgetful, but calls Free ×.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, those single-letter names are even worse. The 1lab's names don't seem so bad?

I could try to summon @TOTBWF to see if he has opinions.

Copy link
Collaborator

@TOTBWF TOTBWF Jan 26, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have been SUMMONED ✨🧊 🧙✨

To get a good idea for names, it's good to understand exactly what is going on with slices. The intuition here is that a slice f : X -> I is how we can encode an I-indexed family of objects X_i without any sort of classifying object like Type. In places like Set, we can move between the two by taking the fibres of f and by forming the total space π₁ : Σ[ i ∈ I ] (P i) → I, but in a general category we cannot do this, so slices it is.

As such, base change pullback-functorial should really be thought of as a functor on slices C/B -> C/A for a morphism A -> B: from the perspective of families, this restricts a family f : X -> B to a new family P -> A along f potentially duplicating or deleting fibres. In other words, we take the fibre product: IE, the pullback. By composing with the projection out of the slice, we've essentially "forgotten" the indexing, and are just looking at the total space of the reindexed family.

From this perspective, Free isn't really the free slice, but rather the constant family on I: each fibre over is a copy of X. Furthermore, Forgetful doesn't really "forget" a slice: it returns the total space of a family by discarding the indexing.

Coforgetful is the trickiest: the bottom leg of the pullback is an obfuscation of the identity morphism, and the right leg is more or less postcomposition by the projection out of the family X -> I. Therefore, this pullback consists of sections of the family X -> I internalized as a exponential objects.

With all that background out of the way, here are my suggestions:

  • Make pullback-functorial a functor on slices, and rename it to Base-change or Reindex
  • Free becomes Constant-family
  • Forgteful becomes Total-space or Total
  • Coforgetful becomes Internal-sections or Sections

PS: this is some really great work!

Copy link
Member Author

@Taneb Taneb Jan 27, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like these names a lot! Thanks for the explanation.

While switching to them, I noticed that pullback-functorial (after @TOTBWF's suggestion to make it less forgetful) looks a lot like Categories.Functor.Slice.BaseChange.BaseChange*. I haven't quite been able to convince myself that they are the same thing, because there's a lot of redirection and it's a little confusing to get my head around, but if they are, I'd like to remove pullback-functorial entirely.

EDIT: I was able to write a NaturalIsomorphism between the two where almost everything was trivial (one use of universal-resp-≈ was necessary for commute), so I went ahead and deleted what was once pullback-functorial

Coforgetful : Functor (Slice A) C
Coforgetful = record
{ F₀ = p.P
; F₁ = λ f → p.universal _ (F₁-lemma f)
; identity = λ {X} → sym $ p.unique X (sym (!-unique _)) $ begin
p.p₂ X ∘ id ≈⟨ identityʳ ⟩
p.p₂ X ≈˘⟨ η-exp′ ⟩
λg (eval′ ∘ first (p.p₂ X)) ≈˘⟨ λ-cong (pullˡ identityˡ) ⟩
λg (id ∘ eval′ ∘ first (p.p₂ X)) ∎
; homomorphism = λ {S} {T} {U} {f} {g} → sym $ p.unique U (sym (!-unique _)) $ begin
p.p₂ U ∘ p.universal U (F₁-lemma g) ∘ p.universal T (F₁-lemma f) ≈⟨ pullˡ (p.p₂∘universal≈h₂ U) ⟩
λg (h g ∘ eval′ ∘ first (p.p₂ T)) ∘ p.universal T (F₁-lemma f) ≈˘⟨ pullˡ (subst ○ λ-cong assoc) ⟩
λg (h g ∘ eval′) ∘ p.p₂ T ∘ p.universal T (F₁-lemma f) ≈⟨ refl⟩∘⟨ p.p₂∘universal≈h₂ T ⟩
λg (h g ∘ eval′) ∘ λg (h f ∘ eval′ ∘ first (p.p₂ S)) ≈⟨ subst ⟩
λg ((h g ∘ eval′) ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S)))) ≈⟨ λ-cong (pullʳ β′) ⟩
λg (h g ∘ (h f ∘ eval′ ∘ first (p.p₂ S))) ≈⟨ λ-cong sym-assoc ⟩
λg ((h g ∘ h f) ∘ eval′ ∘ first (p.p₂ S)) ∎
; F-resp-≈ = λ f≈g → p.universal-resp-≈ _ refl (λ-cong (∘-resp-≈ˡ f≈g))
}
where
p : (X : SliceObj A) → Pullback {X = ⊤} {Z = A ^ A} {Y = Y X ^ A} (λg π₂) (λg (arr X ∘ eval′))
p X = pullback (λg π₂) (λg (arr X ∘ eval′))
module p X = Pullback (p X)

abstract
F₁-lemma : ∀ {S} {T} (f : Slice⇒ S T) → λg π₂ ∘ ! ≈ λg (arr T ∘ eval′) ∘ λg (h f ∘ eval′ ∘ first (p.p₂ S))
F₁-lemma {S} {T} f = λ-unique₂′ $ begin
eval′ ∘ first (λg π₂ ∘ !) ≈˘⟨ refl⟩∘⟨ first∘first ⟩
eval′ ∘ first (λg π₂) ∘ first ! ≈⟨ pullˡ β′ ⟩
π₂ ∘ first ! ≈⟨ π₂∘⁂ ○ identityˡ ⟩
π₂ ≈⟨ λ-inj lemma ⟩
arr S ∘ eval′ ∘ first (p.p₂ S) ≈˘⟨ pullˡ (△ f) ⟩
arr T ∘ h f ∘ eval′ ∘ first (p.p₂ S) ≈˘⟨ pullʳ β′ ⟩
(arr T ∘ eval′) ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S))) ≈˘⟨ pullˡ β′ ⟩
eval′ ∘ first (λg (arr T ∘ eval′)) ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S))) ≈⟨ refl⟩∘⟨ first∘first ⟩
eval′ ∘ first (λg (arr T ∘ eval′) ∘ λg (h f ∘ eval′ ∘ first (p.p₂ S))) ∎
where
lemma : λg π₂ ≈ λg (arr S ∘ eval′ ∘ first (p.p₂ S))
lemma = begin
λg π₂ ≈˘⟨ λ-cong (π₂∘⁂ ○ identityˡ) ⟩
λg (π₂ ∘ first (p.p₁ S)) ≈˘⟨ subst ⟩
λg π₂ ∘ p.p₁ S ≈⟨ p.commute S ⟩
λg (arr S ∘ eval′) ∘ p.p₂ S ≈⟨ subst ○ λ-cong assoc ⟩
λg (arr S ∘ eval′ ∘ first (p.p₂ S)) ∎