Internal categories

Stream: maths

[Zach Murray]

Hello. I'm an undergrad and inexperienced Lean user. I'm trying to implement internal categories with Dorette Pronk and Martin Szyld at Dalhousie University. I'm looking for opinions on how this should be done, and I've run into an issue.

First, here's what we've got. We decided to implement internal categories without requiring the ambient category to have all of its pullbacks. It only needs those relevant to the definition of an internal category. Moreover, we thought it a good idea to mirror the implementation of categories by founding internal categories on internal quivers. Thus, we have the following (please see nLab on internal categories for notation, and note that C₀ and C₁ have become Obj and Arr, respectively):

import category_theory.category.basic
import category_theory.limits.shapes
open category_theory
open category_theory.limits
noncomputable theory

universes v u

class internal_quiver (𝔸 : Type u) [category.{v} 𝔸] :=
(Obj Arr : 𝔸)
(s t : Arr ⟶ Obj)

class internal_category_struct (𝔸 : Type u) [category.{v} 𝔸]
extends internal_quiver 𝔸 :=
(e : Obj ⟶ Arr)
(has_comp : has_pullback t s)          -- Arr × Arr
(c : pullback t s ⟶ Arr)
(has_assocₗ : has_pullback (c ≫ t) s)   -- (Arr × Arr) × Arr
(has_assocᵣ : has_pullback t (c ≫ s))  -- Arr × (Arr × Arr)
(has_idₗ : has_pullback (𝟙 Obj) s)       -- Obj × Arr
(has_idᵣ : has_pullback t (𝟙 Obj))      -- Arr × Obj

Now, a problem. Mirroring the prefunctor and functor definitions, I've worked on an internal_prefunctor and internal_functor:

structure internal_prefunctor {𝔸 : Type u} [category.{v} 𝔸] (𝔻 𝔼 : internal_quiver 𝔸) :=
(obj : 𝔻.Obj ⟶ 𝔼.Obj)
(arr : 𝔻.Arr ⟶ 𝔼.Arr)

structure internal_functor {𝔸 : Type u} [category.{v} 𝔸] (𝔻 𝔼 : internal_category_struct 𝔸)
extends internal_prefunctor 𝔻 𝔼 :=
(resp_source : sorry)
(resp_target : sorry)
(resp_id : sorry)
(resp_comp : sorry)

For some reason, internal_functor gives me this error:

type mismatch at application
  internal_prefunctor 𝔻
term
  𝔻
has type
  internal_category_struct 𝔸 : Type (max u v)
but is expected to have type
  internal_quiver ?m_1 : Type (max ? ?)

Changing 𝔻 and 𝔼 to have type internal_quiver 𝔸 fixes this error.

I don't understand why this error occurs. Is it not the case that every internal_category_struct 𝔸 is an internal_quiver 𝔸, even though the former extends the latter? Why does the seemingly same strategy work for defining functor but not internal_functor? I can only imagine there's something about typeclasses I'm missing.

If anyone has any suggestions on things to consider when implementing internal categories, or how to fix this problem, I'd appreciate them!

[Adam Topaz]

the issue is that you've defined internal quivers as classes, whereas they should just be plain strucrtures (similarly for internal_category_struct)

[Adam Topaz]

A similar construction we have in mathlib that you can try to mimic is docs#Mon_

[Adam Topaz]

and docs#Mon_.hom

[Andrew Yang]

Also, to get the underlying internal_quiver 𝔸 from a 𝔻 : internal_category_struct 𝔸, you should write 𝔻.to_internal_quiver.

[Adam Topaz]

import category_theory.category.basic
import category_theory.limits.shapes
open category_theory
open category_theory.limits
noncomputable theory

universes v u

structure internal_quiver (𝔸 : Type u) [category.{v} 𝔸] :=
(Obj Arr : 𝔸)
(s t : Arr ⟶ Obj)

structure internal_category_struct (𝔸 : Type u) [category.{v} 𝔸]
extends internal_quiver 𝔸 :=
(e : Obj ⟶ Arr)
(has_comp : has_pullback t s)          -- Arr × Arr
(c : pullback t s ⟶ Arr)
(has_assocₗ : has_pullback (c ≫ t) s)   -- (Arr × Arr) × Arr
(has_assocᵣ : has_pullback t (c ≫ s))  -- Arr × (Arr × Arr)
(has_idₗ : has_pullback (𝟙 Obj) s)       -- Obj × Arr
(has_idᵣ : has_pullback t (𝟙 Obj))      -- Arr × Obj

structure internal_prefunctor {𝔸 : Type u} [category.{v} 𝔸] (𝔻 𝔼 : internal_quiver 𝔸) :=
(obj : 𝔻.Obj ⟶ 𝔼.Obj)
(arr : 𝔻.Arr ⟶ 𝔼.Arr)

structure internal_functor {𝔸 : Type u} [category.{v} 𝔸] (𝔻 𝔼 : internal_category_struct 𝔸)
extends internal_prefunctor 𝔻.to_internal_quiver 𝔼.to_internal_quiver :=
(resp_source : sorry)
(resp_target : sorry)
(resp_id : sorry)
(resp_comp : sorry)

[Zach Murray]

Thank you both.

Another problem I'm having concerns reusing pullback t s. For example, adding the following code

section

variables {𝔸 : Type u} [category.{v} 𝔸] [𝔻 : internal_category_struct 𝔸]

example : 𝔸 := pullback 𝔻.t 𝔻.s

end

gives me the error

failed to synthesize type class instance for
𝔸 : Type u,
_inst_1 : category 𝔸,
𝔻 : internal_category_struct 𝔸
⊢ has_pullback 𝔻.to_internal_quiver.t 𝔻.to_internal_quiver.s

Why is Lean not using 𝔻.has_comp to resolve this? (Is it the result of poor style in my definition?)

[Adam Topaz]

You need to declare this as an instance.

[Zach Murray]

I was going to say I already tried that but I just realized I was declaring my instance as inhabited (has_pullback instead of just has_pullback... :sweat_smile: It works now, thanks.

[Adam Topaz]

Out of curiosity, what do you plan to do with these internal categories?

[Zach Murray]

We'd like to implement something on double categories and fibrations. I don't know the details on the full extent of what we're making since I'm learning this material from Dorette and Martin (I've linked them both, perhaps they'll comment).

We tried implementing double categories using the typical "horizontal arrows, vertical arrows, etc" definition and played around with some modifications, but it got ugly and complicated fast (perhaps because I'm inexperienced with Lean). Also, it seems internal categories will be needed anyway, so I'm starting with them instead.

[Martin Szyld]

Hi there, thanks @Adam Topaz and @Andrew Yang for your help here! To satisfy Adam's curiosity a bit, with Dorette and others we've been working the last couple of years on a Grothendieck construction for double categories [1] and on double fibrations (as internal categories in Fib, see [2] for details). Now, the Grothendieck construction of [1] works for a type of indexing functor taking values in double categories and we have shown a correspondence

{these indexing functors} <-> {a type of split fibration between double categories, different to that of [2]}.

But, an issue is that the non-split fibration/indexing pseudofunctors case doesn't seem to "canonnically" work like it did in [2] (or at least we're not clever enough to realize how). So in addition to implementing internal categories and showing how double categories are internal categories in Cat in the Lean context, we were also hoping that the type theory formalism, since in a sense it "forces you to be pseudo" (*), may help us down the road to understand how to correctly "pseudify" the construction in [1].
[1] See Dorette's talk at https://topos.site/topos-colloquium/2021/, this will hopefully be in arXiv soon.
[2] https://arxiv.org/abs/2205.15240
(*) See also https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/double.20categories