Library CatSem.CAT.initial_terminal

Require Export CatSem.CAT.category.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Transparent Obligations.
Unset Automatic Introduction.

Section Initial_Terminal.

Variable obC: Type.
Variable morC: obC -> obC -> Type.

Class Initial (C:Cat_struct morC) := {
     Init : obC;
     InitMor: forall a:obC, morC Init a;
     InitMorUnique: forall b (f:morC Init b), f == InitMor b
}.

Class Terminal (C:Cat_struct morC) := {
      Term: obC;
      TermMor: forall a: obC, morC a Term;
      TermMorUnique: forall b f, f == TermMor b
}.

End Initial_Terminal.

Implicit Arguments Init [obC morC C Initial].
Implicit Arguments Term [obC morC C Terminal].