I've been chatting with folks on Mastodon about this but the perspective there is markedly Agda-focused, so I thought I'd ask here for some broader opinions.
What tools/libraries are there for reasoning about Categories with Families and Language Semantics in a Proof Assistant?
I'm particularly looking for:
- Tools that will let me reason in the language of CwFs without committing to a particular category
- Tools that will help me automatically rewrite goals using the category and CwF laws without much boilerplate. Many of the CwF equations have a "direction" and can safely be turned into rewrite rules without risking non-termination.
In Agda, (1) and (2) are at odds with each other: there's the REWRITING option, but it doesn't support rewriting in terms of fields of a record. So unless morphism composition and comprehension are given concrete definitions, it can't rewrite.
Are there frameworks in Coq or Lean for this? I know there are tactics there to rewrite by a particular equality, but I have no idea how easy it is to automatically rewrite by all of the CwF laws.