Extensionality for functors commuting with shifts #
Mathlib's Functor.CommShift is data: two structures on the same functor need
not agree by proof irrelevance. They do agree when their family of
commutation isomorphisms agrees, because the zero and addition fields are
propositions. This is the data-level comparison used when a shift structure
is assembled through two categorical presentations.
theorem
CategoryTheory.Functor.CommShift.ext
{C : Type u}
{D : Type u'}
[Category.{v, u} C]
[Category.{v', u'} D]
{A : Type w}
[AddMonoid A]
[HasShift C A]
[HasShift D A]
{F : Functor C D}
(h h' : F.CommShift A)
(w : ∀ (n : A), commShiftIso F n = commShiftIso F n)
:
Two CommShift structures on one functor agree when all their
commutation isomorphisms agree.
theorem
CategoryTheory.Functor.CommShift.ext_iff
{C : Type u}
{D : Type u'}
[Category.{v, u} C]
[Category.{v', u'} D]
{A : Type w}
[AddMonoid A]
[HasShift C A]
[HasShift D A]
{F : Functor C D}
{h h' : F.CommShift A}
: