Representable Presheaves, Free Category, Functor and Associated solvers

[maxsnew]

This PR defines representable presheaves a formalization of the notion of a universal property. This includes

1. Isomorphisms between a representable presheaf, a terminal objects in the category of elements and an elementary record description of a universal morphism of a presheaf. See chapter 2 of Riehl's Category Theory in Context for a reference.
2. The Yoneda lemma for contravariant functors as well as variants with increased universe polymorphism
3. Some useful functors: Lifting the homs of a category to a higher universe, lifting the category of sets to a higher universe and lambda and application functors (i.e., the exponential structure in Cat, but without proving the universal property).
4. A definition of a morphism of presheaves between different categories and a definition of when such a morphism preserves representability of the presheaf. This notion should encompass notions such as preservation of limits.

[maxsnew]

I'm converting this to draft as I have developed a lot more code along the same lines that should be useful to bundle together.

[maxsnew]

Updated the description above. Ready for review now

[felixwellen]

I'll start reviewing...

[felixwellen]

Thanks for all this stuff, this looks really useful!

[felixwellen]

We don't have a strict 80-line policy, but we try to avoid very long lines. So use your own judgement, but I think in the following files, some lines are too long:

Cubical/Categories/Constructions/Free/Category/Base.agda
Cubical/Categories/Constructions/Free/Functor.agda
Cubical/Categories/Yoneda.agda

[felixwellen]

Cubical/Tactics/Reflection.agda

Do you think I could also use that to refactor the solver for CommRings/Monoids/...?

[maxsnew]

Cubical/Tactics/Reflection.agda

Do you think I could also use that to refactor the solver for CommRings/Monoids/...?

I think so. Even better if it were in agda-base as it's modified 1lab code already.

[maxsnew]

I'm working on the column overflows (sorry). But I did push one actual (minor) change to the Free category implementation that I had already needed downstream.

[felixwellen]

Good - thanks!

[maxsnew]

Ok column overflows should be good now.

[felixwellen]

In general, the PR looks good and contains a lot of very useful stuff!
One important thing is, that we document what was taken from the 1lab (they use a different license and we should credit them properly in any case).
Otherwise, I mostly commented on things on the level of style questions and asked for more documentation.

[felixwellen]

Is there more code from the 1lab? I think it should be marked because it has a GPL like license

[maxsnew]

Just this file is from the 1lab. I can add a link to the file but let me know if there's a specific format I should follow.

[felixwellen]

Yes, a link is good. And maybe "1Lab (AGPL 3.0)" to make it clear, they use a different license. I'm afraid I don't actually know how to do things like this properly.

[jpoiret]

It would probably be good to follow the SPDX format for this, as it is quite standard now. You can have a look at https://spdx.dev/ids/ for how to do so!

[jpoiret]

IANAL but looking at this closer, GPL is more restrictive than MIT and you can't license GPL code under MIT. I think cubical would have to also include the AGPL license, and be distributed under a dual license.

[felixwellen]

This is now tracked as #1018. The solution there includes adding spdx identifiers, so please do that where necessary.

[plt-amy]

I'm a tad too tired to think about doing a large-scale re-license this week, but I have no issue with treating the 1Lab.Reflection tree as BSD-3-Clause; the other contributors to those files are @ncfavier and @TOTBWF.

[TOTBWF]

I have absolutely no issues with having this file be BSD-3 either

[ncfavier]

Same (not that I see any code I've written in this PR...)

[felixwellen]

Thanks everyone for resolving this!
So we use "BSD-3-Clause" for this file.

[jpoiret]

I've already mentioned this to Felix and Max, but I think the definition of isUniversal (vertex , el) should be simplified to the equivalent isEquiv (λ (f : C [ A , vertex ]) → P ⟪ f ⟫ el). This lets us avoid adding a new specialized record type, and also re-use most Equiv-related combinators. Also, modifying the definition of the category of elements to have the symmetric equality P ⟪ f ⟫ u ≡ v to align more with the definition of a fiber makes isUniversal el be simply the currification of isInitial el! I think this would save quite a lot of work writing some obvious definitions.

I have a simple PoC with these new definitions, but it's not fully formed yet (and I don't have anything regarding hetereogeneous Yoneda).

[maxsnew]

Ok I've addressed the last changes with my most recent commits:

1. Add AGPL >=3.0 license to the file adapted from 1lab
2. fix import order
3. Update to work with the recent changes to Data.Equality/Cubical.Foundations.Id.
4. Refactor UniversalElement to be defined in terms of isEquiv. I also changed the names as @felixwellen suggested an put an extended comment in Presheaf.Representable to explain what the file does in more detail.

For the last point, the equivalence between terminal element and universal element would be simpler if the morphisms in the category of elements were defined differently as @jpoiret mentioned, but a non-trivial amount of code would have to be rewritten around the new definition and I didn't want to increase the scope of this PR any more so I didn't do that.

[jpoiret]

So, I think the last missing bit is marking the 1lab file as BSD-3 instead of AGPLv3. Could you also remove the commented code in Cubical.Categories.Presheaf.Representable? Regarding the Elements change, I have a commit doing it, so I can send a separate PR after yours, it shouldn't be blocking :)

[maxsnew]

Fixed the license and removed the accidentally included comments in the latest force push.

[felixwellen]

Should be good to merge now.