Strict symmetrizations of binary relations

[fredrik-bakke]

Defines the strict symmetrization of a binary relation, and proves some basic properties of these. Among these,

• the construction has a unit R -> S(R) if R is reflexive
• the construction has a counit S(R) -> R if R has extensions.

This construction is useful in defining certain coherences for wild categories.

[fredrik-bakke]

Just for clarity, I do want to write some good explainers for the files I'm developing here before this PR is merged, but my first priority is to find the right definitions.

[fredrik-bakke]

I'm adding a definition of "wide displayed large reflexive graphs", but I do not like the terminology usage "wide" here. I think "wide" should mean "equipped with a section of the family of vertices", but currently I take it to mean "contractible family of vertices". Would love naming suggestions. Basically, what I use it as is a displayed reflexive graph that only adds structure on the edges and keeps the same vertices.

[fredrik-bakke]

If we want to formalize this nice result about wild categories due to Jon Sterling and Mike Shulman for 1-coherent wild categories, we better require the wild identity relation to have an action on wild identifications.

EDIT: On second thought, it may be more fitting to prove this result for extensional wild precategories

[fredrik-bakke]

I'm marking this one as ready for review.

[EgbertRijke]

Nice pull request! I just had a few minor comments.

[fredrik-bakke]

By the way. We have three conflicting notions of "discreteness" in the library:

1. A discrete type is a type with decidable equality.
2. A discrete relation is a relation that is equivalent to the identity relation.
3. A discrete precategory is the precategory defined by the identity types of a set.

If we change a discrete precategory to be the precategory defined by the identity types of a 1-type, then item 2 and 3 would agree, but that still leaves item 1 as a distinct notion of discreteness.

[fredrik-bakke]

I've resolved your comments now

[fredrik-bakke]

I improved a bit on how the concepts of the PR are organized by splitting outer-2-horn-filler-conditions-binary-relations into binary-relations-with-extensions and binary-relations-with-lifts, and I also added a remark about the dual strict symmetrization, although I did not create a separate file for it.

[fredrik-bakke]

I'm merging this PR, any lingering questions can be reconsidered again later.