X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FProductCategories_ch1_6_1.v;h=8373b3743bd7548b63479353f497a019af0eb90e;hp=697641c3e3b0c5298d7a8259d2f037b3aaf81555;hb=fd14c25703d15bd78088c67ff3d417d435b6b136;hpb=ff3003c261295c60d367580b6700396102eb5a9c

diff --git a/src/ProductCategories_ch1_6_1.v b/src/ProductCategories_ch1_6_1.v
index 697641c..8373b37 100644
--- a/src/ProductCategories_ch1_6_1.v
+++ b/src/ProductCategories_ch1_6_1.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
@@ -126,6 +126,12 @@ Section ProductCategoryFunctors.
               case g as [ [g11 g12] g2];
               intros; reflexivity).
     Defined.
+  Definition func_diagonal : Functor C (C ×× C) (fun c => (pair_obj c c)).
+    refine {| fmor := fun a b f => @pair_mor _ _ C _ _ C (pair_obj a a) (pair_obj b b) f f |}.
+    abstract (intros; simpl; repeat split; simpl; auto).
+    abstract (intros; simpl; repeat split; simpl; auto).
+    abstract (intros; simpl; repeat split; simpl; auto).
+    Defined.
 End ProductCategoryFunctors.
 
 Section func_prod.