Usability of Pullback.agda

[sergey-goncharov]

I am struggling with Categories.Diagram.Pullback, trying to use it for my project. I've added some fixes, which helped, but the whole implementation philosophy seems to contradict my use case (any use case?). So, I am seeking guidance.

I believe, mathematically, the central concept is IsPullback, not Pullback. This is because we usually have an already-commuting diagram as input, and we only need to prove that it is a pullback. So, the functional transformation we need is:

• commuting diagram -> pullback property

not:

• cospan -> commuting diagram, which is also a pullback

Sometimes, the difference is shallow. But it gets deep quickly. As an example, I tried to use unglue, which basically subtracts a pullback from another pullback:

unglue : (p : Pullback f g) → Pullback (f ∘ h) g → Pullback h (Pullback.p₁ p)

The problematic clause is this

p₂ = p.universal (sym-assoc ○ q.commute)

Because the pullback span is defined up to isomorphism, Pullback (f ∘ h) g only ensures that a suitable span exists, and it is guaranteed not to match any span that I am highly likely to already have at hand. Thus, to finish the construction of Pullback h (Pullback.p₁ p), we need the universal property of the first pullback, which returns anything but the morphism I probably already have, because I probably already have a concrete factorization of the large pullback's span through the small pullback's span. The resulting pullback Pullback h (Pullback.p₁ p) is then different from my candidate pullback, and that difference is not shallow. It seems that it is easier to prove that the resulting pullback is so from scratch than by using unglue.

Incidentally, unglue is often not general enough, so I added a stronger version, called unglue' , following the IsPullback paradigm. It works perfectly, but still, sometimes, the generality of unglue is enough, so I would prefer to have an IsPullback version of it. So, how should I call it? unglue''? To me, the right thing would be to have unglue and unglue' in the IsPullback form, and whatever for the current unglue.

This is just an example. This whole file is written in Pullback-centric way. Instead of swap : Pullback f g → Pullback g f I would have preferred swap : IsPullback f g h u → IsPullback g f u h, etc. Perhaps, this is not specific to pullbacks but to other structures across the library. So, I am wondering if there is a solid design decision behind this approach, which I am not grasping, being narrowly focused on concrete categorical arguments I am trying to formalize.

Any opinions? Should I just keep adding things that I am missing, and should I stick to any specific naming conventions then?

[JacquesCarette]

Sorry for the super slow reply - you sent this at a time I was very busy, and then I was on vacation for 2 weeks. Now is better, and I'm going through my agda-categories backlog.

This goes way beyond Pullback, even beyond category theory: this is really about the usability of various ways of bundling (or unbundling) information, which applies to much of algebra, where category theory is 1-algebra (and classical algebra is 0-algebra).

The whole of agda-categories is written in a "classical textbook" (roughly speaking, Maclane) style, modified by past experiences of doing CT with dependent types, and some learned lessons that are more recent. Thus what you witness: centered on Pullback instead of IsPullback, because that's how the 'mathematical vernacular' is written. Quite likely, a very close inspection of a lot of actual category theory would reveal that in actual use, there's a lot of fluidity between the two. They are equivalent, after all. But that 'equivalence' is invisible on paper, and introduces a lot of friction in practice.

The current experiment is to create something like Pullback/Unbundled for things that work with IsPullback. In that file, the names can even be identical to others (i.e. swap and unglue), since one tends to use a single style. If you want to use both, you still can, just with qualification.

Does that help?