• API
• FAQ
• Tools
• Archive
A Pastebin account makes a great Christmas gift
SHARE
TWEET

# Untitled

a guest Jul 7th, 2017 99 Never
ENDING IN00days00hours00mins00secs

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.
293. Section BijectionSubcategory.
294.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
295.
296.   Definition Bijection (X Y : Ob) :=
297.     @Sigma (And (Hom X Y) (Hom Y X))
298.     (fun (fg : And (Hom X Y) (Hom Y X)) =>
299.       match fg with
300.         | both f g =>
301.           And (Hom_eq (compose C _ _ _ f g) (identity C _))
302.               (Hom_eq (compose C _ _ _ g f) (identity C _))
303.         end).
304.
305.   Definition Identity_Bijection (X : Ob) : Bijection X X.
306.   apply (witness _ (both (identity C X) (identity C X))).
307.   apply And_idem.
308.   apply category_left_identity.
309.   Defined.
310.
311.   Definition Compose_Bijection (X Y Z : Ob)
312.     (f : Bijection X Y) (g : Bijection Y Z) :
313.     Bijection X Z.
314.   unfold Bijection in *.
315.   destruct f as [[fTo fFrom] [fPrf fPrf']].
316.   destruct g as [[gTo gFrom] [gPrf gPrf']].
317.   apply (witness _ (both (compose C _ _ _ fTo gTo)
318.                          (compose C _ _ _ gFrom fFrom))).
319.
320.   Lemma Compose_Bijection_Lemma
321.     (X Y Z : Ob)
322.     (fTo : Hom X Y)
323.     (fFrom : Hom Y X)
324.     (fPrf : Hom_eq (compose C X Y X fTo fFrom) (identity C X))
325.     (fPrf' : Hom_eq (compose C Y X Y fFrom fTo) (identity C Y))
326.     (gTo : Hom Y Z)
327.     (gFrom : Hom Z Y)
328.     (gPrf : Hom_eq (compose C Y Z Y gTo gFrom) (identity C Y))
329.       :
330.     (Hom_eq
331.       (compose C X Z X (compose C X Y Z fTo gTo)
332.         (compose C Z Y X gFrom fFrom)) (identity C X)).
333.
334.   pose (@SYNTAX_category Ob Hom) as SYN.
335.   assert (
336.     Syntax_eq
337.      (compose SYN X Z X (compose SYN X Y Z (injSYM _ _ fTo) (injSYM _ _ gTo)) (compose SYN Z Y X (injSYM _ _ gFrom) (injSYM _ _ fFrom)))
338.      (compose SYN _ _ _ (injSYM _ _ fTo)
339.        (compose SYN _ _ _
340.          (compose SYN _ _ _ (injSYM _ _ gTo) (injSYM _ _ gFrom))
341.          (injSYM _ _ fFrom)))
342.   ) as EQUATION by apply identical.
343.   pose (Map_Hom_respectful (Interpret C) _ _ _ _ EQUATION) as EQUATION'; simpl in EQUATION'.
344.
345.   eapply (equivalence_transitivity (category_equivalence C _ _)).
346.   apply EQUATION'.
347.   clear EQUATION'; clear EQUATION.
348.
349.   eapply (equivalence_transitivity (category_equivalence C _ _)).
350.   apply Compose_respectful_right.
351.   apply Compose_respectful_left.
352.   apply gPrf.
353.
354.   eapply (equivalence_transitivity (category_equivalence C _ _)).
355.   apply Compose_respectful_right.
356.   apply category_left_identity.
357.   apply fPrf.
358.   Defined.
359.
360.   apply both; apply Compose_Bijection_Lemma;
361.     assumption.
362.   Defined.
363.
364.   Definition BijectionSubcategory :
365.     @Category Ob Bijection
366.     (fun (X Y : Ob) (f g : Bijection X Y) =>
367.       Hom_eq (proj1 (pi1 f)) (proj1 (pi1 g))).
368.   apply (Build_Category
369.     Bijection
370.     (fun (X Y : Ob) (f g : Bijection X Y) =>
371.       Hom_eq (proj1 (pi1 f)) (proj1 (pi1 g)))
372.     (fun X => Identity_Bijection X)
373.     (fun X Y Z f g => Compose_Bijection f g)
374.     ).
375.
376.   intros X Y Z f f' g.
377.   destruct f as [[fTo fFrom] [fPrfTo fPrfFrom]].
378.   destruct f' as [[f'To f'From] [f'PrfTo f'PrfFrom]].
379.   destruct g as [[gTo gFrom] [gPrfTo gPrfFrom]].
380.   simpl.
381.   apply Compose_respectful_left.
382.
383.   intros X Y Z f f' g.
384.   destruct f as [[fTo fFrom] [fPrfTo fPrfFrom]].
385.   destruct f' as [[f'To f'From] [f'PrfTo f'PrfFrom]].
386.   destruct g as [[gTo gFrom] [gPrfTo gPrfFrom]].
387.   simpl.
388.   apply Compose_respectful_right.
389.
390.   intros; apply Equivalence_Pullback.
391.   apply (category_equivalence C).
392.
393.   intros X Y.
394.   destruct f as [[fTo fFrom] [fPrfTo fPrfFrom]].
395.   simpl.
396.   apply category_left_identity.
397.
398.   intros X Y.
399.   destruct f as [[fTo fFrom] [fPrfTo fPrfFrom]].
400.   simpl.
401.   apply category_right_identity.
402.
403.   intros X Y Z W.
404.   destruct f as [[fTo fFrom] [fPrfTo fPrfFrom]].
405.   destruct g as [[gTo gFrom] [gPrfTo gPrfFrom]].
406.   destruct h as [[hTo hFrom] [hPrfTo hPrfFrom]].
407.   simpl.
408.   apply category_associativity.
409.   Defined.
410.
411.   Definition BijectionSubcategory_Embedding : Functor BijectionSubcategory C.
412.   apply (Build_Functor BijectionSubcategory C
413.     (fun X => X)
414.     (fun X Y f => proj1 (pi1 f))); simpl; intros.
415.   apply (equivalence_reflexivity (category_equivalence C _ _)).
416.   destruct f as [[fTo fFrom] [fPrfTo fPrfFrom]].
417.   destruct g as [[gTo gFrom] [gPrfTo gPrfFrom]].
418.   simpl.
419.   apply (equivalence_reflexivity (category_equivalence C _ _)).
420.   assumption.
421.   Defined.
422.
423. End BijectionSubcategory.
424.
425. Section OppositeCategory.
426.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
427.
428.   Definition OppositeCategory : @Category C_Ob (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f).
429.   apply (Build_Category
430.     (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f)
431.     (fun X => identity C X)
432.     (fun X Y Z f g => compose C Z Y X g f)).
433.   intros; apply Compose_respectful_right; assumption.
434.   intros; apply Compose_respectful_left; assumption.
435.   intros;
436.     apply Build_Equivalence; destruct (category_equivalence C X Y);
437.       hypothesis.
438.   intros; apply category_right_identity.
439.   intros; apply category_left_identity.
440.   intros.
441.   apply (equivalence_symmetry (category_equivalence C _ _)).
442.   apply category_associativity.
443.   Defined.
444. End OppositeCategory.
445.
446. Section Trinkets.
447.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
448.
449.   Definition Isomorphism (X Y : Ob) (f : Hom X Y) :=
450.     @Sigma (Hom Y X)
451.     (fun (g : Hom Y X) =>
452.       And (Hom_eq (compose C _ _ _ f g) (identity C _))
453.           (Hom_eq (compose C _ _ _ g f) (identity C _))).
454.
455.   Theorem Bijection_to_Isomorphism {X Y} (f : Bijection C X Y) : Isomorphism (proj1 (pi1 f)).
456.     destruct f as [[to from] [toPrf fromPrf]]; simpl.
457.     apply (witness _ from).
458.     constructor; assumption.
459.   Defined.
460.
461.   Theorem Isomorphism_to_Bijection {X Y} (f : Hom X Y) : Isomorphism f -> Bijection C X Y.
462.     intros [g [fPrf gPrf]].
463.     apply (witness _ (both f g)).
464.     constructor; assumption.
465.   Defined.
466.
467.   Theorem Identity_Isomorphism (X : Ob) : Isomorphism (identity C X).
468.     apply (Bijection_to_Isomorphism (identity (BijectionSubcategory C) X)).
469.   Defined.
470.
471.   Theorem Compose_Isomorphisms (X Y Z : Ob) (f : Hom X Y) (g : Hom Y Z) : Isomorphism f -> Isomorphism g -> Isomorphism (compose C _ _ _ f g).
472.     intros F G.
473.     pose (Bijection_to_Isomorphism (compose (BijectionSubcategory C)
474.       _ _ _
475.       (Isomorphism_to_Bijection F)
476.       (Isomorphism_to_Bijection G))) as i.
477.     destruct F as [f' [fPrf f'Prf]];
478.     destruct G as [g' [gPrf g'Prf]];
479.     simpl in *.
480.     apply i.
481.   Defined.
482.
483.   Definition Exists {X Y : Ob} (P : Hom X Y -> Type) :=
484.     @Sigma (Hom X Y) P.
485.
486.   Definition ExistsUnique {X Y : Ob} (P : Hom X Y -> Type) :=
487.     And (Exists P)
488.         (forall f f' : Hom X Y,
489.           P f -> P f' -> Hom_eq f f').
490.
491.   Definition Terminal (C : @Category Ob Hom Hom_eq) (T : Ob) :=
492.     forall X, ExistsUnique (fun f : Hom X T => True).
493.
494.   Definition Initial (C : @Category Ob Hom Hom_eq) (T : Ob) :=
495.     forall X, ExistsUnique (fun f : Hom T X => True).
496.
497. End Trinkets.
498.
499. Section Terminal_Initial_Dual.
500.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
501.   Definition Cop := OppositeCategory C.
502.
503.   Theorem TerminalOp_Initial (L : C_Ob) :
504.     Terminal Cop L -> Initial C L.
505.     unfold Terminal; unfold Initial.
506.     intros f X; destruct (f X) as [[g IPrf] gPrf].
507.     constructor.
508.     apply (witness _ g).
509.     constructor.
510.     apply gPrf.
511.   Defined.
512.
513.   Theorem InitialOp_Terminal (L : C_Ob) :
514.     Initial Cop L -> Terminal C L.
515.     unfold Terminal; unfold Initial.
516.     intros f X; destruct (f X) as [[g IPrf] gPrf].
517.     constructor.
518.     apply (witness _ g).
519.     constructor.
520.     apply gPrf.
521.   Defined.
522.
523. End Terminal_Initial_Dual.
524.
525. Section Functors.
526.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
527.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
528.   Context {E_Ob E_Hom E_Hom_eq} (E : @Category E_Ob E_Hom E_Hom_eq).
529.
530.   Definition Constant_Functor (V : C_Ob) : Functor C C.
531.   apply (Build_Functor C C
532.     (fun _ => V)
533.     (fun _ _ _ => identity C V)); intros.
534.   apply (equivalence_reflexivity (category_equivalence C _ _)).
535.   apply (equivalence_symmetry (category_equivalence C _ _)).
536.   apply category_left_identity.
537.   apply (equivalence_reflexivity (category_equivalence C _ _)).
538.   Defined.
539.
540.   Definition Identity_Functor : Functor C C.
541.   apply (Build_Functor C C
542.     (fun X => X)
543.     (fun _ _ f => f)); intros.
544.   apply (equivalence_reflexivity (category_equivalence C _ _)).
545.   apply (equivalence_reflexivity (category_equivalence C _ _)).
546.   assumption.
547.   Defined.
548.
549.   Definition Compose_Functors (F : Functor C D) (G : Functor D E) : Functor C E.
550.   apply (Build_Functor C E
551.     (fun X => Map_Ob G (Map_Ob F X))
552.     (fun _ _ f => Map_Hom G _ _ (Map_Hom F _ _ f))); intros.
553.
554.   apply (equivalence_transitivity (category_equivalence E _ _))
555.     with (y := Map_Hom G _ _ (identity D _)).
556.   apply Map_Hom_respectful.
557.   apply (functor_identity F).
558.   apply (functor_identity G).
559.
560.   apply (equivalence_transitivity (category_equivalence E _ _))
561.     with (y := Map_Hom G _ _ (compose D _ _ _
562.       (Map_Hom F _ _ f) (Map_Hom F _ _ g))).
563.   apply Map_Hom_respectful.
564.   apply (functor_compose F).
565.   apply (functor_compose G).
566.
567.   apply Map_Hom_respectful.
568.   apply Map_Hom_respectful.
569.   assumption.
570.   Defined.
571.
572.   Definition Equal_Functors (F F' : Functor C D) : Type :=
573.     @Sigma (forall X, Exists (Isomorphism D (Map_Ob F X) (Map_Ob F' X)))
574.     (fun iso =>
575.       forall X Y (f : C_Hom X Y),
576.         D_Hom_eq
577.           (compose D _ _ _ (Map_Hom F _ _ f) (pi1 (iso Y)))
578.           (compose D _ _ _ (pi1 (iso X)) (Map_Hom F' _ _ f))).
579.
580.   Theorem Equivalence_Equal_Functors : Equivalence Equal_Functors.
581.   apply Build_Equivalence.
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