Generalizable All Variables.
Require Import Preamble.
-Require Import General.
(* very handy *)
(*
| a::b => a -> listOfTypesToType b ret
end.
*)
-
+(*
Section Algebras.
Local Notation "a :: b" := (vec_cons a b).
*)
End Algebras.
-
+*)
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
(* definition 1.1 *)
Class Category
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
(******************************************************************************)
(* Chapter 3.4: CoEqualizers *)
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
(******************************************************************************)
(* Chapter 3.3: Equalizers *)
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
(******************************************************************************)
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.