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
  • One or more equations did not get rendered due to their size.
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
    • One or more equations did not get rendered due to their size.
    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
    • One or more equations did not get rendered due to their size.
    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
      • One or more equations did not get rendered due to their size.