2-Terminal Object and 2-Product

[maxsnew]

A couple of simple examples of 2-limits to get us started discussing design decisions.

I have been playing with the 2-Yoneda lemma to try to figure out what the correct version of these is. I think I have figured out a simple/systematic presentation but it will be nice to prove these equivalent to a definition by representable 2-functors at some point.

The terminal object definition can probably be simplified further but I wanted to show the general pattern. For these two examples you basically need a 1-cell and 2-cell version of the "introduction form" and correspondingly need 1-cell beta/eta isomorphisms, and then 2-cell beta/eta equations that only make sense "up to" 1-cell beta/eta isomorphisms.

It would simplify the 2-cell beta/eta (and I think based on sketching comma objects generally useful) to have a notation for the situation where

i : A ≅ A'
j : B ≅ B'
f : A → B
g : A' → B'

and we want to say f is equal to g along this isomorphism.

Along i j [ f ≈ g ]

maybe? It looks like this is a morphism in an arrow category, so maybe there's something already in the library for this?

For instance in this notation, η₂ would become

η₂ : ∀ {Γ}{p p'}(ϕ : hom Γ A×B [ p , p' ])
   → Along (η₁ _) (η₁ _) [ ϕ ≈ ⟨ (πa ▷ ϕ) , (πb ▷ ϕ) ⟩₂ ]

This is in the spirit of viewing isomorphism as equality. In the strict version, the 1-cell beta/eta are equalities.

Aside: I think the HoTT people have a name for this. "path-over" or something like that, but I couldn't find anything with some quick googling.

Any advice on which arguments should be implicit would also be appreciated.

[JacquesCarette]

I definitely like Along i j [ f ≈ g ]. The construction of the Arrow category is in the library, but not much else. It uses CommutativeSquare for the definition of morphisms. That is useful because https://agda.github.io/agda-categories/Categories.Morphism.Reasoning.Iso.html has a variety of combinators for reasoning on squares. Because the situation here is special (i and j are known isos while f and g are just morphisms), I think it makes sense to introduce something special for those.

Interestingly, the exact same thing comes up in the context of defining double categories.

I think I'd like to experiment with Along being as you have it above, i.e. with 4 explicit arguments.

[maxsnew]

The way I'm thinking of Along is that it's a 2-cell in a double category of morphisms and isomorphisms (framed/equipment as well since isos induce an "adjoint" pair of functions). I have a draft of 2-pullbacks that is getting complicated enough that it looks like it will be useful to implement some of the double cat operations.

[JacquesCarette]

It seems that many are converging on double category as a useful next step -- see #346 for example. Getting consensus on how to go about this makes sense. Having some discussion on both semantics and syntax (at that PR) would make sense.

[JacquesCarette]

And I see that you already have - great!