projects / coq-categories.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
add inverse form of ni_commutes
[coq-categories.git] / src / CoEqualizers_ch3_4.v
1 Generalizable All Variables.
2 Require Import Notations.
3
4 (******************************************************************************)
5 (* Chapter 3.4: CoEqualizers                                                  *)
6 (******************************************************************************)
7
8 (* FIXME *)
formalization of basic category theory in Coq