Documentation

Mathlib.CategoryTheory.WithTerminal.FinCategory

WithTerminal C and WithInitial C are finite whenever C is #

If C has finitely many objects, then so do WithTerminal C and WithInitial C, and likewise if C has finitely many morphisms as well.

source
def CategoryTheory.WithTerminal.optionEquiv (C : Type u) :
Option C ≃ WithTerminal C

The equivalence between Option C and WithTerminal C (they are both the type C plus an extra object none or star).

Equations
    Instances For
      source
      instance CategoryTheory.WithTerminal.instFintype (C : Type u) [Fintype C] :
      Fintype (WithTerminal C)
      Equations
        source
        instance CategoryTheory.WithTerminal.instFinCategory (C : Type u) [SmallCategory C] [FinCategory C] :
        FinCategory (WithTerminal C)
        Equations
          source
          def CategoryTheory.WithInitial.optionEquiv (C : Type u) :
          Option C ≃ WithInitial C

          The equivalence between Option C and WithInitial C (they are both the type C plus an extra object none or star).

          Equations
            Instances For
              source
              instance CategoryTheory.WithInitial.instFintype (C : Type u) [Fintype C] :
              Fintype (WithInitial C)
              Equations
                source
                instance CategoryTheory.WithInitial.instFinCategory (C : Type u) [SmallCategory C] [FinCategory C] :
                FinCategory (WithInitial C)
                Equations