Hofmann-Streicher universes for graphs and globular types

[EgbertRijke]

This pull request is part of the formalization of higher category theory project with Ivan. Here we construct Hofmann-Streicher universes for:

• directed graphs
• reflexive directed graphs
• globular types
• reflexive globular types

Additionally, we add some computations for dependent Pi-types in those toposes, and some infrastructure is streamlined.

[EgbertRijke]

I have now proven the duality theorem for directed graphs (analogous to type duality), which is the toy-result of what I'm really after for globular types.

[fredrik-bakke]

I still find it very frustrating that pre-commit produces such a mess on commented code :(

Unfortunately, it is a choice between two evils, unless we want to start playing with making changes to the auto-formatter. Luckily your issue can be avoided by being mindful of how one comments code.

Your best course of action here is to look through the commit history for a point in time where the code wasn't jumbled. Alternatively, you could try something like text replacing -- with \n, but then you will have to manually indent things again after.

[fredrik-bakke]

Hiya! It looks like this PR is perhaps growing a bit outside the scope of the original goal. While I don't doubt the changes are relevant to one another, do you think it perhaps would be possible to split it up into some more manageable chunks for the eventual review?

[fredrik-bakke]

Oh, I see this PR is marked as ready for review. What's the status here?

[EgbertRijke]

It's ready for review. The contents of this PR are such that it can be merged to the library (modulo review comments, of course).

On the other hand, I haven't split it up yet, because if it is going to take a while for this to be reviewed then I prefer to keep working on it until I got all the HS-universes and all the corresponding duality theorems.

[fredrik-bakke]

I see, okay, so do you want a heads-up about when I think I'll be able to review?

[EgbertRijke]

Sure, or alternatively perhaps you can review the graph theory here in this PR and then I can separate it out into a separate PR when I resolved your comments.

[fredrik-bakke]

okay, sounds good

[EgbertRijke]

One thing I'm still debating on with myself is whether I should use the terminology "displayed" or "dependent".

Displayed is such a weird word to use in this context, but on the other hand it is the standard for some people.

[fredrik-bakke]

I used the word "displayed" when I defined reflexive graphs because I had my eye toward wild categories, but I agree the landscape is pretty different for graphs. At the end of the day it's your domain though, so it's up to you what you want to call it.

[fredrik-bakke]

Amazing effort!

This review regards modules in foundation-core, foundation, and graph-theory.

[EgbertRijke]

Amazing effort!

This review regards modules in foundation-core, foundation, and graph-theory.

Thanks for the swift review Fredrik!

[EgbertRijke]

That was a very helpful review, Fredrik! I have also made the corresponding changes for globular types, so that you don't have to make the same remarks again.

Thanks so much!

[fredrik-bakke]

I'm glad! 😄