• API
• FAQ
• Tools
• Archive
SHARE
TWEET

Untitled

a guest Jul 7th, 2017 85 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. Set Implicit Arguments.
2.
3. Ltac hypothesis := match goal with [ H : _ |- _ ] => apply H end.
4.
5. Section PublicService.
6.
7.   Inductive False : Type :=.
8.
9.   Definition Not (P : Type) := P -> False.
10.
11.   Inductive True : Type :=
12.   | I : True.
13.
14.   Inductive Identity (T : Type) (t : T) : T -> Type :=
15.   | identical : Identity t t.
16.
17.   Inductive And (P Q : Type) : Type :=
18.   | both : P -> Q -> And P Q.
19.   Definition proj1 {P Q} (a : And P Q) : P :=
20.     match a with both p q => p end.
21.   Definition proj2 {P Q} (a : And P Q) : Q :=
22.     match a with both p q => q end.
23.
24.   Definition And_idem (P : Type) : P -> And P P.
25.   intro p; apply (both p p).
26.   Defined.
27.
28.   Inductive Or (P Q : Type) : Type :=
29.   | inleft : P -> Or P Q
30.   | inright : Q -> Or P Q.
31.
32.   Definition Decidable (P : Type) := Or P (Not P).
33.
34.   Inductive Sigma (T : Type) (P : T -> Type) : Type :=
35.   | witness : forall t : T, P t -> Sigma P.
36.   Definition pi1 {T P} (s : @Sigma T P) : T :=
37.     match s with
38.       | witness t _ => t
39.     end.
40.   Definition pi2 {T P} (s : @Sigma T P) : P (pi1 s) :=
41.     match s with
42.       | witness _ p => p
43.     end.
44.
45.   Definition Relation (T : Type) := T -> T -> Type.
46.
47.   Record Equivalence {T : Type} (R : Relation T)
48.     := { equivalence_reflexivity : forall x, R x x
49.        ; equivalence_symmetry : forall x y, R x y -> R y x
50.        ; equivalence_transitivity : forall x y z, R x y -> R y z -> R x z
51.        }.
52.
53.   Theorem Equivalence_Identity {T : Type} : Equivalence (@Identity T).
54.   apply Build_Equivalence.
55.   intros x; apply identical.
56.   intros x y; intro E; elim E; apply identical.
57.   intros x y z; intros E F; elim F; elim E; apply identical.
58.   Defined.
59.
60.   Theorem Equivalence_Pullback {X T} (R : Relation T) (f : X -> T) : Equivalence R -> Equivalence (fun x y => R (f x) (f y)).
61.     intros [Erefl Esymm Etrans].
62.     apply Build_Equivalence.
63.     intros; apply Erefl.
64.     intros; apply Esymm; assumption.
65.     intros; apply Etrans with (y := f y); assumption.
66.   Defined.
67.
68.   Theorem Equivalence_Identity_Pullback {X T : Type} (f : X -> T) : Equivalence (fun x x' => @Identity T (f x) (f x')).
69.     apply Equivalence_Pullback.
70.     apply Equivalence_Identity.
71.   Defined.
72.
73. End PublicService.
74.
75. Section CategoryTheory.
76.
77. Record Category
78.   (Ob : Type)
79.   (Hom : Ob -> Ob -> Type)
80.   (Hom_eq : forall X Y, Relation (Hom X Y))
81.
82.   := { identity : forall X, Hom X X
83.      ; compose : forall X Y Z, Hom X Y -> Hom Y Z -> Hom X Z
84.      ; Compose_respectful_left : forall X Y Z (f f' : Hom X Y) (g : Hom Y Z),
85.        Hom_eq _ _ f f' ->
86.        Hom_eq _ _ (compose f g) (compose f' g)
87.      ; Compose_respectful_right : forall X Y Z (f : Hom X Y) (g g' : Hom Y Z),
88.        Hom_eq _ _ g g' ->
89.        Hom_eq _ _ (compose f g) (compose f g')
90.      ; category_equivalence : forall X Y, Equivalence (Hom_eq X Y)
91.      ; category_left_identity : forall X Y (f : Hom X Y),
92.        Hom_eq _ _ (compose (identity _) f) f
93.      ; category_right_identity : forall X Y (f : Hom X Y),
94.        Hom_eq _ _ (compose f (identity _)) f
95.      ; category_associativity : forall X Y Z W (f : Hom X Y) (g : Hom Y Z) (h : Hom Z W),
96.        Hom_eq _ _ (compose f (compose g h))
97.                   (compose (compose f g) h)
98.      }.
99.
100. End CategoryTheory.
101.
102. Notation "f '[' C ']'  g" := (compose C _ _ _ f g) (at level 20).
103. Notation "'Id[' C ']'" := (identity C _) (at level 20).
104.
105. Section Functor.
106.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
107.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
108.
109.   Record Functor
110.     := { Map_Ob : C_Ob -> D_Ob
111.        ; Map_Hom : forall X Y,
112.          C_Hom X Y -> D_Hom (Map_Ob X) (Map_Ob Y)
113.        ; functor_identity : forall X,
114.          D_Hom_eq (Map_Hom (identity C X)) (identity D (Map_Ob X))
115.        ; functor_compose : forall X Y Z (f : C_Hom X Y) (g : C_Hom Y Z),
116.          D_Hom_eq (Map_Hom (compose C _ _ _ f g)) (compose D _ _ _ (Map_Hom f) (Map_Hom g))
117.        ; Map_Hom_respectful : forall X Y (f f' : C_Hom X Y),
118.          C_Hom_eq f f' -> D_Hom_eq (Map_Hom f) (Map_Hom f')
119.        }.
120.
121. End Functor.
122.
123. Notation "F '@' x" := (Map_Ob F x) (at level 20).
124. Notation "F '\$' f" := (Map_Hom F f) (at level 20).
125.
126. Section SYMBOLIC.
127.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
128.
129.   Inductive Syntax : Ob -> Ob -> Type :=
130.   | idSYM : forall X : Ob, Syntax X X
131.   | compSYM : forall X Y Z : Ob, Syntax X Y -> Syntax Y Z -> Syntax X Z
132.   | injSYM : forall X Y, Hom X Y -> Syntax X Y.
133.
134.   Inductive Semantics : Ob -> Ob -> Type :=
135.   | nilSYM : forall X : Ob, Semantics X X
136.   | consSYM : forall X Y Z : Ob, Hom X Y -> Semantics Y Z -> Semantics X Z.
137.
138.   Fixpoint append {X Y Z : Ob} (f : Semantics X Y) : Semantics Y Z -> Semantics X Z :=
139.   match f with
140.     | nilSYM _ => fun g => g
141.     | consSYM _ _ _ s f => fun g => consSYM s (append f g)
142.   end.
143.
144.   Lemma append_nil :
145.     forall (X Y : Ob) (x : Semantics X Y),
146.       Identity (append x (nilSYM Y)) x.
147.     induction x; simpl.
148.     apply identical.
149.     elim (equivalence_symmetry Equivalence_Identity _ _ IHx).
150.     apply identical.
151.   Defined.
152.
153.   Lemma append_associative :
154.   forall (X Y Z W : Ob) (f : Semantics X Y) (g : Semantics Y Z) (h : Semantics Z W),
155.     Identity (append f (append g h))
156.              (append (append f g) h).
157.     intros; induction f; simpl.
158.     apply identical.
159.     elim (IHf _).
160.     apply identical.
161.   Defined.
162.
163.   Fixpoint evalSYN {X Y} (s : Syntax X Y) : Semantics X Y :=
164.     match s with
165.       | idSYM _ => nilSYM _
166.       | compSYM _ _ _ f g => append (evalSYN f) (evalSYN g)
167.       | injSYM _ _ f => consSYM f (nilSYM _)
168.     end.
169.
170.   Fixpoint quoteSYN {X Y} (s : Semantics X Y) : Syntax X Y :=
171.     match s with
172.       | nilSYM _ => idSYM _
173.       | consSYM _ _ _ f s => compSYM (injSYM f) (quoteSYN s)
174.     end.
175.
176.   Definition Syntax_eq {X Y : Ob} (f f' : Syntax X Y) :=
177.     Identity (evalSYN f) (evalSYN f').
178.   Theorem Equivalence_Syntax_eq {X Y} : Equivalence (@Syntax_eq X Y).
179.     apply (Equivalence_Identity_Pullback evalSYN).
180.   Defined.
181.
182.   Definition SYNTAX_category : Category Syntax (@Syntax_eq).
183.   apply (Build_Category Syntax (@Syntax_eq)
184.     idSYM
185.     compSYM); unfold Syntax_eq; simpl.
186.   intros X Y Z f f' g E; elim E; apply identical.
187.   intros X Y Z f g g' E; elim E; apply identical.
188.   intros X Y; apply Equivalence_Syntax_eq.
189.   intros X Y f; apply identical.
190.   intros X Y f; apply append_nil.
191.   intros X Y Z W f g h; apply append_associative.
192.   Defined.
193.
194.   Theorem quote_eval_equal {X Y : Ob} (f : Syntax X Y) :
195.     Syntax_eq (quoteSYN (evalSYN f)) f.
196.     induction f; simpl in *;
197.       try apply identical.
198.
199.     Lemma quote_eval_equal_lemma {X Y Z} (e1 : Semantics X Y) (e2 : Semantics Y Z) :
200.       Syntax_eq (quoteSYN (append e1 e2)) (compSYM (quoteSYN e1) (quoteSYN e2)).
201.       intros; induction e1; simpl.
202.       apply identical.
203.       elim (IHe1 e2).
204.       eapply (equivalence_transitivity (category_equivalence SYNTAX_category _ _)).
205.       Focus 2.
206.       apply (category_associativity SYNTAX_category _ _).
207.       apply (Compose_respectful_right SYNTAX_category).
208.       apply IHe1.
209.     Defined.
210.
211.     eapply (equivalence_transitivity Equivalence_Syntax_eq).
212.     apply quote_eval_equal_lemma.
213.     eapply (equivalence_transitivity (category_equivalence SYNTAX_category _ _)).
214.     apply (Compose_respectful_left SYNTAX_category).
215.     apply IHf1.
216.     eapply (equivalence_transitivity (category_equivalence SYNTAX_category _ _)).
217.     apply (Compose_respectful_right SYNTAX_category).
218.     apply IHf2.
219.     apply (equivalence_reflexivity (category_equivalence SYNTAX_category _ _)).
220.   Defined.
221.
222.   Fixpoint interpret_Syntax {X Y} (f : Syntax X Y) : Hom X Y :=
223.     match f with
224.       | idSYM _ => identity C _
225.       | compSYM _ _ _ f g => compose C _ _ _ (interpret_Syntax f) (interpret_Syntax g)
226.       | injSYM _ _ f => f
227.     end.
228.
229.   Fixpoint interpret_Semantics {X Y} (f : Semantics X Y) : Hom X Y :=
230.     match f with
231.       | nilSYM _ => identity C _
232.       | consSYM _ _ _ s f => compose C _ _ _ s (interpret_Semantics f)
233.     end.
234.
235.   Theorem interpretation_factors_through_evaluation {X Y} (f : Syntax X Y) :
236.     Hom_eq (interpret_Syntax f)
237.            (interpret_Semantics (evalSYN f)).
238.     induction f; simpl.
239.     apply (equivalence_reflexivity (category_equivalence C _ _)).
240.     eapply (equivalence_transitivity (category_equivalence C _ _)).
241.     apply Compose_respectful_left.
242.     apply IHf1.
243.     eapply (equivalence_transitivity (category_equivalence C _ _)).
244.     apply Compose_respectful_right.
245.     apply IHf2.
246.     Lemma append_pushthrough_compose {X Y Z} (f : Semantics X Y) (g : Semantics Y Z) :
247.       Hom_eq (compose C _ _ _ (interpret_Semantics f) (interpret_Semantics g))
248.              (interpret_Semantics (append f g)).
249.       induction f; simpl.
250.       apply category_left_identity.
251.       eapply (equivalence_transitivity (category_equivalence C _ _)).
252.       apply (equivalence_symmetry (category_equivalence C _ _)).
253.       apply (category_associativity C).
254.       apply Compose_respectful_right.
255.       apply IHf.
256.     Defined.
257.     apply append_pushthrough_compose.
258.
259.     apply (equivalence_symmetry (category_equivalence C _ _)).
260.     apply category_right_identity.
261.   Defined.
262.
263.   Definition Interpret : Functor SYNTAX_category C.
264.   Print Build_Functor.
265.   apply (Build_Functor
266.     SYNTAX_category C
267.     (fun X => X)
268.     (fun X Y f => interpret_Syntax f)
269.   ).
270.
271.   intros; apply (equivalence_reflexivity (category_equivalence C _ _)).
272.   intros; apply (equivalence_reflexivity (category_equivalence C _ _)).
273.
274.   intros X Y f f' E.
275.   pose (quote_eval_equal f) as A.
276.   pose (quote_eval_equal f') as B.
277.   pose (interpretation_factors_through_evaluation f) as U.
278.   pose (interpretation_factors_through_evaluation f') as V.
279.   unfold Syntax_eq in *.
280.   assert (
281.     Hom_eq (interpret_Syntax f) (interpret_Semantics (evalSYN f'))
282.   ) as P.
283.   elim E.
284.   assumption.
285.   eapply (equivalence_transitivity (category_equivalence C _ _)).
286.   apply P.
287.   apply (equivalence_symmetry (category_equivalence C _ _)).
288.   apply V.
289.   Defined.
290.
291. End SYMBOLIC.
292. Section Trinkets.
293.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
294.
295.   Definition Isomorphism (X Y : Ob) (f : Hom X Y) :=
296.     @Sigma (Hom Y X)
297.     (fun (g : Hom Y X) =>
298.       And (Hom_eq (compose C _ _ _ f g) (identity C _))
299.           (Hom_eq (compose C _ _ _ g f) (identity C _))).
300.
301.   Definition Exists {X Y : Ob} (P : Hom X Y -> Type) :=
302.     @Sigma (Hom X Y) P.
303.
304.   Definition ExistsUnique {X Y : Ob} (P : Hom X Y -> Type) :=
305.     And (Exists P)
306.         (forall f f' : Hom X Y,
307.           P f -> P f' -> Hom_eq f f').
308.
309.   Definition Terminal (C : @Category Ob Hom Hom_eq) (T : Ob) :=
310.     forall X, ExistsUnique (fun f : Hom X T => True).
311.
312.   Definition Initial (C : @Category Ob Hom Hom_eq) (T : Ob) :=
313.     forall X, ExistsUnique (fun f : Hom T X => True).
314.
315. End Trinkets.
316.
317. Section OppositeCategory.
318.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
319.
320.   Definition OppositeCategory : @Category C_Ob (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f).
321.   apply (Build_Category
322.     (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f)
323.     (fun X => identity C X)
324.     (fun X Y Z f g => compose C Z Y X g f)).
325.   intros; apply Compose_respectful_right; assumption.
326.   intros; apply Compose_respectful_left; assumption.
327.   intros;
328.     apply Build_Equivalence; destruct (category_equivalence C X Y);
329.       hypothesis.
330.   intros; apply category_right_identity.
331.   intros; apply category_left_identity.
332.   intros.
333.   apply (equivalence_symmetry (category_equivalence C _ _)).
334.   apply category_associativity.
335.   Defined.
336. End OppositeCategory.
337.
338. Section Terminal_Initial_Dual.
339.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
340.   Definition Cop := OppositeCategory C.
341.
342.   Theorem TerminalOp_Initial (L : C_Ob) :
343.     Terminal Cop L -> Initial C L.
344.     unfold Terminal; unfold Initial.
345.     intros f X; destruct (f X) as [[g IPrf] gPrf].
346.     constructor.
347.     apply (witness _ g).
348.     constructor.
349.     apply gPrf.
350.   Defined.
351.
352.   Theorem InitialOp_Terminal (L : C_Ob) :
353.     Initial Cop L -> Terminal C L.
354.     unfold Terminal; unfold Initial.
355.     intros f X; destruct (f X) as [[g IPrf] gPrf].
356.     constructor.
357.     apply (witness _ g).
358.     constructor.
359.     apply gPrf.
360.   Defined.
361.
362. End Terminal_Initial_Dual.
363.
364. Section BijectionSubcategory.
365.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
366.
367.   Definition Bijection (X Y : Ob) := Exists (Isomorphism C X Y).
368.
369.   Definition Invert_Bijection (X Y : Ob) : Bijection X Y -> Bijection Y X.
370.   intros [f [g [p1 p2]]].
371.   apply (witness _ g).
372.   apply (witness _ f).
373.   constructor; assumption.
374.   Defined.
375.
376.   Definition Identity_Bijection (X : Ob) : Bijection X X.
377.   apply (witness _ (identity C X)).
378.   apply (witness _ (identity C X)).
379.   apply And_idem.
380.   apply category_left_identity.
381.   Defined.
382.
383.   Definition Compose_Bijection (X Y Z : Ob)
384.     (f : Bijection X Y) (g : Bijection Y Z) :
385.     Bijection X Z.
386.   unfold Bijection in *.
387.   destruct f as [fTo [fFrom [fPrf fPrf']]].
388.   destruct g as [gTo [gFrom [gPrf gPrf']]].
389.   apply (witness _ (compose C _ _ _ fTo gTo)).
390.   apply (witness _ (compose C _ _ _ gFrom fFrom)).
391.
392.   Lemma Compose_Bijection_Lemma
393.     (X Y Z : Ob)
394.     (fTo : Hom X Y)
395.     (fFrom : Hom Y X)
396.     (fPrf : Hom_eq (compose C X Y X fTo fFrom) (identity C X))
397.     (fPrf' : Hom_eq (compose C Y X Y fFrom fTo) (identity C Y))
398.     (gTo : Hom Y Z)
399.     (gFrom : Hom Z Y)
400.     (gPrf : Hom_eq (compose C Y Z Y gTo gFrom) (identity C Y))
401.       :
402.     (Hom_eq
403.       (compose C X Z X (compose C X Y Z fTo gTo)
404.         (compose C Z Y X gFrom fFrom)) (identity C X)).
405.
406.   pose (@SYNTAX_category Ob Hom) as SYN.
407.   assert (
408.     Syntax_eq
409.      (compose SYN X Z X (compose SYN X Y Z (injSYM _ _ fTo) (injSYM _ _ gTo)) (compose SYN Z Y X (injSYM _ _ gFrom) (injSYM _ _ fFrom)))
410.      (compose SYN _ _ _ (injSYM _ _ fTo)
411.        (compose SYN _ _ _
412.          (compose SYN _ _ _ (injSYM _ _ gTo) (injSYM _ _ gFrom))
413.          (injSYM _ _ fFrom)))
414.   ) as EQUATION by apply identical.
415.   pose (Map_Hom_respectful (Interpret C) _ _ _ _ EQUATION) as EQUATION'; simpl in EQUATION'.
416.
417.   eapply (equivalence_transitivity (category_equivalence C _ _)).
418.   apply EQUATION'.
419.   clear EQUATION'; clear EQUATION.
420.
421.   eapply (equivalence_transitivity (category_equivalence C _ _)).
422.   apply Compose_respectful_right.
423.   apply Compose_respectful_left.
424.   apply gPrf.
425.
426.   eapply (equivalence_transitivity (category_equivalence C _ _)).
427.   apply Compose_respectful_right.
428.   apply category_left_identity.
429.   apply fPrf.
430.   Defined.
431.
432.   apply both; apply Compose_Bijection_Lemma;
433.     assumption.
434.   Defined.
435.
436.   Definition BijectionSubcategory :
437.     @Category Ob Bijection
438.     (fun (X Y : Ob) (f g : Bijection X Y) =>
439.       Hom_eq (pi1 f) (pi1 g)).
440.   apply (Build_Category
441.     Bijection
442.     (fun (X Y : Ob) (f g : Bijection X Y) =>
443.       Hom_eq (pi1 f) (pi1 g))
444.     (fun X => Identity_Bijection X)
445.     (fun X Y Z f g => Compose_Bijection f g)).
446.
447.   intros X Y Z f f' g.
448.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
449.   destruct f' as [f'To [f'From [f'PrfTo f'PrfFrom]]].
450.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
451.   simpl.
452.   apply Compose_respectful_left.
453.
454.   intros X Y Z f f' g.
455.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
456.   destruct f' as [f'To [f'From [f'PrfTo f'PrfFrom]]].
457.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
458.   simpl.
459.   apply Compose_respectful_right.
460.
461.   intros; apply Equivalence_Pullback.
462.   apply (category_equivalence C).
463.
464.   intros X Y.
465.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
466.   simpl.
467.   apply category_left_identity.
468.
469.   intros X Y.
470.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
471.   simpl.
472.   apply category_right_identity.
473.
474.   intros X Y Z W.
475.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
476.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
477.   destruct h as [hTo [hFrom [hPrfTo hPrfFrom]]].
478.   simpl.
479.   apply category_associativity.
480.   Defined.
481.
482.   Definition BijectionSubcategory_Embedding : Functor BijectionSubcategory C.
483.   apply (Build_Functor BijectionSubcategory C
484.     (fun X => X)
485.     (fun X Y f => pi1 f)); simpl; intros.
486.   apply (equivalence_reflexivity (category_equivalence C _ _)).
487.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
488.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
489.   simpl.
490.   apply (equivalence_reflexivity (category_equivalence C _ _)).
491.   assumption.
492.   Defined.
493.
494. End BijectionSubcategory.
495.
496. Section Functors.
497.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
498.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
499.   Context {E_Ob E_Hom E_Hom_eq} (E : @Category E_Ob E_Hom E_Hom_eq).
500.
501.   Definition Constant_Functor (V : C_Ob) : Functor C C.
502.   apply (Build_Functor C C
503.     (fun _ => V)
504.     (fun _ _ _ => identity C V)); intros.
505.   apply (equivalence_reflexivity (category_equivalence C _ _)).
506.   apply (equivalence_symmetry (category_equivalence C _ _)).
507.   apply category_left_identity.
508.   apply (equivalence_reflexivity (category_equivalence C _ _)).
509.   Defined.
510.
511.   Definition Identity_Functor : Functor C C.
512.   apply (Build_Functor C C
513.     (fun X => X)
514.     (fun _ _ f => f)); intros.
515.   apply (equivalence_reflexivity (category_equivalence C _ _)).
516.   apply (equivalence_reflexivity (category_equivalence C _ _)).
517.   assumption.
518.   Defined.
519.
520.   Definition Compose_Functors (F : Functor C D) (G : Functor D E) : Functor C E.
521.   apply (Build_Functor C E
522.     (fun X => Map_Ob G (Map_Ob F X))
523.     (fun _ _ f => Map_Hom G _ _ (Map_Hom F _ _ f))); intros.
524.
525.   apply (equivalence_transitivity (category_equivalence E _ _))
526.     with (y := Map_Hom G _ _ (identity D _)).
527.   apply Map_Hom_respectful.
528.   apply (functor_identity F).
529.   apply (functor_identity G).
530.
531.   apply (equivalence_transitivity (category_equivalence E _ _))
532.     with (y := Map_Hom G _ _ (compose D _ _ _
533.       (Map_Hom F _ _ f) (Map_Hom F _ _ g))).
534.   apply Map_Hom_respectful.
535.   apply (functor_compose F).
536.   apply (functor_compose G).
537.
538.   apply Map_Hom_respectful.
539.   apply Map_Hom_respectful.
540.   assumption.
541.   Defined.
542.
543.   Definition Equal_Functors (F F' : Functor C D) : Type :=
544.     @Sigma (forall X, Exists (Isomorphism D (Map_Ob F X) (Map_Ob F' X)))
545.     (fun iso =>
546.       forall X Y (f : C_Hom X Y),
547.         D_Hom_eq
548.           (compose D _ _ _ (Map_Hom F _ _ f) (pi1 (iso Y)))
549.           (compose D _ _ _ (pi1 (iso X)) (Map_Hom F' _ _ f))).
550.
551.   Theorem Equivalence_Equal_Functors : Equivalence Equal_Functors.
552.     unfold Equal_Functors; apply Build_Equivalence.
553.
554.     intro F; apply (witness _ (fun X => identity (BijectionSubcategory D) (Map_Ob F X))); simpl.
555.     intros X Y f.
556.     eapply (equivalence_transitivity (category_equivalence D _ _)).
557.     apply category_right_identity.
558.     apply (equivalence_symmetry (category_equivalence D _ _)).
559.     apply category_left_identity.
560.
561.     intros F G [a b].
562.     apply (witness _ (fun X => Invert_Bijection (a X))).
563.     intros X Y f.
564.     generalize (b _ _ f).
565.     destruct (a X) as [ax' [ax'' [ax''' ax'''']]].
566.     destruct (a Y) as [ay' [ay'' [ay''' ay'''']]].
567.     simpl.
568.     Lemma eq_functors_lemma1
569.       (F : Functor C D) (G : Functor C D)
570.       (X : C_Ob) (Y : C_Ob) (f : C_Hom X Y)
571.       (ax' : D_Hom (F @ X) (G @ X))
572.       (ax'' : D_Hom (G @ X) (F @ X))
573.       (ax''' : D_Hom_eq (ax' [D] ax'') (Id[D]))
574.       (ax'''' : D_Hom_eq (ax'' [D] ax') (Id[D]))
575.       (ay' : D_Hom (F @ Y) (G @ Y))
576.       (ay'' : D_Hom (G @ Y) (F @ Y))
577.       (ay''' : D_Hom_eq (ay' [D] ay'') (Id[D]))
578.       (ay'''' : D_Hom_eq (ay'' [D] ay') (Id[D])) :
579.       D_Hom_eq ((F \$ X) Y f [D] ay') (ax' [D] (G \$ X) Y f) ->
580.       D_Hom_eq ((G \$ X) Y f [D] ay'') (ax'' [D] (F \$ X) Y f).
582.     apply eq_functors_lemma1; assumption.
583.
584.     intros F G H [fg FG] [gh GH].
585.     apply (witness _ (fun X => compose (BijectionSubcategory D) _ _ _
586.       (fg X) (gh X))); simpl.
587.     intros X Y f.
588.     destruct (fg X) as [fgXF [fgXG [fgXPrf fpXPrf']]].
589.     destruct (gh X) as [ghXF [ghXG [ghXPrf ghXPrf']]].
590.     destruct (fg Y) as [fgYF [fgYG [fgYPrf fpYPrf']]].
591.     destruct (gh Y) as [ghYF [ghYG [ghYPrf ghYPrf']]].
592.     simpl.
593.     Lemma eq_functors_lemma2
594.       (F : Functor C D) (G : Functor C D) (H : Functor C D)
595.       (X : C_Ob) (Y : C_Ob) (f : C_Hom X Y)
596.       (fgXF : D_Hom (F @ X) (G @ X))
597.       (fgXG : D_Hom (G @ X) (F @ X))
598.       (fgXPrf : D_Hom_eq (fgXF [D] fgXG) (Id[D]))
599.       (fpXPrf' : D_Hom_eq (fgXG [D] fgXF) (Id[D]))
600.       (ghXF : D_Hom (G @ X) (H @ X))
601.       (ghXG : D_Hom (H @ X) (G @ X))
602.       (ghXPrf : D_Hom_eq (ghXF [D] ghXG) (Id[D]))
603.       (ghXPrf' : D_Hom_eq (ghXG [D] ghXF) (Id[D]))
604.       (fgYF : D_Hom (F @ Y) (G @ Y))
605.       (fgYG : D_Hom (G @ Y) (F @ Y))
606.       (fgYPrf : D_Hom_eq (fgYF [D] fgYG) (Id[D]))
607.       (fpYPrf' : D_Hom_eq (fgYG [D] fgYF) (Id[D]))
608.       (ghYF : D_Hom (G @ Y) (H @ Y))
609.       (ghYG : D_Hom (H @ Y) (G @ Y))
610.       (ghYPrf : D_Hom_eq (ghYF [D] ghYG) (Id[D]))
611.       (ghYPrf' : D_Hom_eq (ghYG [D] ghYF) (Id[D])) :
612.       D_Hom_eq ((F \$ X) Y f [D] (fgYF [D] ghYF))
613.       ((fgXF [D] ghXF) [D] (H \$ X) Y f).
615.     eapply eq_functors_lemma2; hypothesis.
616.   Defined.
617. End Functors.
618.
619.
620.
621. (*
622. *** Local Variables: ***
623. *** coq-prog-args: ("-emacs-U" "-nois") ***
624. *** End: ***
625. *)
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.
Not a member of Pastebin yet?