Need a unique gift idea?
A Pastebin account makes a great Christmas gift
SHARE
TWEET

Untitled

a guest Jul 6th, 2017 80 Never
Upgrade to PRO!
ENDING IN00days00hours00mins00secs
 
  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].
  471. Admitted.
  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)).
  488. Admitted.
  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. OK, I Understand
 
Top