Documentation

Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Finiteness instances on multi-spans #

source
instance CategoryTheory.Limits.WalkingMulticospan.instFintype {J : MulticospanShape} [Fintype J.L] [Fintype J.R] :
Fintype (WalkingMulticospan J)
Equations
    source
    instance CategoryTheory.Limits.WalkingMulticospan.instFinCategoryOfLOfDecidableEqR {J : MulticospanShape} [Fintype J.L] [Fintype J.R] [DecidableEq J.L] [DecidableEq J.R] :
    FinCategory (WalkingMulticospan J)
    Equations
      source
      instance CategoryTheory.Limits.WalkingMultispan.instFintype {J : MultispanShape} [Fintype J.L] [Fintype J.R] :
      Fintype (WalkingMultispan J)
      Equations
        source
        instance CategoryTheory.Limits.WalkingMultispan.instFinCategoryOfLOfDecidableEqR {J : MultispanShape} [Fintype J.L] [Fintype J.R] [DecidableEq J.L] [DecidableEq J.R] :
        FinCategory (WalkingMultispan J)
        Equations