Finiteness instances on multi-spans

@[instance_reducible]

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_reducible]

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_reducible]

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_reducible]

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.