API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Jul 7th, 2017
129
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
OCaml Brief 24.42 KB | None | 0 0
raw download clone embed print report
  1. Set Implicit Arguments.
  2.  
  3. Ltac hypothesis := match goal with [ H : _ |- _ ] => apply H end.
  4.  
  5. Inductive False : Type :=.
  6.  
  7. Definition Not (P : Type) := P -> False.
  8.  
  9. Inductive True : Type :=
  10. | I : True.
  11.  
  12. Inductive Identity (T : Type) (t : T) : T -> Type :=
  13. | identical : Identity t t.
  14.  
  15. Inductive And (P Q : Type) : Type :=
  16. | both : P -> Q -> And P Q.
  17.  
  18. Inductive Or (P Q : Type) : Type :=
  19. | inleft : P -> Or P Q
  20. | inright : Q -> Or P Q.
  21.  
  22. Definition Decidible (P : Type) := Or P (Not P).
  23.  
  24. Definition And_idem (P : Type) : P -> And P P.
  25. intro p; apply (both p p).
  26. Defined.
  27.  
  28. Inductive Sigma (T : Type) (P : T -> Type) : Type :=
  29. | witness : forall t : T, P t -> Sigma P.
  30.  
  31. Definition Relation (T : Type) := T -> T -> Type.
  32.  
  33. Record Equivalence {T : Type} (R : Relation T)
  34.   := { equivalence_reflexivity : forall x, R x x
  35.      ; equivalence_symmetry : forall x y, R x y -> R y x
  36.      ; equivalence_transitivity : forall x y z, R x y -> R y z -> R x z
  37.      }.
  38.  
  39. Theorem Equivalence_Identity {T : Type} : Equivalence (@Identity T).
  40. apply Build_Equivalence.
  41. intros; constructor.
  42. intros; elim H; constructor.
  43. intros; elim H0; elim H; constructor.
  44. Defined.
  45.  
  46. Record Category (Ob : Type) (Hom : Ob -> Ob -> Type)
  47.                 (Hom_eq : forall X Y, Relation (Hom X Y))
  48.   := { identity : forall X, Hom X X
  49.      ; compose : forall X Y Z, Hom X Y -> Hom Y Z -> Hom X Z
  50.      ; compose_respectful_left : forall X Y Z (f f' : Hom X Y) (g : Hom Y Z),
  51.        Hom_eq _ _ f f' -> Hom_eq _ _ (compose f g) (compose f' g)
  52.      ; compose_respectful_right : forall X Y Z (f : Hom X Y) (g g' : Hom Y Z),
  53.        Hom_eq _ _ g g' -> Hom_eq _ _ (compose f g) (compose f g')
  54.      ; hom_equivalence : forall X Y, Equivalence (Hom_eq X Y)
  55.      ; category_left_identity : forall X Y (f : Hom X Y),
  56.        Hom_eq _ _ (compose (identity _) f) f
  57.      ; category_right_identity : forall X Y (f : Hom X Y),
  58.        Hom_eq _ _ (compose f (identity _)) f
  59.      ; category_associativity : forall X Y Z W (f : Hom X Y) (g : Hom Y Z) (h : Hom Z W),
  60.        Hom_eq _ _ (compose f (compose g h))
  61.                   (compose (compose f g) h)
  62.      }.
  63.  
  64. Notation "f '[' C ']'  g" := (compose C _ _ _ f g) (at level 20).
  65. Notation "'1_' C" := (identity C _) (at level 20).
  66.  
  67. Ltac refl :=
  68.   eapply equivalence_reflexivity;
  69.     [apply hom_equivalence;assumption].
  70. Ltac symm :=
  71.   eapply equivalence_symmetry;
  72.     [apply hom_equivalence;assumption|idtac].
  73. Ltac trans :=
  74.   eapply equivalence_transitivity;
  75.     [apply hom_equivalence;assumption|idtac|idtac].
  76.  
  77. Section Isomorphism.
  78.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  79.  
  80.   Definition Isomorphism (X Y : C_Ob) :=
  81.     @Sigma (And (C_Hom X Y) (C_Hom Y X))
  82.            (fun fg =>
  83.              match fg with
  84.                | both f g =>
  85.                  And (C_Hom_eq (compose C _ _ _ g f) (identity C _))
  86.                      (C_Hom_eq (compose C _ _ _ f g) (identity C _))
  87.              end).
  88.  
  89.   Definition isomorphism_to (X Y : C_Ob) (i : Isomorphism X Y) : C_Hom X Y.
  90.   destruct i as [[to from] _]; apply to.
  91.   Defined.
  92.  
  93.   Definition isomorphism_from (X Y : C_Ob) (i : Isomorphism X Y) : C_Hom Y X.
  94.   destruct i as [[to from] _]; apply from.
  95.   Defined.
  96.  
  97.   Theorem Isomorphism_Equivalence : Equivalence Isomorphism.
  98.   apply Build_Equivalence.
  99.  
  100.   Lemma Isomorphism_Identity : forall x : C_Ob, Isomorphism x x.
  101.     intro x; apply (witness _ (both (identity C x) (identity C x))).
  102.     apply And_idem.
  103.     apply category_left_identity.
  104.   Defined.
  105.   apply Isomorphism_Identity.
  106.  
  107.   intros x y [[I J] [i j]].
  108.   apply (witness _ (both J I)).
  109.   apply (both j i).
  110.  
  111.   Lemma Isomorphism_Compose : forall x y z : C_Ob, Isomorphism x y -> Isomorphism y z -> Isomorphism x z.
  112.     intros x y z [[I J] [i j]] [[I' J'] [i' j']].
  113.     apply (witness _ (both (compose C _ _ _ I I') (compose C _ _ _ J' J))).
  114.     apply both.
  115.    
  116.     trans.
  117.     apply (category_associativity C).
  118.     trans.
  119.     apply (compose_respectful_left C).
  120.     trans.
  121.     symm.
  122.     apply (category_associativity C).
  123.     apply (compose_respectful_right C).
  124.     apply i.
  125.     assert (C_Hom_eq (compose C z y y J' (identity C y))
  126.                      J').
  127.     apply category_right_identity.
  128.     trans.
  129.     apply (compose_respectful_left C).
  130.     apply X.
  131.     assumption.
  132.    
  133.     trans.
  134.     apply (category_associativity C).
  135.     trans.
  136.     apply (compose_respectful_left C).
  137.     trans.
  138.     symm.
  139.     apply (category_associativity C).
  140.     apply (compose_respectful_right C).
  141.     apply j'.
  142.     assert (C_Hom_eq (compose C x y y I (identity C y))
  143.                      I).
  144.     apply category_right_identity.
  145.     trans.
  146.     apply (compose_respectful_left C).
  147.     apply X.
  148.     assumption.
  149.     Defined.
  150.   apply Isomorphism_Compose.
  151.   Defined.
  152. End Isomorphism.
  153.  
  154. Section Functor.
  155.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  156.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  157.  
  158.   Record Functor
  159.     := { Map_Ob : C_Ob -> D_Ob
  160.        ; Map_Hom : forall X Y, C_Hom X Y -> D_Hom (Map_Ob X) (Map_Ob Y)
  161.        ; functor_identity : forall X, D_Hom_eq (Map_Hom (identity C X)) (identity D (Map_Ob X))
  162.        ; functor_compose : forall X Y Z (f : C_Hom X Y) (g : C_Hom Y Z),
  163.          D_Hom_eq (Map_Hom (compose C _ _ _ f g)) (compose D _ _ _ (Map_Hom f) (Map_Hom g))
  164.        ; Map_Hom_respectful : forall X Y (f f' : C_Hom X Y),
  165.          C_Hom_eq f f' -> D_Hom_eq (Map_Hom f) (Map_Hom f')
  166.     }.
  167.  
  168.   Notation "F '@' x" := (Map_Ob F x) (at level 20).
  169.   Notation "F '$' f" := (Map_Hom F f) (at level 20).
  170.  
  171.   Definition Functor_equality (F G : Functor) :=
  172.     @Sigma (forall X : C_Ob,
  173.              Isomorphism D (Map_Ob F X) (Map_Ob G X))
  174.           (fun Ob_iso =>
  175.             forall X Y (f : C_Hom X Y),
  176.               D_Hom_eq (Map_Hom F f)
  177.                        (compose D _ _ _
  178.                          (isomorphism_to (Ob_iso _))
  179.                          (compose D _ _ _
  180.                            (Map_Hom G f)
  181.                             (isomorphism_from (Ob_iso _))))).
  182.  
  183.   Theorem Functor_equivalence : Equivalence Functor_equality.
  184.     apply Build_Equivalence.
  185.    
  186.     intro x.
  187.     unfold Functor_equality.
  188.     apply witness with (t := (fun X => @Isomorphism_Identity _ _ _ D (Map_Ob x X))).
  189.     intros X Y f.
  190.     simpl.
  191.     trans.
  192.     symm.
  193.     apply category_left_identity.
  194.     apply compose_respectful_right.
  195.     trans.
  196.     symm.
  197.     apply category_right_identity.
  198.     apply compose_respectful_right.
  199.     refl.
  200.    
  201.     intros F G.
  202.     intros [F' F''].
  203.    
  204.     pose (Isomorphism_Equivalence D).
  205.     pose (match e with
  206.             | Build_Equivalence _ Isymm _ => Isymm
  207.           end) as Isymm.
  208.     unfold Functor_equality.
  209.     apply (witness _ (fun X => Isymm _ _ (F' X))).
  210.     intros X Y f.
  211.     unfold Isymm in *; unfold e in *; simpl.
  212.     generalize (F'' _ _ f).
  213.    
  214.     destruct (F' X); simpl.
  215.     destruct t; simpl.
  216.     destruct y; simpl.
  217.     destruct (F' Y); simpl.
  218.     destruct t; simpl.
  219.     destruct y; simpl.
  220.    
  221.     intro.
  222.     assert (
  223.       D_Hom_eq (compose D _ _ _ d0 (compose D _ _ _ (Map_Hom F f) d3))
  224.       (compose D _ _ _ d0 (compose D _ _ _
  225.         (compose D (Map_Ob F X) (Map_Ob G X) (Map_Ob F Y) d
  226.             (compose D (Map_Ob G X) (Map_Ob G Y) (Map_Ob F Y)
  227.                (Map_Hom G f) d4)) d3))
  228.       ).
  229.     apply compose_respectful_right.
  230.     apply compose_respectful_left.
  231.     assumption.
  232.    
  233.     trans.
  234.     Focus 2.
  235.     symm.
  236.     apply X1.
  237.     (* Gf = (d0 ((d (Gf d4)) d3)) *)
  238.     Lemma YUK
  239.       (F : Functor)
  240.       (G : Functor)
  241.       (X : C_Ob)
  242.       (Y : C_Ob)
  243.       (f : C_Hom X Y)
  244.       (d : D_Hom (F @ X) (G @ X))
  245.       (d0 : D_Hom (G @ X) (F @ X))
  246.       (d1 : D_Hom_eq (d0 [D] d) (identity D _))
  247.       (d2 : D_Hom_eq (d [D] d0) (identity D _))
  248.       (d3 : D_Hom (F @ Y) (G @ Y))
  249.       (d4 : D_Hom (G @ Y) (F @ Y))
  250.       (d5 : D_Hom_eq (d4 [D] d3) (identity D _))
  251.       (d6 : D_Hom_eq (d3 [D] d4) (identity D _))
  252.       (X0 : D_Hom_eq (F $ f) (d [D] ((G $ f) [D] d4)))
  253.       (X1 : D_Hom_eq (d0 [D] ((F $ f) [D] d3))
  254.              (d0 [D] ((d [D] ((G $ f) [D] d4)) [D] d3))) :
  255.       D_Hom_eq (G $ f) (d0 [D] ((d [D] ((G $ f) [D] d4)) [D] d3)).
  256.      
  257.       cut (D_Hom_eq (G $ f) ((G $ f) [D] (identity D _))).
  258.       cut (D_Hom_eq ((G $ f) [D] (identity D _)) ((G $ f) [D] (d4 [D] d3))).
  259.       cut (D_Hom_eq ((G $ f) [D] (d4 [D] d3)) ((identity D _) [D] ((G $ f) [D] (d4 [D] d3)))).
  260.       cut (D_Hom_eq ((identity D _) [D] ((G $ f) [D] (d4 [D] d3))) ((d0 [D] d) [D] ((G $ f) [D] (d4 [D] d3)))).
  261.       cut (D_Hom_eq ((d0 [D] d) [D] ((G $ f) [D] (d4 [D] d3))) (d0 [D] (d [D] ((G $ f) [D] (d4 [D] d3))))).
  262.       cut (D_Hom_eq (d0 [D] (d [D] ((G $ f) [D] (d4 [D] d3)))) (d0 [D] (d [D] (((G $ f) [D] d4) [D] d3)))).
  263.       cut (D_Hom_eq (d0 [D] (d [D] (((G $ f) [D] d4) [D] d3))) (d0 [D] ((d [D] ((G $ f) [D] d4)) [D] d3))).
  264.       intros.
  265.      
  266.       do 7 (trans;[hypothesis|]); refl.
  267.      
  268.       apply compose_respectful_right.
  269.       apply (category_associativity D _ _ _ _ d ((G $ f) [D] d4) d3).
  270.      
  271.       do 2 apply compose_respectful_right.
  272.       apply category_associativity.
  273.      
  274.       symm; apply category_associativity.
  275.      
  276.       apply compose_respectful_left.
  277.       symm; assumption.
  278.      
  279.       symm; apply category_left_identity.
  280.      
  281.       apply compose_respectful_right.
  282.       symm; assumption.
  283.    
  284.       symm; apply category_right_identity.
  285.     Defined.
  286.     apply YUK; assumption.
  287.    
  288.     intros x y z F G; unfold Functor_equality.
  289.     destruct F.
  290.     destruct G.
  291.     pose (Isomorphism_Equivalence D).
  292.     pose (match e with
  293.             | Build_Equivalence _ _ Itrans => Itrans
  294.           end) as Itrans.
  295.     unfold Functor_equality.
  296.     apply (witness _ (fun X => Itrans _ _ _ (t X) (t0 X))).
  297.     intros; simpl.
  298.    
  299.     generalize (d X Y f).
  300.     generalize (d0 X Y f).
  301.    
  302.     destruct (t X); simpl.
  303.     destruct t1; destruct y0; simpl.
  304.     destruct (t0 X); simpl.
  305.     destruct t1; destruct y0; simpl.
  306.     simpl.
  307.     destruct (t Y); simpl.
  308.     destruct t1; destruct y0; simpl.
  309.     destruct (t0 Y); simpl.
  310.     destruct t1; destruct y0; simpl.
  311.     simpl.
  312.     (* Xf = ((d1 d5)(Zf (d14 d10))) *)
  313.    
  314.     Lemma BLECH
  315.       (F : Functor)
  316.       (G : Functor)
  317.       (H : Functor)
  318.       (X : C_Ob)
  319.       (Y : C_Ob)
  320.       (f : C_Hom X Y)
  321.       (d1 : D_Hom (F @ X) (G @ X))
  322.       (d2 : D_Hom (G @ X) (F @ X))
  323.       (d3 : D_Hom_eq (d2 [D] d1) (identity D _))
  324.       (d4 : D_Hom_eq (d1 [D] d2) (identity D _))
  325.       (d5 : D_Hom (G @ X) (H @ X))
  326.       (d6 : D_Hom (H @ X) (G @ X))
  327.       (d7 : D_Hom_eq (d6 [D] d5) (identity D _))
  328.       (d8 : D_Hom_eq (d5 [D] d6) (identity D _))
  329.       (d9 : D_Hom (F @ Y) (G @ Y))
  330.       (d10 : D_Hom (G @ Y) (F @ Y))
  331.       (d11 : D_Hom_eq (d10 [D] d9) (identity D _))
  332.       (d12 : D_Hom_eq (d9 [D] d10) (identity D _))
  333.       (d13 : D_Hom (G @ Y) (H @ Y))
  334.       (d14 : D_Hom (H @ Y) (G @ Y))
  335.       (d15 : D_Hom_eq (d14 [D] d13) (identity D _))
  336.       (d16 : D_Hom_eq (d13 [D] d14) (identity D _))
  337.     (WW : D_Hom_eq (F $ f) (d1 [D] ((G $ f) [D] d10)))
  338.     (MM : D_Hom_eq (G $ f) (d5 [D] ((H $ f) [D] d14))) :
  339.    D_Hom_eq (F $ f) ((d1 [D] d5) [D] ((H $ f) [D] (d14 [D] d10))).
  340.       symm.
  341.       cut (D_Hom_eq
  342.         (G $ f)
  343.         (d5 [D] ((H $ f) [D] d14))).
  344.       cut (D_Hom_eq
  345.         (F $ f)
  346.         (d1 [D] ((G $ f) [D] d10))).
  347.       intros.
  348.      
  349.       Ltac step K :=
  350.         match goal with |- D_Hom_eq ?X ?Y =>
  351.           cut (D_Hom_eq X K);[intro;trans;hypothesis|]
  352.         end.
  353.      
  354.       step (((d1 [D] d5) [D] (((H $ f) [D] d14) [D] d10))).
  355.       step ((d1 [D] (d5 [D] (((H $ f) [D] d14) [D] d10)))).
  356.       match goal with |- D_Hom_eq ?X ?y =>
  357.         cut (D_Hom_eq X ((d1 [D] ((d5 [D] ((H $ f) [D] d14)) [D] d10))))
  358.       end.
  359.       intro.
  360.       trans.
  361.       apply X4.
  362.      
  363.       match goal with |- D_Hom_eq ?X ?y =>
  364.         cut (D_Hom_eq X (d1 [D] ((G $ f) [D] d10)))
  365.       end.
  366.       intro; trans.
  367.       apply X5.
  368.      
  369.       apply compose_respectful_right.
  370.       trans.
  371.       apply compose_respectful_left.
  372.       apply X1.
  373.       symm.
  374.       apply (category_associativity D _ _ _ _ d5 ((H $ f) [D] d14) d10).
  375.      
  376.       apply compose_respectful_right.
  377.       apply compose_respectful_left.
  378.       symm; hypothesis.
  379.      
  380.       step ((d1 [D] (d5 [D] (((H $ f) [D] d14) [D] d10)))).
  381.      
  382.       apply (category_associativity D _ _ _ _).
  383.       symm; apply (category_associativity D _ _ _ _).
  384.       trans; [apply X0|].
  385.       apply compose_respectful_right.
  386.       symm.
  387.       step (((d5 [D] ((H $ f) [D] d14)) [D] d10)).
  388.       symm; assumption.
  389.       apply (category_associativity D _ _ _ _ d5).
  390.       apply compose_respectful_right.
  391.       apply (category_associativity D _ _ _ _).
  392.      
  393.       assumption.
  394.    
  395.       assumption.
  396.    
  397.     Defined.
  398.     intros.
  399.     eapply BLECH; hypothesis.
  400.   Defined.
  401. End Functor.
  402.  
  403. Section Functors.
  404.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  405.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  406.   Context {E_Ob E_Hom E_Hom_eq} (E : @Category E_Ob E_Hom E_Hom_eq).
  407.  
  408.   Theorem Functor_Equal (F : Functor C D) {X Y} (f f' : C_Hom X Y) : C_Hom_eq f f' -> D_Hom_eq (Map_Hom F _ _ f) (Map_Hom F _ _ f').
  409.   intros; apply Map_Hom_respectful.
  410.   assumption.
  411.   Defined.
  412.  
  413.   Definition Identity_Functor : Functor C C.
  414.   Print Build_Functor.
  415.   apply (Build_Functor C C
  416.     (fun X => X)
  417.     (fun X Y f => f)).
  418.   intros; refl.
  419.   intros; refl.
  420.   intros; assumption.
  421.   Defined.
  422.  
  423.   Definition Compose_Functor (F : Functor C D) (G : Functor D E) : Functor C E.
  424.   Print Build_Functor.
  425.   apply (Build_Functor C E
  426.     (fun X => Map_Ob G (Map_Ob F X))
  427.     (fun X Y f => Map_Hom G _ _ (Map_Hom F _ _ f))).
  428.  
  429.   intros.
  430.   trans.
  431.   apply Map_Hom_respectful.
  432.   apply (functor_identity F X).
  433.   apply (functor_identity G _).
  434.  
  435.   intros.
  436.   trans.
  437.   apply Map_Hom_respectful.
  438.   apply (functor_compose F).
  439.   apply (functor_compose G).
  440.  
  441.   intros.
  442.   apply Map_Hom_respectful.
  443.   apply Map_Hom_respectful.
  444.   assumption.
  445.   Defined.
  446. End Functors.
  447.  
  448. Section NaturalTransformation.
  449.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  450.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  451.  
  452.   Context (F G : Functor C D).
  453.  
  454.   Record NaturalTransformation
  455.     := { Component : forall X : C_Ob, D_Hom (Map_Ob F X) (Map_Ob G X)
  456.        ; naturality : forall X Y (f : C_Hom X Y),
  457.          D_Hom_eq (compose D _ _ _ (Map_Hom F _ _ f) (Component Y))
  458.                   (compose D _ _ _ (Component X) (Map_Hom G _ _ f))
  459.        }.
  460. End NaturalTransformation.
  461.  
  462. Section NaturalTransformations.
  463.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  464.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  465.  
  466.   Context (F G H : Functor C D).
  467.  
  468.   Print Component.
  469.   Definition NaturalTransformation_Equivalence : Equivalence (fun (eta nu : NaturalTransformation F G) => forall X : C_Ob, D_Hom_eq (Component eta X) (Component nu X)).
  470.   apply Build_Equivalence.
  471.  
  472.   intros; refl.
  473.  
  474.   intros; symm; hypothesis.
  475.  
  476.   intros; trans; hypothesis.
  477.   Defined.
  478.  
  479.   Definition Identity_NaturalTransformation : NaturalTransformation F F.
  480.   apply (Build_NaturalTransformation F F
  481.     (fun X => identity D (Map_Ob F X))).
  482.   intros; trans.
  483.   apply category_right_identity.
  484.   symm; apply category_left_identity.
  485.   Defined.
  486.  
  487.   Definition Compose_NaturalTransformation (eta : NaturalTransformation F G) (nu : NaturalTransformation G H) : NaturalTransformation F H.
  488.   apply (Build_NaturalTransformation F H
  489.     (fun X => compose D _ _ _ (Component eta X) (Component nu X))).
  490.   intros.
  491.   trans.
  492.   apply (category_associativity D).
  493.   trans.
  494.   apply (compose_respectful_left D).
  495.   apply (naturality eta).
  496.   trans.
  497.   symm; apply (category_associativity D).
  498.   symm.
  499.   trans.
  500.   symm.
  501.   apply (category_associativity D).
  502.   apply (compose_respectful_right D).
  503.   symm.
  504.   apply (naturality nu).
  505.   Defined.
  506. End NaturalTransformations.
  507.  
  508.  
  509. Section FunctorCategory.
  510.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  511.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  512.   Definition FunctorCategory : @Category
  513.     (Functor C D) (fun F G => NaturalTransformation F G)
  514.     (fun F G =>
  515.       fun (eta nu : NaturalTransformation F G) =>
  516.         forall X : C_Ob,
  517.           D_Hom_eq (Component eta X) (Component nu X)).
  518.   Print Build_Category.
  519.   Print Identity_NaturalTransformation.
  520.   apply (@Build_Category
  521.    
  522.     (Functor C D)
  523.     (fun F G => NaturalTransformation F G)
  524.     (fun F G =>
  525.       fun (eta nu : NaturalTransformation F G) =>
  526.         forall X : C_Ob,
  527.           D_Hom_eq (Component eta X) (Component nu X))
  528.    
  529.     (fun F => Identity_NaturalTransformation F)
  530.     (fun _ _ _ eta nu => Compose_NaturalTransformation eta nu));
  531.   simpl; intros.
  532.  
  533.   apply compose_respectful_left.
  534.   hypothesis.
  535.  
  536.   apply compose_respectful_right.
  537.   hypothesis.
  538.  
  539.   apply NaturalTransformation_Equivalence.
  540.  
  541.   apply category_left_identity.
  542.  
  543.   apply category_right_identity.
  544.  
  545.   apply category_associativity.
  546.   Defined.
  547. End FunctorCategory.
  548.  
  549. Section OppositeCategory.
  550.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  551.  
  552.   Definition OppositeCategory : @Category C_Ob (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f).
  553.   apply (Build_Category
  554.     (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f)
  555.     (fun X => identity C X)
  556.     (fun X Y Z f g => compose C Z Y X g f)).
  557.   intros; apply compose_respectful_right; hypothesis.
  558.   intros; apply compose_respectful_left; hypothesis.
  559.   intros;
  560.     apply Build_Equivalence; destruct (hom_equivalence C X Y);
  561.       hypothesis.
  562.   intros; apply category_right_identity.
  563.   intros; apply category_left_identity.
  564.   intros; symm; apply category_associativity.
  565.   Defined.
  566. End OppositeCategory.
  567.  
  568. Section UniqueExistence.
  569.   Context {C_Ob : Type}
  570.           {C_Hom : C_Ob -> C_Ob -> Type}
  571.           {C_Hom_eq : forall X Y, Relation (C_Hom X Y)}.
  572.  
  573.   Definition ExistsUnique {X Y} (C : @Category C_Ob C_Hom C_Hom_eq) (P : C_Hom X Y -> Type) :=
  574.     Sigma (fun f =>
  575.       And (P f) (forall f' : C_Hom X Y, P f' -> C_Hom_eq f f')).
  576. End UniqueExistence.
  577.  
  578. Section TerminalObject.
  579.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  580.  
  581.   Definition Terminal (T : C_Ob) :=
  582.     forall X, ExistsUnique C (fun (f : C_Hom X T) => True).
  583.  
  584.   (** TODO: unique up to unique isomorphism,
  585.      needs predicative definition of isomorphism **)
  586.   Theorem Terminal_unique (T T' : C_Ob) :
  587.     Terminal T -> Terminal T' -> Isomorphism C T T'.
  588.   unfold Terminal; unfold Isomorphism; intros.
  589.   pose (X T); pose (X T').
  590.   pose (X0 T); pose (X0 T').
  591.   destruct e; destruct e0; destruct e1; destruct e2.
  592.   apply (witness _ (both t1 t0)).
  593.   destruct a; destruct a2.
  594.   pose (c (t1 [C] t0) I).
  595.   pose (c0 (t0 [C] t1) I).
  596.   pose (c (identity C _) I).
  597.   pose (c0 (identity C _) I).
  598.   constructor.
  599.   trans; [symm|]; hypothesis.
  600.   trans; [symm|]; hypothesis.
  601.   Defined.
  602.  
  603. End TerminalObject.
  604.  
  605. Section ConstantFunctor.
  606.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  607.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  608.  
  609.   Definition Delta (U : D_Ob) : Functor C D.
  610.   apply (Build_Functor C D
  611.     (fun _ => U)
  612.     (fun _ _ _ => identity D U)).
  613.   intro; refl.
  614.   intros; symm; apply category_left_identity.
  615.   intros; refl.
  616.   Defined.
  617. End ConstantFunctor.
  618.  
  619. Section Cone.
  620.   Context {II_Ob II_Hom II_Hom_eq} (II : @Category II_Ob II_Hom II_Hom_eq).
  621.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  622.  
  623.   Definition Cone (U : C_Ob) (D : Functor II C) := NaturalTransformation (Delta II C U) D.
  624. End Cone.
  625.  
  626.  
  627.  
  628.  
  629. Section SYMBOLIC.
  630.  
  631.   Inductive SYMBOLIC_Objects := a'' | b'' | c'' | d'' | e''.
  632.   Inductive SYMBOLIC_Morphisms : SYMBOLIC_Objects -> SYMBOLIC_Objects -> Type :=
  633.   | f'' : SYMBOLIC_Morphisms a'' b''
  634.   | g'' : SYMBOLIC_Morphisms b'' c''
  635.   | h'' : SYMBOLIC_Morphisms c'' d''
  636.   | k'' : SYMBOLIC_Morphisms d'' e''.
  637.  
  638.   Inductive SYMBOLIC_Closure : SYMBOLIC_Objects -> SYMBOLIC_Objects -> Type :=
  639.   | SYMBOLIC_Identity : forall x, SYMBOLIC_Closure x x
  640.   | SYMBOLIC_Cons : forall x y z, SYMBOLIC_Morphisms x y -> SYMBOLIC_Closure y z -> SYMBOLIC_Closure x z.
  641.  
  642.   Fixpoint SYMBOLIC_append x y z (f : SYMBOLIC_Closure x y) : SYMBOLIC_Closure y z -> SYMBOLIC_Closure x z :=
  643.   match f in SYMBOLIC_Closure A' B' return SYMBOLIC_Closure B' z -> SYMBOLIC_Closure A' z with
  644.     | SYMBOLIC_Identity _ => fun y => y
  645.     | SYMBOLIC_Cons _ _ _ k x => fun y => SYMBOLIC_Cons k (SYMBOLIC_append x y)
  646.   end.
  647.  
  648.   Theorem SYMBOLIC_append_nil :
  649.     forall (X Y : SYMBOLIC_Objects) (f : SYMBOLIC_Closure X Y),
  650.       Identity (SYMBOLIC_append f (SYMBOLIC_Identity Y)) f.
  651.   induction f.
  652.   constructor.
  653.   simpl.
  654.   cut (Identity f (SYMBOLIC_append f (SYMBOLIC_Identity z))).
  655.   intro X; elim X.
  656.   constructor.
  657.   apply (equivalence_symmetry (Equivalence_Identity)).
  658.   assumption.
  659.   Defined.
  660.  
  661.   Theorem SYMBOLIC_append_associative :
  662.   forall (X Y Z W : SYMBOLIC_Objects) (f : SYMBOLIC_Closure X Y)
  663.     (g : SYMBOLIC_Closure Y Z) (h : SYMBOLIC_Closure Z W),
  664.     Identity (SYMBOLIC_append f (SYMBOLIC_append g h))
  665.   (SYMBOLIC_append (SYMBOLIC_append f g) h).
  666.   induction f.
  667.   constructor.
  668.   intros.
  669.   simpl.
  670.   cut (
  671.     Identity (SYMBOLIC_append f (SYMBOLIC_append g h))
  672.              (SYMBOLIC_append (SYMBOLIC_append f g) h)
  673.   ).
  674.   intro X; elim X.
  675.   constructor.
  676.   apply IHf.
  677.   Defined.
  678.  
  679.   Definition SYMBOLIC_Cat : Category SYMBOLIC_Closure (fun X Y => @Identity _).
  680.   apply (@Build_Category _ SYMBOLIC_Closure (fun X Y => @Identity _)
  681.     (fun x => SYMBOLIC_Identity x)
  682.     (fun x y z F G => SYMBOLIC_append F G)); simpl.
  683.  
  684.   intros; elim H; constructor.
  685.  
  686.   intros; elim H; constructor.
  687.  
  688.   intros; apply Equivalence_Identity.
  689.  
  690.   intros; constructor.
  691.  
  692.   apply SYMBOLIC_append_nil.
  693.  
  694.   apply SYMBOLIC_append_associative.
  695.  
  696.   Defined.
  697.  
  698.   Definition X := SYMBOLIC_Cat.
  699.   Notation "'<' e '>'" := (@SYMBOLIC_Cons _ _ _ e (SYMBOLIC_Identity _)).
  700.  
  701.   Theorem NASTY_THEOREM :
  702.     Identity ((< f'' > [X] < g'' >) [X] (< h'' > [X] < k'' >))
  703.              ((< f'' > [X] (< g'' > [X] < h'' >)) [X] < k'' >).
  704.   constructor.
  705.   Defined.
  706.  
  707.   Axiom Ob : Type.
  708.   Axiom a b c d e : Ob.
  709.   Axiom ARR : Ob -> Ob -> Type.
  710.   Axiom f : ARR a b.
  711.   Axiom g : ARR b c.
  712.   Axiom h : ARR c d.
  713.   Axiom k : ARR d e.
  714.   Axiom REL : forall X Y, Relation (ARR X Y).
  715.  
  716.   Axiom ARR_category : @Category Ob ARR REL.
  717.  
  718.   Definition interpret_symbolic_object := (fun X =>
  719.       match X with
  720.         | a'' => a
  721.         | b'' => b
  722.         | c'' => c
  723.         | d'' => d
  724.         | e'' => e
  725.       end).
  726.   Definition interpret_symbolic_map (X Y : SYMBOLIC_Objects) (f : SYMBOLIC_Morphisms X Y) : ARR (interpret_symbolic_object X) (interpret_symbolic_object Y).
  727.   destruct f; simpl.
  728.   apply f.
  729.   apply g.
  730.   apply h.
  731.   apply k.
  732.   Defined.
  733.  
  734.   Definition interpret_symbolic_closure (X Y : SYMBOLIC_Objects) (f : SYMBOLIC_Closure X Y) : ARR (interpret_symbolic_object X) (interpret_symbolic_object Y).
  735.   induction f.
  736.   apply (identity ARR_category).
  737.   eapply (compose ARR_category).
  738.   apply (interpret_symbolic_map s).
  739.   apply IHf.
  740.   Defined.
  741.  
  742.   Definition SYMBOLIC_ARR_Functor : Functor SYMBOLIC_Cat ARR_category.
  743.   Print Functor.
  744.   apply (Build_Functor SYMBOLIC_Cat ARR_category
  745.     interpret_symbolic_object
  746.     interpret_symbolic_closure);
  747.   simpl; intros.
  748.  
  749.   apply (hom_equivalence ARR_category).
  750.  
  751.   induction f0.
  752.   simpl.
  753.   apply (equivalence_symmetry (hom_equivalence ARR_category _ _)).
  754.   apply (category_left_identity ARR_category).
  755.   simpl in *.
  756.  
  757.   apply (equivalence_symmetry (hom_equivalence ARR_category _ _)).
  758.   eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
  759.   apply (equivalence_symmetry (hom_equivalence ARR_category _ _)).
  760.   apply (category_associativity ARR_category).
  761.   apply (compose_respectful_right ARR_category).
  762.   apply (equivalence_symmetry (hom_equivalence ARR_category _ _)).
  763.   apply IHf0.
  764.  
  765.   elim H.
  766.   apply (equivalence_reflexivity (hom_equivalence ARR_category _ _)).
  767.   Defined.
  768.  
  769.   Definition Y := ARR_category.
  770.   Theorem NASTY_THEOREM_easy_proof :
  771.     REL ((f [Y] g) [Y] (h [Y] k))
  772.         ((f [Y] (g [Y] h)) [Y] k).
  773.   pose NASTY_THEOREM.
  774.   pose (Functor_Equal SYMBOLIC_ARR_Functor i) as GIFT.
  775.   simpl in GIFT.
  776. (* FAIL *)
  777.  
  778. End SYMBOLIC.
  779.  
  780.  
  781. (*
  782. *** Local Variables: ***
  783. *** coq-prog-args: ("-emacs-U" "-nois") ***
  784. *** End: ***
  785. *)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
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
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!