End calculus

[4e554c4c]

This PR is a collection of theorems and refactorings that were developed during my master's thesis.

This includes

• Initial objects
  • are colimits
• Strict initial objects
  • Initial objects in a Cartesian category are strict
• The category of twisted arrows
  • has a forgetful functor
  • Twist (F ∘ J) is iso to F ∘ Twist J
• End calculus
  • Ends are preserved by continuous functors
  • The setoid of natural transformations is an end (given size constraints)
  • Parameterized ends (EndF)
  • are ends
  • are preserved by continuous functors
  • The end of a parameterized end is an end in the product category (Fubini)

Many definitions could be simplified if #419 is resolved.

Considerations

--lossy-unification is currently necessary for Categories.Diagram.End.Fubini. I was hoping that refactoring EndF to use an opaque end-η could fix this, but it does not.

[JacquesCarette]

Re: --lossy-unification. Is this because otherwise it takes way too long? At this this is cause by Agda reconstructing some implicit arguments "the hard way" even though, to use, they are obvious. I've been able to cut some typechecking time down a lot by supplying just the right implicits. One big clue is if you ask Agda for the type of various things and stuff is eta-expanded. This definitely happens in the presence of things that compute, such as ×ᶜ.

[4e554c4c]

Re: --lossy-unification. Is this because otherwise it takes way too long?

Yes, but I don't think this is all about reconstructing implicit arguments. It is also comparing terms. I reference #419 because one of the things that needs to be compared often is apices of ends

[4e554c4c]

I can't resolve all of the <greek letter>.dinatural.α blah noise in the fubini proofs. I can move give names to some of them in where clauses if I define the ends using copatterns (as is probably more reasonable anyway). Really the main solution to this would be to resolve agda/agda#7156 and allow for "applying" wedges (or ends) to an object to get the appropriate map.

[4e554c4c]

@JacquesCarette whenever you have the time, I would appreciate another look. I haven't changed everything that you suggested, but I left comments wherever I did not.

[Taneb]

...would it be possible to split this into several other PRs? It's very big and scary to look at for me (this isn't a requirement but I'd appreciate it)

[4e554c4c]

...would it be possible to split this into several other PRs? It's very big and scary to look at for me (this isn't a requirement but I'd appreciate it)

I can't split off too much, since github PRs can't depend on eachother. I split off some misc changes into #423 and #424 (will probably add to both of these later)

[JacquesCarette]

Sorry for the slowness - was on vacation all last week.