Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: topos theory

Topic: Internal presheaves as coalgebras

Bhavik Mehta (Jun 09 2020 at 20:03):

In Section 3 here: https://ncatlab.org/toddtrimble/published/Three+topos+theorems+in+one#eq:ttt2, he describes a functor and says it's a comonad, but I'm struggling to see why it's a comonad (or even what the comonad structure should be) - am I missing something obvious?

Dan Doel (Jun 09 2020 at 20:14):

I think this is the category analogue of $M → -$ where $M$ is a monoid. You extact by applying to the monoid unit, and duplicate by multiplying in the monoid.

Dan Doel (Jun 09 2020 at 20:18):

And the unit/associativity axioms for the comonad follow from unit/associativity for the monoid. And similarly when you replace the monoid with a category.

Dan Doel (Jun 09 2020 at 21:43):

I'm not sure what your background is, but here is an analogous construction in Agda, to give some idea of what each thing does.

W : Type₁ → Type₁
W Y = Σ[ U ∈ Type₀ ] ((T : Type₀) → (T → U) → Y)

ε : ∀{Y} → W Y → Y
ε (U , e) = e U (idfun U)

δ : ∀{Y} → W Y → W (W Y)
δ (U , e) = (U , λ T f → (T , λ S g → e S (f ∘ g)))

Bhavik Mehta (Jun 09 2020 at 21:58):

I can see how to do this for monoids but the analogy is confusing me at the moment

Bhavik Mehta (Jun 09 2020 at 21:58):

I'm trying right now to show this is a comonad in Lean

Bhavik Mehta (Jun 09 2020 at 22:28):

I think what I don't see is why your W is the same as the functor described there

Dan Doel (Jun 09 2020 at 22:33):

Well, it's exactly the formula that page uses after the initial description, specialized to C = Type₀

Dan Doel (Jun 09 2020 at 22:35):

That is a particularly easy specialization, though. Depending on how you're modelling everything in Lean, it might be considerably less convenient to write things down.

Bhavik Mehta (Jun 09 2020 at 22:35):

Dan Doel said:

Well, it's exactly the formula that page uses after the initial description, specialized to C = Type₀

Oh right, I can see that

Bhavik Mehta (Jun 09 2020 at 22:37):

Dan Doel said:

That is a particularly easy specialization, though. Depending on how you're modelling everything in Lean, it might be considerably less convenient to write things down.

Yeah I think this is the scenario I'm in. I'm modelling it virtually as described there, I've got an internal category in a LCCC, and the functor is defined exactly as written there

Bhavik Mehta (Jun 09 2020 at 22:37):

That is - in pretty much the same level of generality

Dan Doel (Jun 09 2020 at 22:45):

Well, a slightly more general version is this:

module _
  (O : Type₀)
  ([_,_] : O → O → Type₀)
  (i : ∀{a} → [ a , a ])
  (_∘_ : ∀{a b c} → [ b , c ] → [ a , b ] → [ a , c ])
  where
  W : Type₀ → Type₀
  W Y = Σ[ u ∈ O ] ((t : O) → [ t , u ] → Y)

  ε : W Y → Y
  ε (u , e) = e u i

  δ : W Y → W (W Y)
  δ (u , e) = (u , λ t f → (t , λ s g → e s (f ∘ g)))

Dan Doel (Jun 09 2020 at 22:45):

Omitting the associativity stuff which is no longer trivial.

Dan Doel (Jun 09 2020 at 22:47):

Now, that type theoretic stuff can in principle be translated to any LCCC, and you'll end up with something about the span definition. But maybe that's not satisfying. :)

Bhavik Mehta (Jun 09 2020 at 22:48):

"In principle" :)

Bhavik Mehta (Jun 09 2020 at 22:48):

Thanks though, this definitely gives me some things to try!

Dan Doel (Jun 09 2020 at 22:55):

It's probably not so hard to work through in this case, or at least use it as a guide of what to do from the 'external' perspective.

Bhavik Mehta (Jun 09 2020 at 22:57):

Right now part of the problem is that I haven't made it at all pleasant to work with the Pi functor so even doing an application is awkward... But these are technical issues now, thanks!

Bhavik Mehta (Jun 19 2020 at 02:33):

Another question on the same topic - he describes a coalgebra for that comonad, and says that we get a contravariant action of the (internal) category on the set Y - this much is fine, but I don't see why p(y^f) should be x', using the notation there. In other words I don't see why the action respects fibers properly

Bhavik Mehta (Jun 19 2020 at 02:34):

(In the E=Set case, for now at least)

Dan Doel (Jun 19 2020 at 03:06):

I think that is ensured by coherence with splitting. Note that in my δ, t occurs as the value of $p$ for the inner part, where t is the domain of f. Two applications of a coalgebra must agree with one application that is split. In order for that to happen, $p(y^f)$ must be $x'$, or there is no hope for $(y^f)^g = y^{(f \circ g)}$ to work out.

Bhavik Mehta (Jun 19 2020 at 03:08):

By coherence with splitting do you mean the coassociative law for the coalgebra?

Bhavik Mehta (Jun 19 2020 at 03:08):

I certainly appreciate why it should be true, just not entirely sure what the actual argument is

Dan Doel (Jun 19 2020 at 03:09):

Well, I was going to call it that, but it's not actually associativity, right?

Bhavik Mehta (Jun 19 2020 at 03:10):

Alright sure, just making sure I'm following correctly!

Dan Doel (Jun 19 2020 at 03:10):

Anyhow, it's the $δ\circφ = Tφ \circ φ$ sort of rule. Whatever that's called (I'm blanking on the name).

Dan Doel (Jun 19 2020 at 03:13):

If you unpack that by projecting/applying each side, I think you'll arrive at a requirement for $p(y^f) = x'$ along the way.

Bhavik Mehta (Jun 19 2020 at 03:14):

That makes sense, thanks!