Commit 2023-06-06 03:55 9aaa5995

View on Github →

feat: port CategoryTheory.WithTerminal (#2630)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/WithTerminal.lean

added def CategoryTheory.WithInitial.Hom

added def CategoryTheory.WithInitial.comp

added def CategoryTheory.WithInitial.down

added theorem CategoryTheory.WithInitial.down_comp

added theorem CategoryTheory.WithInitial.down_id

added theorem CategoryTheory.WithInitial.false_of_to_star

added def CategoryTheory.WithInitial.homTo

added def CategoryTheory.WithInitial.id

added def CategoryTheory.WithInitial.incl

added def CategoryTheory.WithInitial.inclLift

added def CategoryTheory.WithInitial.inclLiftToInitial

added def CategoryTheory.WithInitial.lift

added def CategoryTheory.WithInitial.liftStar

added theorem CategoryTheory.WithInitial.liftStar_lift_map

added def CategoryTheory.WithInitial.liftToInitial

added def CategoryTheory.WithInitial.liftToInitialUnique

added def CategoryTheory.WithInitial.liftUnique

added def CategoryTheory.WithInitial.map

added def CategoryTheory.WithInitial.starInitial

added inductive CategoryTheory.WithInitial

added def CategoryTheory.WithTerminal.Hom

added def CategoryTheory.WithTerminal.comp

added def CategoryTheory.WithTerminal.down

added theorem CategoryTheory.WithTerminal.down_comp

added theorem CategoryTheory.WithTerminal.down_id

added theorem CategoryTheory.WithTerminal.false_of_from_star

added def CategoryTheory.WithTerminal.homFrom

added def CategoryTheory.WithTerminal.id

added def CategoryTheory.WithTerminal.incl

added def CategoryTheory.WithTerminal.inclLift

added def CategoryTheory.WithTerminal.inclLiftToTerminal

added def CategoryTheory.WithTerminal.lift

added def CategoryTheory.WithTerminal.liftStar

added def CategoryTheory.WithTerminal.liftToTerminal

added def CategoryTheory.WithTerminal.liftToTerminalUnique

added def CategoryTheory.WithTerminal.liftUnique

added theorem CategoryTheory.WithTerminal.lift_map_liftStar

added def CategoryTheory.WithTerminal.map

added def CategoryTheory.WithTerminal.starTerminal

added inductive CategoryTheory.WithTerminal