Post #2636099

@mc@mathstodon.xyz @JacquesC2@types.pl I wouldn't take any notes you find in there as particularly definitive, they're just some thoughts that I put down at some point and likely outdated. Our approach is to encode all universal properties as representable functors (and displayed versions of this). This is motivated by wanting to have one single definition of universal property out of which concrete instances would be special cases so that we could get for free many of the reasoning principles you want out of a universal property. I don't think this is particularly radical approach but compared to textbooks we try very hard to adhere to the DRY principle and formulate things in as much generality as possible. So for instance we prefer to avoid defining functors by hand when they have a universal property (https://github.com/um-catlab/cubical-categorical-logic/blob/main/Cubical/Categories/FunctorComprehension/Base.agda) which gets you things like functoriality of products, exponentials "for free". We also use displayed categories heavily because it's just much more natural way to handle indexing in dependent type theory. We have started integrating them further into the core of the library. For example, I'm sure no sane textbook defines the binary product of categories as a total category of a weakened category (https://github.com/agda/cubical/blob/master/Cubical/Categories/Instances/BinProduct.agda#L23). We also have some fun defining the universal property of free constructions to produce a global section of a displayed category and then derive the more typical universal property from that (https://github.com/agda/cubical/blob/7a4fbe151cc7185b5b782f8257976753317ed176/Cubical/Categories/Instances/Free/Category/Quiver.agda#L122) There's also some more strange stuff that is pretty experimental in there. We define bifunctors in an unusual that helps us to produce nicer compositional definitions of things like the exponential. There's a whole sub-module of large and locally small categories that we haven't adopted yet but helps us handle some very universe-polymorphic stuff better. And there's probably like 3 different definitions of presheaf and 5 different definitions of natural transformation of (displayed) presheaves that all have weird tradeoffs that we haven't totally settled yet. (btw what's the difference between representable functors and universal arrows? Aren't they the same thing?)