Commit 2024-11-11 14:39 c0085aa0

View on Github →

feat: improve defeq in skeletonEquivalence (#18746)

  • Change the inverse in skeletonEquivalence to be defeq to Quotient.mk; it's previously obtained from IsEquivalence.asEquivalence by arbitrary choice.
  • Make tensorIso notation scoped (tensorObj and tensorHom are already scoped).
  • Add a CoeSort instance for Sksleton.
  • Add a few API lemmas.

Estimated changes