• API
• FAQ
• Tools
• Archive
SHARE
TWEET

# Untitled

a guest Jul 6th, 2017 82 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. Inductive False : Prop :=.
2. Inductive True : Prop := I.
3. Inductive eq {T : Type} (x : T) : T -> Prop := refl : eq x x.
4. Inductive and (X Y : Type) : Type :=
5. | both : X -> Y -> and X Y.
6. Inductive or (X Y : Type) : Type :=
7. | inleft : X -> or X Y
8. | inright : Y -> or X Y.
9. Inductive Sigma (T : Type) (P : T -> Type) : Type :=
10. | witnessS : forall t : T, P t -> Sigma T P.
11. Inductive Exists (T : Type) (P : T -> Prop) : Prop :=
12. | witnessE : forall t : T, P t -> Exists T P.
13.
14. Definition pi1 {T} {P} (S : Sigma T P) : T :=
15.   match S with
16.     | witnessS t _ => t
17.   end.
18.
19. Theorem symm (T : Type) (x y : T) : eq x y -> eq y x.
20. intro E; elim E; apply refl.
21. Defined.
22.
23. Theorem trans (T : Type) (x y z : T) : eq x y -> eq y z -> eq x z.
24. intro E; elim E.
25. intro E'; elim E'.
26. apply refl.
27. Defined.
28.
29. Definition Relation (T : Type) := T -> T -> Prop.
30.
31. Record Equivalence {T : Type} (R : Relation T) :=
32.   { equivalence_reflexivity : forall x, R x x
33.   ; equivalence_symmetry : forall x y, R x y -> R y x
34.   ; equivalence_transitivity : forall x y z, R x y -> R y z -> R x z
35.   }.
36.
37. Theorem eq_Equivalence (T : Type) : Equivalence (@eq T).
38. apply Build_Equivalence.
39. intros x; apply refl.
40. intros x y; apply symm.
41. intros x y z; apply trans.
42. Defined.
43.
44. Theorem eq_f_Equivalence (X T : Type) (f : X -> T) : Equivalence (fun x x' => @eq T (f x) (f x')).
45. apply Build_Equivalence.
46. intros x; apply refl.
47. intros x y; apply symm.
48. intros x y z; apply trans.
49. Defined.
50.
51. Definition Respectful
52.   {A : Type} (R : Relation A)
53.   {B : Type} (S : Relation B)
54.   (f : A -> B) : Prop :=
55.   forall a a', R a a' -> S (f a) (f a').
56.
57. Record Category
58.   (Ob : Type) (Hom : Ob -> Ob -> Type)
59.   (ObEq : Relation Ob) (HomEq : forall X Y, Relation (Hom X Y)) :=
60.   { identity : forall {X}, Hom X X
61.   ; compose : forall {X Y Z}, Hom X Y -> Hom Y Z -> Hom X Z
62.   ; compose_respectful_left : forall {X Y Z} (f : Hom X Y),
63.     Respectful (HomEq Y Z) (HomEq X Z) (fun g => compose f g)
64.   ; compose_respectful_right : forall {X Y Z} (g : Hom Y Z),
65.     Respectful (HomEq X Y) (HomEq X Z) (fun f => compose f g)
66.   ; category_ObEq_equivalence : Equivalence ObEq
67.   ; category_HomEq_equivalence : forall X Y, Equivalence (HomEq X Y)
68.   ; category_associativity : forall X Y Z W,
69.     forall (f : Hom X Y) (g : Hom Y Z) (h : Hom Z W),
70.       HomEq _ _ (compose (compose f g) h) (compose f (compose g h))
71.   ; category_left_identity : forall X Y,
72.     forall (f : Hom X Y),
73.       HomEq _ _ (compose identity f) f
74.   ; category_right_identity : forall X Y,
75.     forall (f : Hom X Y),
76.       HomEq _ _ (compose f identity) f
77.   }.
78.
79.
80. Section Setoids.
81.
82. Record Setoid :=
83.   { carrier : Type
84.   ; relation : Relation carrier
85.   ; setoid_relation_eq : Equivalence relation
86.   }.
87.
88. Definition Morphism (X Y : Setoid) :=
89.   Sigma (carrier X -> carrier Y) (fun f => Respectful (relation X) (relation Y) f).
90.
91. Definition Morphism_Identity (X : Setoid) : Morphism X X.
92. apply (witnessS (carrier X -> carrier X) _ (fun x => x)).
93. unfold Respectful; intros; assumption.
94. Defined.
95.
96. Definition Morphism_Compose (X Y Z : Setoid) (f : Morphism X Y) (g : Morphism Y Z) : Morphism X Z.
97. apply (witnessS (carrier X -> carrier Z) _ (fun x => pi1 g (pi1 f x))).
98. destruct f; destruct g.
99. unfold Respectful in *; simpl; intros.
100. apply r0.
101. apply r.
102. assumption.
103. Defined.
104.
105. Definition Morphism_equality (X Y : Setoid) (m m' : Morphism X Y) :=
106.   forall x : carrier X,
107.     relation Y (pi1 m x) (pi1 m' x).
108.
109. Definition Setoid_Isomorphism (S T : Setoid) : Prop :=
110.   Exists (and (Morphism S T) (Morphism T S)) (fun fg =>
111.     match fg with
112.       | both f g => and
113.          (Morphism_equality _ _ (Morphism_Compose _ _ _ f g)
114.                                (Morphism_Identity _))
115.          (Morphism_equality _ _ (Morphism_Compose _ _ _ g f)
116.                                (Morphism_Identity _))
117.     end).
118.
119. Theorem Equivalence_Setoid_Isomorphism : Equivalence (fun X Y : Setoid => Setoid_Isomorphism X Y).
120. apply Build_Equivalence; unfold Setoid_Isomorphism.
121.
122. intro; apply (witnessE _ _ (both _ _ (Morphism_Identity _) (Morphism_Identity _))).
123. assert (Morphism_equality x x
124.         (Morphism_Compose x x x (Morphism_Identity x) (Morphism_Identity x))
125.         (Morphism_Identity x));
126. unfold Morphism_equality; unfold Morphism_Compose; simpl.
127.
128. intros; apply (setoid_relation_eq x).
129. constructor.
130. apply H.
131. apply H.
132.
133. intros x y [[l r] [l' r']].
134. apply (witnessE _ _ (both _ _ r l)).
135. apply (both _ _ r' l').
136.
137. intros x y z [[l r] [l' r']] [[r'' h] [r''' h']].
138. pose (Morphism_Compose _ _ _ l r'') as m.
139. pose (Morphism_Compose _ _ _ h r) as m'.
140. apply (witnessE _ _ (both _ _ m m')).
141. constructor;
142. unfold Morphism_equality in *; unfold Morphism_Compose in *; simpl in *; clear m; clear m';
143. intros.
144.
145. eapply equivalence_transitivity.
146. apply (setoid_relation_eq x).
147. Focus 2.
148. apply l'.
149. assert (relation y (pi1 h (pi1 r'' (pi1 l x0))) (pi1 l x0)).
150. apply r'''.
151. unfold Morphism in r.
152. destruct r.
153. simpl.
154. apply r.
155. assumption.
156.
157. eapply equivalence_transitivity.
158. apply (setoid_relation_eq z).
159. Focus 2.
160. apply h'.
161. assert (relation y (pi1 l (pi1 r (pi1 h x0))) (pi1 h x0)).
162. apply r'.
163. unfold Morphism in r'.
164. destruct r''.
165. simpl.
166. apply r0.
167. assumption.
168. Defined.
169.
170. End Setoids.
171.
172. Section SET.
173.   Definition SET : Category
174.     Setoid (fun X Y => Morphism X Y)
175.     (fun X Y => Setoid_Isomorphism X Y) (fun X Y f g => Morphism_equality X Y f g).
176.   Print Build_Category.
177.   apply (Build_Category
178.     Setoid (fun X Y => Morphism X Y)
179.     (fun X Y => Setoid_Isomorphism X Y) (fun X Y f g => Morphism_equality X Y f g)
180.     (fun X => Morphism_Identity X)
181.     (fun X Y Z f g => Morphism_Compose X Y Z f g));
182.   unfold Respectful in *;
183.   unfold Morphism_equality in *;
184.   unfold Morphism_Compose in *;
185.   simpl in *; intros.
186.
187.   apply H.
188.
189.   pose (H x).
190.   destruct g; simpl in *.
191.   unfold Respectful in *.
192.   apply r0.
193.   apply r.
194.
195.   apply Equivalence_Setoid_Isomorphism.
196.
197.   apply Build_Equivalence.
198.   intros; apply equivalence_reflexivity.
199.   apply (setoid_relation_eq Y).
200.   intros; apply equivalence_symmetry.
201.   apply (setoid_relation_eq Y).
202.   apply H.
203.   intros; eapply equivalence_transitivity.
204.   apply (setoid_relation_eq Y).
205.   apply H.
206.   apply H0.
207.
208.   apply equivalence_reflexivity.
209.   apply (setoid_relation_eq W).
210.   apply equivalence_reflexivity.
211.   apply (setoid_relation_eq Y).
212.   apply equivalence_reflexivity.
213.   apply (setoid_relation_eq Y).
214.   Defined.
215. End SET.
216.
217. (*
218.
219. Definition SET : Category Set (fun X Y => X -> Y) (eq) (fun _ _ f g => forall x, eq (f x) (g x)).
220. apply (Build_Category
221.   Set (fun X Y => X -> Y) (eq) (fun _ _ f g => forall x, eq (f x) (g x))
222.   (fun X x => x)
223.   (fun X Y Z f g x => g (f x))).
224.
225. unfold Respectful; intros.
226. apply H.
227.
228. unfold Respectful; intros.
229. elim (H x).
230. apply refl.
231.
232. apply eq_Equivalence.
233.
234. intros; apply Build_Equivalence.
235. intros; apply refl.
236. intros; apply symm.
237. apply H.
238. intros; eapply trans.
239. apply H.
240. apply H0.
241.
242. intros; apply refl.
243.
244. intros; apply refl.
245.
246. intros; apply refl.
247. Defined.
248.
249. *)
250.
251. Record Functor
252.   {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq)
253.   {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq') :=
254.   { MapOb : Ob -> Ob'
255.   ; MapHom : forall X Y : Ob, Hom X Y -> Hom' (MapOb X) (MapOb Y)
256.   ; functor_respectful : forall X Y : Ob,
257.     Respectful (@HomEq X Y) (@HomEq' (MapOb X) (MapOb Y)) (MapHom X Y)
258.   ; functor_identity : forall X,
259.     HomEq' _ _ (identity _ _ _ _ D) (MapHom X X (identity _ _ _ _ C))
260.   ; functor_compose : forall X Y Z,
261.     forall (f : Hom X Y) (g : Hom Y Z),
262.       HomEq' _ _ (MapHom _ _ (compose _ _ _ _ C f g))
263.                  (compose _ _ _ _ D (MapHom _ _ f) (MapHom _ _ g))
264.   }.
265.
266. Section Opposite.
267.   Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
268.
269.   Definition Op : Category Ob (fun Y X => Hom X Y) ObEq (fun X Y f g => HomEq Y X f g).
270.   apply (Build_Category
271.     Ob (fun Y X => Hom X Y) ObEq (fun X Y f g => HomEq Y X f g)
272.     (fun X => identity _ _ _ _ C)
273.     (fun X Y Z f g => compose _ _ _ _ C g f)).
274.
275.   unfold Respectful; intros.
276.   apply compose_respectful_right.
277.   assumption.
278.
279.   unfold Respectful; intros.
280.   apply compose_respectful_left.
281.   assumption.
282.
283.   apply (category_ObEq_equivalence _ _ _ _ C).
284.   intros X Y; pose (category_HomEq_equivalence _ _ _ _ C) as E.
285.   destruct (E Y X) as [axR axS axT].
286.   apply Build_Equivalence; assumption.
287.
288.   intros.
289.   apply equivalence_symmetry.
290.   apply (category_HomEq_equivalence _ _ _ _ C).
291.   apply category_associativity.
292.
293.   intros.
294.   apply category_right_identity.
295.
296.   intros.
297.   apply category_left_identity.
298.   Defined.
299. End Opposite.
300.
301. Section Functors.
302.   Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
303.   Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').
304.   Context {Ob'' Hom'' ObEq'' HomEq''} (E : Category Ob'' Hom'' ObEq'' HomEq'').
305.
306.   Definition Functor_equality (F G : Functor C D) : Prop :=
307.     and (forall X, ObEq' (MapOb C D F X) (MapOb C D F X))
308.         (forall X Y (f : Hom X Y), HomEq' _ _ (MapHom C D F X Y f) (MapHom C D G X Y f)).
309.
310.   Definition Identity_Functor : Functor C C.
311.   apply (Build_Functor
312.     _ _ _ _ C
313.     _ _ _ _ C
314.     (fun X => X)
315.     (fun X Y f => f)
316.   ).
317.
318.   unfold Respectful; intros; assumption.
319.
320.   intros; apply equivalence_reflexivity.
321.   apply (category_HomEq_equivalence _ _ _ _ C X X).
322.
323.   intros; apply equivalence_reflexivity.
324.   apply (category_HomEq_equivalence _ _ _ _ C X Z).
325.   Defined.
326.
327.   Definition Compose_Functors (F : Functor C D) (G : Functor D E) : Functor C E.
328.   apply (Build_Functor
329.     _ _ _ _ C
330.     _ _ _ _ E
331.     (fun X => MapOb _ _ G (MapOb _ _ F X))
332.     (fun X Y f => MapHom _ _ G _ _ (MapHom _ _ F _ _ f))
333.   ).
334.
335.   unfold Respectful; intros.
336.   apply functor_respectful.
337.   apply functor_respectful.
338.   assumption.
339.
340.   intros.
341.   apply equivalence_transitivity with
342.     (y := MapHom D E G (MapOb C D F X) (MapOb C D F X)
343.       (identity Ob' Hom' ObEq' HomEq' D)).
344.   apply (category_HomEq_equivalence _ _ _ _ E _ _).
345.   apply functor_identity.
346.
347.   apply functor_respectful.
348.   apply functor_identity.
349.
350.   intros.
351.   assert (
352.     HomEq' _ _
353.     (MapHom C D F X Z (compose Ob Hom ObEq HomEq C f g))
354.     (compose _ _ _ _ D
355.       (MapHom C D F X Y f)
356.       (MapHom C D F Y Z g))) as lemma by apply functor_compose.
357.   Print functor_respectful.
358.   pose (functor_respectful D E G _ _ _ _ lemma) as lemma'.
359.   eapply equivalence_transitivity.
360.   apply (category_HomEq_equivalence _ _ _ _ E _ _).
361.   apply lemma'.
362.   apply (functor_compose D E G).
363.   Defined.
364. End Functors.
365.
366. Section Isomorphism.
367.   Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
368.
369.   Record Isomorphism {X Y : Ob} (iso : Hom X Y) :=
370.     { inverse : Hom Y X
371.     ; isomorphism_left_inverse : HomEq _ _ (compose _ _ _ _ C inverse iso) (identity _ _ _ _ C)
372.     ; isomorphism_right_inverse : HomEq _ _ (compose _ _ _ _ C iso inverse) (identity _ _ _ _ C)
373.     }.
374.
375. End Isomorphism.
376.
377. Section Terminal.
378.   Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
379.
380.   Record Terminal :=
381.     { terminal_object : Ob
382.     ; terminal_morphism : forall X, Hom X terminal_object
383.     ; terminal_morphism_unique : forall X (f : Hom X terminal_object),
384.       HomEq _ _ f (terminal_morphism X)
385.     }.
386.
387.   Theorem Terminal_Isomorphism (terminal : Terminal) :
388.     Isomorphism C (terminal_morphism terminal (terminal_object terminal)).
389.   apply (Build_Isomorphism
390.     C _ _ _
391.     (terminal_morphism terminal (terminal_object terminal))).
392.   apply equivalence_transitivity with (y := terminal_morphism terminal (terminal_object terminal)).
393.   apply (category_HomEq_equivalence _ _ _ _ C _ _).
394.   apply terminal_morphism_unique.
395.   apply equivalence_symmetry.
396.   apply (category_HomEq_equivalence _ _ _ _ C _ _).
397.   apply terminal_morphism_unique.
398.
399.   apply equivalence_transitivity with (y := terminal_morphism terminal (terminal_object terminal)).
400.   apply (category_HomEq_equivalence _ _ _ _ C _ _).
401.   apply terminal_morphism_unique.
402.   apply equivalence_symmetry.
403.   apply (category_HomEq_equivalence _ _ _ _ C _ _).
404.   apply terminal_morphism_unique.
405.   Defined.
406.
407. End Terminal.
408.
409. Section Initial.
410.   Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
411.
412.   Definition Initial := @Terminal Ob (fun Y X => Hom X Y) (fun X Y f g => HomEq Y X f g).
413.
414.   Definition initial_object (i : Initial) := terminal_object i.
415.
416.   Definition initial_morphism (i : Initial) : forall X, Hom (initial_object i) X.
417.   destruct i as [termOb termMor termUniq].
418.   simpl.
419.   intro; apply termMor.
420.   Defined.
421.
422.   Definition initial_morphism_unique (i : Initial) : forall X (f : Hom (initial_object i) X), HomEq _ _ f (initial_morphism i X).
423.   destruct i as [termOb termMor termUniq]; simpl.
424.   intros.
425.   apply termUniq.
426.   Defined.
427.
428.   Theorem Initial_Isomorphism (i : Initial) :
429.     Isomorphism C (initial_morphism i (initial_object i)).
430.
431.     pose (@Terminal_Isomorphism _ _ _ _ (Op C) i) as t.
432.     destruct t as [tInv tInvL tInvR]; simpl in *.
433.
434.     destruct i as [iObj iMor iUniq]; simpl in *.
435.
436.     apply Build_Isomorphism with (inverse := tInv).
437.
438.     apply tInvR.
439.
440.     apply tInvL.
441.   Defined.
442. End Initial.
443.
444. Section NaturalTransform.
445.   Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
446.   Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').
447.   Context (F : Functor C D) (G : Functor C D).
448.
449.   Record NaturalTransform :=
450.     { eta_ : forall X, Hom' (MapOb _ _ F X) (MapOb _ _ G X)
451.     ; naturality : forall X Y,
452.       forall f : Hom X Y,
453.         HomEq' _ _ (compose _ _ _ _ D (MapHom _ _ F _ _ f) (eta_ Y))
454.                    (compose _ _ _ _ D (eta_ X) (MapHom _ _ G _ _ f))
455.     }.
456. End NaturalTransform.
457.
458. Section CategoryOfSmallCats.
459.
460. Record SmallCategory :=
461.   { S : Set
462.   ; R : Relation S
463.   ; Hom : S -> S -> Set
464.   ; HomR : forall X Y, Relation (Hom X Y)
465.   ; smallCategory_carrier : Category S Hom R HomR
466.   }.
467.
468. Definition SmallCategory_Isomorphism : Relation SmallCategory.
469. unfold Relation.
470. intros [S_C R_C Hom_C HomR_C C] [S_D R_D Hom_D HomR_D D].
472.
473. Definition SmallFunctor (C : SmallCategory) (D : SmallCategory) := Functor (smallCategory_carrier C) (smallCategory_carrier D).
474.
475. Axiom SmallFunctor_Isomorphism : forall C D, Relation (SmallFunctor C D).
476.
477. Definition CAT : Category SmallCategory SmallFunctor SmallCategory_Isomorphism SmallFunctor_Isomorphism.
478. Print Build_Category.
479. apply (Build_Category
480.   SmallCategory SmallFunctor SmallCategory_Isomorphism SmallFunctor_Isomorphism
481.   (fun X =>
482.     Identity_Functor (smallCategory_carrier X))
483.   (fun X Y Z f g =>
484.     Compose_Functors (smallCategory_carrier X)
485.                      (smallCategory_carrier Y)
486.                      (smallCategory_carrier Z)
487.                      f g)).
489.
490. End CategoryOfSmallCats.
491.
492. Section NaturalTransforms.
493.   Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
494.   Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').
495.   Context (F : Functor C D) (G : Functor C D) (H : Functor C D).
496.
497.   Context (eta : NaturalTransform C D F G).
498.   Context (nu : NaturalTransform C D G H).
499.
500.   Definition Identity_NaturalTransform'' : NaturalTransform C C (Identity_Functor C) (Identity_Functor C).
501.   Print Build_NaturalTransform.
502.   apply (Build_NaturalTransform
503.     C C (Identity_Functor C) (Identity_Functor C)
504.     (fun X => identity _ _ _ _ C)).
505.   simpl; intros.
506.   eapply equivalence_transitivity.
507.   apply (category_HomEq_equivalence _ _ _ _ C).
508.   apply category_right_identity.
509.   apply equivalence_symmetry.
510.   apply (category_HomEq_equivalence _ _ _ _ C).
511.   apply category_left_identity.
512.   Defined.
513.
514.   Definition Identity_NaturalTransform : NaturalTransform C D F F.
515.   Print Build_NaturalTransform.
516.   apply (Build_NaturalTransform
517.     C D F F
518.     (fun X => identity _ _ _ _ D)).
519.   simpl; intros.
520.   eapply equivalence_transitivity.
521.   apply (category_HomEq_equivalence _ _ _ _ D).
522.   apply category_right_identity.
523.   apply equivalence_symmetry.
524.   apply (category_HomEq_equivalence _ _ _ _ D).
525.   apply category_left_identity.
526.   Defined.
527.
528.   Definition Compose_NaturalTransformations : NaturalTransform C D F H.
529.   Print Build_NaturalTransform.
530.   Print eta_.
531.   apply (Build_NaturalTransform
532.     C D F H
533.     (fun X => compose _ _ _ _ D (eta_ C D F G eta X) (eta_ C D G H nu X))).
534.   intros.
535.   apply equivalence_transitivity with
536.     (y := compose _ _ _ _ D
537.       (compose Ob' Hom' ObEq' HomEq' D (MapHom C D F X Y f)
538.         (eta_ C D F G eta Y))
539.       (eta_ C D G H nu Y)).
540.   apply (category_HomEq_equivalence _ _ _ _ D).
541.   eapply equivalence_symmetry.
542.   apply (category_HomEq_equivalence _ _ _ _ D).
543.   apply (category_associativity).
544.   apply equivalence_transitivity with
545.     (y := compose _ _ _ _ D (eta_ C D F G eta _)
546.       (compose _ _ _ _ D (MapHom C D G _ _ f)
547.         (eta_ C D G H nu Y))).
548.   apply (category_HomEq_equivalence _ _ _ _ D).
549.
550.   eapply equivalence_symmetry.
551.   apply (category_HomEq_equivalence _ _ _ _ D).
552.   eapply equivalence_transitivity with
553.     (y := compose Ob' Hom' ObEq' HomEq' D
554.       (compose Ob' Hom' ObEq' HomEq' D (eta_ C D F G eta _)
555.         (MapHom C D G X Y f)) (eta_ C D G H nu Y)).
556.   apply (category_HomEq_equivalence _ _ _ _ D).
557.   eapply equivalence_symmetry.
558.   apply (category_HomEq_equivalence _ _ _ _ D).
559.   apply category_associativity.
560.   apply compose_respectful_right.
561.   eapply equivalence_symmetry.
562.   apply (category_HomEq_equivalence _ _ _ _ D).
563.   apply naturality.
564.
565.   eapply equivalence_symmetry.
566.   apply (category_HomEq_equivalence _ _ _ _ D).
567.   eapply equivalence_transitivity with
568.     (y := compose Ob' Hom' ObEq' HomEq' D (eta_ C D F G eta X)
569.       (compose Ob' Hom' ObEq' HomEq' D
570.         (eta_ C D G H nu X) (MapHom C D H X Y f))).
571.   apply (category_HomEq_equivalence _ _ _ _ D).
572.   apply category_associativity.
573.   apply compose_respectful_left.
574.   eapply equivalence_symmetry.
575.   apply (category_HomEq_equivalence _ _ _ _ D).
576.   apply naturality.
577.   Defined.
578.
579. End NaturalTransforms.
580.
581. Section FunctorCategory.
582.   Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
583.   Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').
584.
585.   Definition FunctorCategory : Category
586.     (Functor C D) (NaturalTransform C D)
587.     (fun F G => forall c, F c = G c) (fun _ _ _ _ => True).
588.   Print Identity_NaturalTransform.
589.   apply (Build_Category
590.     (Functor C D) (NaturalTransform C D)
591.     (fun F G => _) (fun _ _ _ _ => True)
592.     (fun F => Identity_NaturalTransform C D F)
593.     (fun F G H eta nu => Compose_NaturalTransformations C D F G H eta nu)).
594.
595.
596. (*
597. *** Local Variables: ***
598. *** coq-prog-args: ("-emacs-U" "-nois") ***
599. *** End: ***
600. *)
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top