Documentation

Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Finiteness instances on multi-spans #

instance CategoryTheory.Limits.WalkingMulticospan.instFintype {J : MulticospanShape} [Fintype J.L] [Fintype J.R] :

Fintype (WalkingMulticospan J)

Equations

CategoryTheory.Limits.WalkingMulticospan.instFintype = Fintype.ofEquiv (J.L ⊕ J.R) (CategoryTheory.Limits.WalkingMulticospan.proxyTypeEquiv J)

instance CategoryTheory.Limits.WalkingMulticospan.instFinCategoryOfLOfDecidableEqR {J : MulticospanShape} [Fintype J.L] [Fintype J.R] [DecidableEq J.L] [DecidableEq J.R] :

FinCategory (WalkingMulticospan J)

Equations

One or more equations did not get rendered due to their size.

instance CategoryTheory.Limits.WalkingMultispan.instFintype {J : MultispanShape} [Fintype J.L] [Fintype J.R] :

Fintype (WalkingMultispan J)

Equations

CategoryTheory.Limits.WalkingMultispan.instFintype = Fintype.ofEquiv (J.L ⊕ J.R) (CategoryTheory.Limits.WalkingMultispan.proxyTypeEquiv J)

instance CategoryTheory.Limits.WalkingMultispan.instFinCategoryOfLOfDecidableEqR {J : MultispanShape} [Fintype J.L] [Fintype J.R] [DecidableEq J.L] [DecidableEq J.R] :

FinCategory (WalkingMultispan J)

Equations

One or more equations did not get rendered due to their size.