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]

please don't use instance arguments. I'm fine with opaque and unfolding, but not these. Things are slow enough as it is, let's not make it worse.

[4e554c4c]

I'm not sure if the instances are making things slow here.

They make a lot of definitions nicer. For example, in Properties.agda there is the type

end-η-resp-∘ : (α : NaturalTransformation F G) (β : NaturalTransformation G H)
  {{ef : ∫ F}} {{eg : ∫ G}} {{eh : ∫ H}} →
  end-η (β ∘ᵥ α) ≈ end-η β ∘ end-η α

Stating each end here for end-η complicates the definition a lot, and I don't think that it makes things nicer. Using implicit arguments isn't possible either, since the only portion of the end that is solved uniquely is the apex.

The instance arguments work less well for parameterized ends, which is probably why you noticed it in this file and not the other.

[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.