daily pastebin goal
62%
SHARE
TWEET

Untitled

a guest Jul 7th, 2017 60 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. 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 Decidable (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. Theorem Equivalence_Identity_map {X T : Type} (f : X -> T) : Equivalence (fun x y => @Identity T (f x) (f y)).
  47. apply Build_Equivalence.
  48. intros; constructor.
  49. intros; elim H; constructor.
  50. intros; elim H0; elim H; constructor.
  51. Defined.
  52.  
  53. Record Category (Ob : Type) (Hom : Ob -> Ob -> Type)
  54.                 (Hom_eq : forall X Y, Relation (Hom X Y))
  55.   := { identity : forall X, Hom X X
  56.      ; compose : forall X Y Z, Hom X Y -> Hom Y Z -> Hom X Z
  57.      ; compose_respectful_left : forall X Y Z (f f' : Hom X Y) (g : Hom Y Z),
  58.        Hom_eq _ _ f f' -> Hom_eq _ _ (compose f g) (compose f' g)
  59.      ; compose_respectful_right : forall X Y Z (f : Hom X Y) (g g' : Hom Y Z),
  60.        Hom_eq _ _ g g' -> Hom_eq _ _ (compose f g) (compose f g')
  61.      ; hom_equivalence : forall X Y, Equivalence (Hom_eq X Y)
  62.      ; category_left_identity : forall X Y (f : Hom X Y),
  63.        Hom_eq _ _ (compose (identity _) f) f
  64.      ; category_right_identity : forall X Y (f : Hom X Y),
  65.        Hom_eq _ _ (compose f (identity _)) f
  66.      ; category_associativity : forall X Y Z W (f : Hom X Y) (g : Hom Y Z) (h : Hom Z W),
  67.        Hom_eq _ _ (compose f (compose g h))
  68.                   (compose (compose f g) h)
  69.      }.
  70.  
  71. Notation "f '[' C ']'  g" := (compose C _ _ _ f g) (at level 20).
  72. Notation "'1_' C" := (identity C _) (at level 20).
  73.  
  74. Ltac refl :=
  75.   eapply equivalence_reflexivity;
  76.     [apply hom_equivalence;assumption].
  77. Ltac symm :=
  78.   eapply equivalence_symmetry;
  79.     [apply hom_equivalence;assumption|idtac].
  80. Ltac trans :=
  81.   eapply equivalence_transitivity;
  82.     [apply hom_equivalence;assumption|idtac|idtac].
  83.  
  84. Section Isomorphism.
  85.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  86.  
  87.   Definition Isomorphism (X Y : C_Ob) :=
  88.     @Sigma (And (C_Hom X Y) (C_Hom Y X))
  89.            (fun fg =>
  90.              match fg with
  91.                | both f g =>
  92.                  And (C_Hom_eq (compose C _ _ _ g f) (identity C _))
  93.                      (C_Hom_eq (compose C _ _ _ f g) (identity C _))
  94.              end).
  95.  
  96.   Definition isomorphism_to (X Y : C_Ob) (i : Isomorphism X Y) : C_Hom X Y.
  97.   destruct i as [[to from] _]; apply to.
  98.   Defined.
  99.  
  100.   Definition isomorphism_from (X Y : C_Ob) (i : Isomorphism X Y) : C_Hom Y X.
  101.   destruct i as [[to from] _]; apply from.
  102.   Defined.
  103.  
  104.   Theorem Isomorphism_Equivalence : Equivalence Isomorphism.
  105.   apply Build_Equivalence.
  106.  
  107.   Lemma Isomorphism_Identity : forall x : C_Ob, Isomorphism x x.
  108.     intro x; apply (witness _ (both (identity C x) (identity C x))).
  109.     apply And_idem.
  110.     apply category_left_identity.
  111.   Defined.
  112.   apply Isomorphism_Identity.
  113.  
  114.   intros x y [[I J] [i j]].
  115.   apply (witness _ (both J I)).
  116.   apply (both j i).
  117.  
  118.   Lemma Isomorphism_Compose : forall x y z : C_Ob, Isomorphism x y -> Isomorphism y z -> Isomorphism x z.
  119.     intros x y z [[I J] [i j]] [[I' J'] [i' j']].
  120.     apply (witness _ (both (compose C _ _ _ I I') (compose C _ _ _ J' J))).
  121.     apply both.
  122.    
  123.     trans.
  124.     apply (category_associativity C).
  125.     trans.
  126.     apply (compose_respectful_left C).
  127.     trans.
  128.     symm.
  129.     apply (category_associativity C).
  130.     apply (compose_respectful_right C).
  131.     apply i.
  132.     assert (C_Hom_eq (compose C z y y J' (identity C y))
  133.                      J').
  134.     apply category_right_identity.
  135.     trans.
  136.     apply (compose_respectful_left C).
  137.     apply X.
  138.     assumption.
  139.    
  140.     trans.
  141.     apply (category_associativity C).
  142.     trans.
  143.     apply (compose_respectful_left C).
  144.     trans.
  145.     symm.
  146.     apply (category_associativity C).
  147.     apply (compose_respectful_right C).
  148.     apply j'.
  149.     assert (C_Hom_eq (compose C x y y I (identity C y))
  150.                      I).
  151.     apply category_right_identity.
  152.     trans.
  153.     apply (compose_respectful_left C).
  154.     apply X.
  155.     assumption.
  156.     Defined.
  157.   apply Isomorphism_Compose.
  158.   Defined.
  159. End Isomorphism.
  160.  
  161. Section Functor.
  162.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  163.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  164.  
  165.   Record Functor
  166.     := { Map_Ob : C_Ob -> D_Ob
  167.        ; Map_Hom : forall X Y, C_Hom X Y -> D_Hom (Map_Ob X) (Map_Ob Y)
  168.        ; functor_identity : forall X, D_Hom_eq (Map_Hom (identity C X)) (identity D (Map_Ob X))
  169.        ; functor_compose : forall X Y Z (f : C_Hom X Y) (g : C_Hom Y Z),
  170.          D_Hom_eq (Map_Hom (compose C _ _ _ f g)) (compose D _ _ _ (Map_Hom f) (Map_Hom g))
  171.        ; Map_Hom_respectful : forall X Y (f f' : C_Hom X Y),
  172.          C_Hom_eq f f' -> D_Hom_eq (Map_Hom f) (Map_Hom f')
  173.     }.
  174.  
  175.   Notation "F '@' x" := (Map_Ob F x) (at level 20).
  176.   Notation "F '$' f" := (Map_Hom F f) (at level 20).
  177.  
  178.   Definition Functor_equality (F G : Functor) :=
  179.     @Sigma (forall X : C_Ob,
  180.              Isomorphism D (Map_Ob F X) (Map_Ob G X))
  181.           (fun Ob_iso =>
  182.             forall X Y (f : C_Hom X Y),
  183.               D_Hom_eq (Map_Hom F f)
  184.                        (compose D _ _ _
  185.                          (isomorphism_to (Ob_iso _))
  186.                          (compose D _ _ _
  187.                            (Map_Hom G f)
  188.                             (isomorphism_from (Ob_iso _))))).
  189.  
  190.   Theorem Functor_equivalence : Equivalence Functor_equality.
  191.     apply Build_Equivalence.
  192.    
  193.     intro x.
  194.     unfold Functor_equality.
  195.     apply witness with (t := (fun X => @Isomorphism_Identity _ _ _ D (Map_Ob x X))).
  196.     intros X Y f.
  197.     simpl.
  198.     trans.
  199.     symm.
  200.     apply category_left_identity.
  201.     apply compose_respectful_right.
  202.     trans.
  203.     symm.
  204.     apply category_right_identity.
  205.     apply compose_respectful_right.
  206.     refl.
  207.    
  208.     intros F G.
  209.     intros [F' F''].
  210.    
  211.     pose (Isomorphism_Equivalence D).
  212.     pose (match e with
  213.             | Build_Equivalence _ Isymm _ => Isymm
  214.           end) as Isymm.
  215.     unfold Functor_equality.
  216.     apply (witness _ (fun X => Isymm _ _ (F' X))).
  217.     intros X Y f.
  218.     unfold Isymm in *; unfold e in *; simpl.
  219.     generalize (F'' _ _ f).
  220.    
  221.     destruct (F' X); simpl.
  222.     destruct t; simpl.
  223.     destruct y; simpl.
  224.     destruct (F' Y); simpl.
  225.     destruct t; simpl.
  226.     destruct y; simpl.
  227.    
  228.     intro.
  229.     assert (
  230.       D_Hom_eq (compose D _ _ _ d0 (compose D _ _ _ (Map_Hom F f) d3))
  231.       (compose D _ _ _ d0 (compose D _ _ _
  232.         (compose D (Map_Ob F X) (Map_Ob G X) (Map_Ob F Y) d
  233.             (compose D (Map_Ob G X) (Map_Ob G Y) (Map_Ob F Y)
  234.                (Map_Hom G f) d4)) d3))
  235.       ).
  236.     apply compose_respectful_right.
  237.     apply compose_respectful_left.
  238.     assumption.
  239.    
  240.     trans.
  241.     Focus 2.
  242.     symm.
  243.     apply X1.
  244.     (* Gf = (d0 ((d (Gf d4)) d3)) *)
  245.     Lemma YUK
  246.       (F : Functor)
  247.       (G : Functor)
  248.       (X : C_Ob)
  249.       (Y : C_Ob)
  250.       (f : C_Hom X Y)
  251.       (d : D_Hom (F @ X) (G @ X))
  252.       (d0 : D_Hom (G @ X) (F @ X))
  253.       (d1 : D_Hom_eq (d0 [D] d) (identity D _))
  254.       (d2 : D_Hom_eq (d [D] d0) (identity D _))
  255.       (d3 : D_Hom (F @ Y) (G @ Y))
  256.       (d4 : D_Hom (G @ Y) (F @ Y))
  257.       (d5 : D_Hom_eq (d4 [D] d3) (identity D _))
  258.       (d6 : D_Hom_eq (d3 [D] d4) (identity D _))
  259.       (X0 : D_Hom_eq (F $ f) (d [D] ((G $ f) [D] d4)))
  260.       (X1 : D_Hom_eq (d0 [D] ((F $ f) [D] d3))
  261.              (d0 [D] ((d [D] ((G $ f) [D] d4)) [D] d3))) :
  262.       D_Hom_eq (G $ f) (d0 [D] ((d [D] ((G $ f) [D] d4)) [D] d3)).
  263.      
  264.       cut (D_Hom_eq (G $ f) ((G $ f) [D] (identity D _))).
  265.       cut (D_Hom_eq ((G $ f) [D] (identity D _)) ((G $ f) [D] (d4 [D] d3))).
  266.       cut (D_Hom_eq ((G $ f) [D] (d4 [D] d3)) ((identity D _) [D] ((G $ f) [D] (d4 [D] d3)))).
  267.       cut (D_Hom_eq ((identity D _) [D] ((G $ f) [D] (d4 [D] d3))) ((d0 [D] d) [D] ((G $ f) [D] (d4 [D] d3)))).
  268.       cut (D_Hom_eq ((d0 [D] d) [D] ((G $ f) [D] (d4 [D] d3))) (d0 [D] (d [D] ((G $ f) [D] (d4 [D] d3))))).
  269.       cut (D_Hom_eq (d0 [D] (d [D] ((G $ f) [D] (d4 [D] d3)))) (d0 [D] (d [D] (((G $ f) [D] d4) [D] d3)))).
  270.       cut (D_Hom_eq (d0 [D] (d [D] (((G $ f) [D] d4) [D] d3))) (d0 [D] ((d [D] ((G $ f) [D] d4)) [D] d3))).
  271.       intros.
  272.      
  273.       do 7 (trans;[hypothesis|]); refl.
  274.      
  275.       apply compose_respectful_right.
  276.       apply (category_associativity D _ _ _ _ d ((G $ f) [D] d4) d3).
  277.      
  278.       do 2 apply compose_respectful_right.
  279.       apply category_associativity.
  280.      
  281.       symm; apply category_associativity.
  282.      
  283.       apply compose_respectful_left.
  284.       symm; assumption.
  285.      
  286.       symm; apply category_left_identity.
  287.      
  288.       apply compose_respectful_right.
  289.       symm; assumption.
  290.    
  291.       symm; apply category_right_identity.
  292.     Defined.
  293.     apply YUK; assumption.
  294.    
  295.     intros x y z F G; unfold Functor_equality.
  296.     destruct F.
  297.     destruct G.
  298.     pose (Isomorphism_Equivalence D).
  299.     pose (match e with
  300.             | Build_Equivalence _ _ Itrans => Itrans
  301.           end) as Itrans.
  302.     unfold Functor_equality.
  303.     apply (witness _ (fun X => Itrans _ _ _ (t X) (t0 X))).
  304.     intros; simpl.
  305.    
  306.     generalize (d X Y f).
  307.     generalize (d0 X Y f).
  308.    
  309.     destruct (t X); simpl.
  310.     destruct t1; destruct y0; simpl.
  311.     destruct (t0 X); simpl.
  312.     destruct t1; destruct y0; simpl.
  313.     simpl.
  314.     destruct (t Y); simpl.
  315.     destruct t1; destruct y0; simpl.
  316.     destruct (t0 Y); simpl.
  317.     destruct t1; destruct y0; simpl.
  318.     simpl.
  319.     (* Xf = ((d1 d5)(Zf (d14 d10))) *)
  320.    
  321.     Lemma BLECH
  322.       (F : Functor)
  323.       (G : Functor)
  324.       (H : Functor)
  325.       (X : C_Ob)
  326.       (Y : C_Ob)
  327.       (f : C_Hom X Y)
  328.       (d1 : D_Hom (F @ X) (G @ X))
  329.       (d2 : D_Hom (G @ X) (F @ X))
  330.       (d3 : D_Hom_eq (d2 [D] d1) (identity D _))
  331.       (d4 : D_Hom_eq (d1 [D] d2) (identity D _))
  332.       (d5 : D_Hom (G @ X) (H @ X))
  333.       (d6 : D_Hom (H @ X) (G @ X))
  334.       (d7 : D_Hom_eq (d6 [D] d5) (identity D _))
  335.       (d8 : D_Hom_eq (d5 [D] d6) (identity D _))
  336.       (d9 : D_Hom (F @ Y) (G @ Y))
  337.       (d10 : D_Hom (G @ Y) (F @ Y))
  338.       (d11 : D_Hom_eq (d10 [D] d9) (identity D _))
  339.       (d12 : D_Hom_eq (d9 [D] d10) (identity D _))
  340.       (d13 : D_Hom (G @ Y) (H @ Y))
  341.       (d14 : D_Hom (H @ Y) (G @ Y))
  342.       (d15 : D_Hom_eq (d14 [D] d13) (identity D _))
  343.       (d16 : D_Hom_eq (d13 [D] d14) (identity D _))
  344.     (WW : D_Hom_eq (F $ f) (d1 [D] ((G $ f) [D] d10)))
  345.     (MM : D_Hom_eq (G $ f) (d5 [D] ((H $ f) [D] d14))) :
  346.    D_Hom_eq (F $ f) ((d1 [D] d5) [D] ((H $ f) [D] (d14 [D] d10))).
  347.       symm.
  348.       cut (D_Hom_eq
  349.         (G $ f)
  350.         (d5 [D] ((H $ f) [D] d14))).
  351.       cut (D_Hom_eq
  352.         (F $ f)
  353.         (d1 [D] ((G $ f) [D] d10))).
  354.       intros.
  355.      
  356.       Ltac step K :=
  357.         match goal with |- D_Hom_eq ?X ?Y =>
  358.           cut (D_Hom_eq X K);[intro;trans;hypothesis|]
  359.         end.
  360.      
  361.       step (((d1 [D] d5) [D] (((H $ f) [D] d14) [D] d10))).
  362.       step ((d1 [D] (d5 [D] (((H $ f) [D] d14) [D] d10)))).
  363.       match goal with |- D_Hom_eq ?X ?y =>
  364.         cut (D_Hom_eq X ((d1 [D] ((d5 [D] ((H $ f) [D] d14)) [D] d10))))
  365.       end.
  366.       intro.
  367.       trans.
  368.       apply X4.
  369.      
  370.       match goal with |- D_Hom_eq ?X ?y =>
  371.         cut (D_Hom_eq X (d1 [D] ((G $ f) [D] d10)))
  372.       end.
  373.       intro; trans.
  374.       apply X5.
  375.      
  376.       apply compose_respectful_right.
  377.       trans.
  378.       apply compose_respectful_left.
  379.       apply X1.
  380.       symm.
  381.       apply (category_associativity D _ _ _ _ d5 ((H $ f) [D] d14) d10).
  382.      
  383.       apply compose_respectful_right.
  384.       apply compose_respectful_left.
  385.       symm; hypothesis.
  386.      
  387.       step ((d1 [D] (d5 [D] (((H $ f) [D] d14) [D] d10)))).
  388.      
  389.       apply (category_associativity D _ _ _ _).
  390.       symm; apply (category_associativity D _ _ _ _).
  391.       trans; [apply X0|].
  392.       apply compose_respectful_right.
  393.       symm.
  394.       step (((d5 [D] ((H $ f) [D] d14)) [D] d10)).
  395.       symm; assumption.
  396.       apply (category_associativity D _ _ _ _ d5).
  397.       apply compose_respectful_right.
  398.       apply (category_associativity D _ _ _ _).
  399.      
  400.       assumption.
  401.    
  402.       assumption.
  403.    
  404.     Defined.
  405.     intros.
  406.     eapply BLECH; hypothesis.
  407.   Defined.
  408. End Functor.
  409.  
  410. Section Functors.
  411.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  412.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  413.   Context {E_Ob E_Hom E_Hom_eq} (E : @Category E_Ob E_Hom E_Hom_eq).
  414.  
  415.   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').
  416.   intros; apply Map_Hom_respectful.
  417.   assumption.
  418.   Defined.
  419.  
  420.   Definition Identity_Functor : Functor C C.
  421.   Print Build_Functor.
  422.   apply (Build_Functor C C
  423.     (fun X => X)
  424.     (fun X Y f => f)).
  425.   intros; refl.
  426.   intros; refl.
  427.   intros; assumption.
  428.   Defined.
  429.  
  430.   Definition Compose_Functor (F : Functor C D) (G : Functor D E) : Functor C E.
  431.   Print Build_Functor.
  432.   apply (Build_Functor C E
  433.     (fun X => Map_Ob G (Map_Ob F X))
  434.     (fun X Y f => Map_Hom G _ _ (Map_Hom F _ _ f))).
  435.  
  436.   intros.
  437.   trans.
  438.   apply Map_Hom_respectful.
  439.   apply (functor_identity F X).
  440.   apply (functor_identity G _).
  441.  
  442.   intros.
  443.   trans.
  444.   apply Map_Hom_respectful.
  445.   apply (functor_compose F).
  446.   apply (functor_compose G).
  447.  
  448.   intros.
  449.   apply Map_Hom_respectful.
  450.   apply Map_Hom_respectful.
  451.   assumption.
  452.   Defined.
  453. End Functors.
  454.  
  455. Section NaturalTransformation.
  456.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  457.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  458.  
  459.   Context (F G : Functor C D).
  460.  
  461.   Record NaturalTransformation
  462.     := { Component : forall X : C_Ob, D_Hom (Map_Ob F X) (Map_Ob G X)
  463.        ; naturality : forall X Y (f : C_Hom X Y),
  464.          D_Hom_eq (compose D _ _ _ (Map_Hom F _ _ f) (Component Y))
  465.                   (compose D _ _ _ (Component X) (Map_Hom G _ _ f))
  466.        }.
  467. End NaturalTransformation.
  468.  
  469. Section NaturalTransformations.
  470.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  471.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  472.  
  473.   Context (F G H : Functor C D).
  474.  
  475.   Print Component.
  476.   Definition NaturalTransformation_Equivalence : Equivalence (fun (eta nu : NaturalTransformation F G) => forall X : C_Ob, D_Hom_eq (Component eta X) (Component nu X)).
  477.   apply Build_Equivalence.
  478.  
  479.   intros; refl.
  480.  
  481.   intros; symm; hypothesis.
  482.  
  483.   intros; trans; hypothesis.
  484.   Defined.
  485.  
  486.   Definition Identity_NaturalTransformation : NaturalTransformation F F.
  487.   apply (Build_NaturalTransformation F F
  488.     (fun X => identity D (Map_Ob F X))).
  489.   intros; trans.
  490.   apply category_right_identity.
  491.   symm; apply category_left_identity.
  492.   Defined.
  493.  
  494.   Definition Compose_NaturalTransformation (eta : NaturalTransformation F G) (nu : NaturalTransformation G H) : NaturalTransformation F H.
  495.   apply (Build_NaturalTransformation F H
  496.     (fun X => compose D _ _ _ (Component eta X) (Component nu X))).
  497.   intros.
  498.   trans.
  499.   apply (category_associativity D).
  500.   trans.
  501.   apply (compose_respectful_left D).
  502.   apply (naturality eta).
  503.   trans.
  504.   symm; apply (category_associativity D).
  505.   symm.
  506.   trans.
  507.   symm.
  508.   apply (category_associativity D).
  509.   apply (compose_respectful_right D).
  510.   symm.
  511.   apply (naturality nu).
  512.   Defined.
  513. End NaturalTransformations.
  514.  
  515.  
  516. Section FunctorCategory.
  517.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  518.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  519.   Definition FunctorCategory : @Category
  520.     (Functor C D) (fun F G => NaturalTransformation F G)
  521.     (fun F G =>
  522.       fun (eta nu : NaturalTransformation F G) =>
  523.         forall X : C_Ob,
  524.           D_Hom_eq (Component eta X) (Component nu X)).
  525.   Print Build_Category.
  526.   Print Identity_NaturalTransformation.
  527.   apply (@Build_Category
  528.    
  529.     (Functor C D)
  530.     (fun F G => NaturalTransformation F G)
  531.     (fun F G =>
  532.       fun (eta nu : NaturalTransformation F G) =>
  533.         forall X : C_Ob,
  534.           D_Hom_eq (Component eta X) (Component nu X))
  535.    
  536.     (fun F => Identity_NaturalTransformation F)
  537.     (fun _ _ _ eta nu => Compose_NaturalTransformation eta nu));
  538.   simpl; intros.
  539.  
  540.   apply compose_respectful_left.
  541.   hypothesis.
  542.  
  543.   apply compose_respectful_right.
  544.   hypothesis.
  545.  
  546.   apply NaturalTransformation_Equivalence.
  547.  
  548.   apply category_left_identity.
  549.  
  550.   apply category_right_identity.
  551.  
  552.   apply category_associativity.
  553.   Defined.
  554. End FunctorCategory.
  555.  
  556. Section OppositeCategory.
  557.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  558.  
  559.   Definition OppositeCategory : @Category C_Ob (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f).
  560.   apply (Build_Category
  561.     (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f)
  562.     (fun X => identity C X)
  563.     (fun X Y Z f g => compose C Z Y X g f)).
  564.   intros; apply compose_respectful_right; hypothesis.
  565.   intros; apply compose_respectful_left; hypothesis.
  566.   intros;
  567.     apply Build_Equivalence; destruct (hom_equivalence C X Y);
  568.       hypothesis.
  569.   intros; apply category_right_identity.
  570.   intros; apply category_left_identity.
  571.   intros; symm; apply category_associativity.
  572.   Defined.
  573. End OppositeCategory.
  574.  
  575. Section UniqueExistence.
  576.   Context {C_Ob : Type}
  577.           {C_Hom : C_Ob -> C_Ob -> Type}
  578.           {C_Hom_eq : forall X Y, Relation (C_Hom X Y)}.
  579.  
  580.   Definition ExistsUnique {X Y} (C : @Category C_Ob C_Hom C_Hom_eq) (P : C_Hom X Y -> Type) :=
  581.     Sigma (fun f =>
  582.       And (P f) (forall f' : C_Hom X Y, P f' -> C_Hom_eq f f')).
  583. End UniqueExistence.
  584.  
  585. Section TerminalObject.
  586.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  587.  
  588.   Definition Terminal (T : C_Ob) :=
  589.     forall X, ExistsUnique C (fun (f : C_Hom X T) => True).
  590.  
  591.   (** TODO: unique up to unique isomorphism,
  592.      needs predicative definition of isomorphism **)
  593.   Theorem Terminal_unique (T T' : C_Ob) :
  594.     Terminal T -> Terminal T' -> Isomorphism C T T'.
  595.   unfold Terminal; unfold Isomorphism; intros.
  596.   pose (X T); pose (X T').
  597.   pose (X0 T); pose (X0 T').
  598.   destruct e; destruct e0; destruct e1; destruct e2.
  599.   apply (witness _ (both t1 t0)).
  600.   destruct a; destruct a2.
  601.   pose (c (t1 [C] t0) I).
  602.   pose (c0 (t0 [C] t1) I).
  603.   pose (c (identity C _) I).
  604.   pose (c0 (identity C _) I).
  605.   constructor.
  606.   trans; [symm|]; hypothesis.
  607.   trans; [symm|]; hypothesis.
  608.   Defined.
  609.  
  610. End TerminalObject.
  611.  
  612. Section ConstantFunctor.
  613.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  614.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  615.  
  616.   Definition Delta (U : D_Ob) : Functor C D.
  617.   apply (Build_Functor C D
  618.     (fun _ => U)
  619.     (fun _ _ _ => identity D U)).
  620.   intro; refl.
  621.   intros; symm; apply category_left_identity.
  622.   intros; refl.
  623.   Defined.
  624. End ConstantFunctor.
  625.  
  626. Section Cone.
  627.   Context {II_Ob II_Hom II_Hom_eq} (II : @Category II_Ob II_Hom II_Hom_eq).
  628.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  629.  
  630.   Definition Cone (U : C_Ob) (D : Functor II C) := NaturalTransformation (Delta II C U) D.
  631. End Cone.
  632.  
  633.  
  634.  
  635.  
  636. Section SYMBOLIC.
  637.  
  638.   Inductive Symbolic_Objects := aSYM | bSYM | cSYM | dSYM | eSYM.
  639.   Inductive Symbolic_Maps : Symbolic_Objects -> Symbolic_Objects -> Type :=
  640.   | fSYM : Symbolic_Maps aSYM bSYM
  641.   | gSYM : Symbolic_Maps bSYM cSYM
  642.   | hSYM : Symbolic_Maps cSYM dSYM
  643.   | kSYM : Symbolic_Maps dSYM eSYM.
  644.   Inductive Symbolic_Syntax : Symbolic_Objects -> Symbolic_Objects -> Type :=
  645.   | idSYM : forall S, Symbolic_Syntax S S
  646.   | compSYM : forall X Y Z, Symbolic_Syntax X Y -> Symbolic_Syntax Y Z -> Symbolic_Syntax X Z
  647.   | symbolSYM : forall X Y, Symbolic_Maps X Y -> Symbolic_Syntax X Y.
  648.   Inductive Symbolic_Closure : Symbolic_Objects -> Symbolic_Objects -> Type :=
  649.   | nilClosure : forall X, Symbolic_Closure X X
  650.   | consClosure : forall X Y Z, Symbolic_Maps X Y -> Symbolic_Closure Y Z -> Symbolic_Closure X Z.
  651.  
  652.   Fixpoint Symbolic_append x y z (f : Symbolic_Closure x y) : Symbolic_Closure y z -> Symbolic_Closure x z :=
  653.   match f in Symbolic_Closure A' B' return Symbolic_Closure B' z -> Symbolic_Closure A' z with
  654.     | nilClosure _ => fun y => y
  655.     | consClosure _ _ _ k x => fun y => consClosure k (Symbolic_append x y)
  656.   end.
  657.  
  658.   Theorem Symbolic_append_nil :
  659.     forall (X Y : Symbolic_Objects) (f : Symbolic_Closure X Y),
  660.       Identity (Symbolic_append f (nilClosure Y)) f.
  661.   induction f.
  662.   constructor.
  663.   simpl.
  664.   cut (Identity f (Symbolic_append f (nilClosure Z))).
  665.   intro H; elim H.
  666.   constructor.
  667.   apply (equivalence_symmetry (Equivalence_Identity)).
  668.   assumption.
  669.   Defined.
  670.  
  671.   Theorem Symbolic_append_associative :
  672.   forall (X Y Z W : Symbolic_Objects) (f : Symbolic_Closure X Y)
  673.     (g : Symbolic_Closure Y Z) (h : Symbolic_Closure Z W),
  674.     Identity (Symbolic_append f (Symbolic_append g h))
  675.   (Symbolic_append (Symbolic_append f g) h).
  676.   induction f.
  677.   constructor.
  678.   intros.
  679.   simpl.
  680.   cut (
  681.     Identity (Symbolic_append f (Symbolic_append g h))
  682.              (Symbolic_append (Symbolic_append f g) h)
  683.   ).
  684.   intro H; elim H.
  685.   constructor.
  686.   apply IHf.
  687.   Defined.
  688.  
  689.   Definition Symbolic_Semantics {X Y} (S : Symbolic_Syntax X Y) : Symbolic_Closure X Y.
  690.   induction S.
  691.   constructor.
  692.   apply (Symbolic_append IHS1 IHS2).
  693.   apply (consClosure s (nilClosure _)).
  694.   Defined.
  695.  
  696.   Definition Symbolic_eq := (fun X Y (f g : Symbolic_Syntax X Y) => Identity (Symbolic_Semantics f) (Symbolic_Semantics g)).
  697.  
  698.   Definition Symbolic_Cat : Category Symbolic_Syntax Symbolic_eq.
  699.   apply (@Build_Category _ Symbolic_Syntax Symbolic_eq
  700.     (fun x => idSYM x)
  701.     (fun x y z F G => compSYM F G));
  702.   unfold Symbolic_eq in *; simpl.
  703.  
  704.   intros; elim H; constructor.
  705.  
  706.   intros; elim H; constructor.
  707.  
  708.   intros; apply Equivalence_Identity_map.
  709.  
  710.   intros; constructor.
  711.  
  712.   intros.
  713.   apply Symbolic_append_nil.
  714.  
  715.   intros.
  716.   apply Symbolic_append_associative.
  717.   Defined.
  718.  
  719.   Fixpoint Quote_Semantics (X Y : Symbolic_Objects) (f : Symbolic_Closure X Y) : Symbolic_Syntax X Y :=
  720.     match f with
  721.       | nilClosure _ => identity Symbolic_Cat _
  722.       | consClosure _ _ _ s f =>
  723.         compose Symbolic_Cat _ _ _ (symbolSYM s) (Quote_Semantics f)
  724.     end.
  725.  
  726.   Lemma quote_eval_harmony {X Y} (f : Symbolic_Syntax X Y) :
  727.     Symbolic_eq (Quote_Semantics (Symbolic_Semantics f))
  728.                 f.
  729.   unfold Symbolic_eq.
  730.   Lemma quote_eval_harmony' {X Y} (f : Symbolic_Closure X Y) :
  731.     Identity (Symbolic_Semantics (Quote_Semantics f))
  732.              f.
  733.     induction f; simpl.
  734.     constructor.
  735.     pose (equivalence_symmetry (Equivalence_Identity) _ _ IHf).
  736.     elim i.
  737.     constructor.
  738.   Defined.
  739.   apply quote_eval_harmony'.
  740.   Defined.
  741.  
  742.   Definition X := Symbolic_Cat.
  743.   Notation "'<' e '>'" := (symbolSYM e).
  744.  
  745.   Theorem NASTY_THEOREM :
  746.     Symbolic_eq ((< fSYM > [X] < gSYM >) [X] (< hSYM > [X] < kSYM >))
  747.                 ((< fSYM > [X] (< gSYM > [X] < hSYM >)) [X] < kSYM >).
  748.   constructor.
  749.   Defined.
  750.  
  751.   Axiom Ob : Type.
  752.   Axiom a b c d e : Ob.
  753.   Axiom ARR : Ob -> Ob -> Type.
  754.   Axiom f : ARR a b.
  755.   Axiom g : ARR b c.
  756.   Axiom h : ARR c d.
  757.   Axiom k : ARR d e.
  758.   Axiom REL : forall X Y, Relation (ARR X Y).
  759.  
  760.   Axiom ARR_category : @Category Ob ARR REL.
  761.  
  762.   Definition interpret_symbolic_object := (fun X =>
  763.       match X with
  764.         | aSYM => a
  765.         | bSYM => b
  766.         | cSYM => c
  767.         | dSYM => d
  768.         | eSYM => e
  769.       end).
  770.  
  771.   Definition interpret_symbolic_syntax (X Y : Symbolic_Objects) (f : Symbolic_Syntax X Y) : ARR (interpret_symbolic_object X) (interpret_symbolic_object Y).
  772.  
  773.   induction f; simpl in *.
  774.  
  775.   apply (identity ARR_category).
  776.  
  777.   apply (compose ARR_category _ _ _ IHf1 IHf2).
  778.  
  779.   destruct s; simpl.
  780.   apply f.
  781.   apply g.
  782.   apply h.
  783.   apply k.
  784.   Defined.
  785.  
  786.   Definition interp_symbolic_syntax (X Y : Symbolic_Objects) (f : Symbolic_Closure X Y) : ARR (interpret_symbolic_object X) (interpret_symbolic_object Y).
  787.   induction f.
  788.   apply (identity ARR_category).
  789.   apply (compose ARR_category _ _ _ (interpret_symbolic_syntax (symbolSYM s)) IHf).
  790.   Defined.
  791.  
  792.   Theorem interp_factors (X Y : Symbolic_Objects) : forall f : Symbolic_Syntax X Y,
  793.     REL (interpret_symbolic_syntax f)
  794.         (interp_symbolic_syntax (Symbolic_Semantics f)).
  795.     induction f0;
  796.       simpl.
  797.     apply (equivalence_reflexivity (hom_equivalence ARR_category _ _)).
  798.     Lemma factor_through_append X Y Z (f : Symbolic_Closure X Y) (g : Symbolic_Closure Y Z) :
  799.     REL (interp_symbolic_syntax f [ARR_category] interp_symbolic_syntax g)
  800.         (interp_symbolic_syntax (Symbolic_append f g)).
  801.       induction f.
  802.       simpl.
  803.       apply category_left_identity.
  804.       pose (IHf g).
  805.       assert (
  806.         REL (interp_symbolic_syntax (Symbolic_append (consClosure s f0) g))
  807.             ((interpret_symbolic_syntax (symbolSYM s)) [ARR_category] (interp_symbolic_syntax (Symbolic_append f0 g)))
  808.       ).
  809.       apply (equivalence_reflexivity (hom_equivalence ARR_category _ _)).
  810.       eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
  811.       Focus 2.
  812.       apply (equivalence_symmetry (hom_equivalence ARR_category _ _)).
  813.       apply X1.
  814.       assert (
  815.         REL
  816.         (interp_symbolic_syntax (consClosure s f0) [ARR_category]
  817.           interp_symbolic_syntax g)
  818.         ((interpret_symbolic_syntax < s > [ARR_category] interp_symbolic_syntax f0) [ARR_category]
  819.           interp_symbolic_syntax g)
  820.       ).
  821.       apply (equivalence_reflexivity (hom_equivalence ARR_category _ _)).
  822.       eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
  823.       apply X2.
  824.       eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
  825.       apply (equivalence_symmetry (hom_equivalence ARR_category _ _)).
  826.       apply (category_associativity ARR_category).
  827.       apply compose_respectful_right.
  828.       hypothesis.
  829.     Defined.
  830.    
  831.     Focus 2.
  832.     destruct s; simpl;
  833.       apply (equivalence_symmetry (hom_equivalence ARR_category _ _));
  834.         apply category_right_identity.
  835.    
  836.     eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
  837.     Focus 2.
  838.     apply (@factor_through_append _ _ _ (Symbolic_Semantics f0_1) (Symbolic_Semantics f0_2)).
  839.     eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
  840.     apply compose_respectful_left.
  841.     apply IHf0_1.
  842.     eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
  843.     apply compose_respectful_right.
  844.     apply IHf0_2.
  845.     apply (equivalence_reflexivity (hom_equivalence ARR_category _ _)).
  846.   Defined.
  847.  
  848.   Definition Symbolic_ARR_Functor : Functor Symbolic_Cat ARR_category.
  849.   Print Functor.
  850.   apply (Build_Functor Symbolic_Cat ARR_category
  851.     interpret_symbolic_object
  852.     interpret_symbolic_syntax);
  853.   simpl; intros.
  854.  
  855.   apply (hom_equivalence ARR_category).
  856.   apply (hom_equivalence ARR_category).
  857.  
  858.   pose (quote_eval_harmony f0).
  859.   pose (quote_eval_harmony f').
  860.  
  861.   pose (interp_factors f0).
  862.   pose (interp_factors f').
  863.  
  864.   eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
  865.   apply r.
  866.  
  867.   eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
  868.   Focus 2.
  869.   eapply (equivalence_symmetry (hom_equivalence ARR_category _ _)).
  870.   apply r0.
  871.   elim H.
  872.   apply (equivalence_reflexivity (hom_equivalence ARR_category _ _)).
  873.  
  874.   Defined.
  875.  
  876.   Definition Y := ARR_category.
  877.   Theorem NASTY_THEOREM_easy_proof :
  878.     REL ((f [Y] g) [Y] (h [Y] k))
  879.         ((f [Y] (g [Y] h)) [Y] k).
  880.   pose NASTY_THEOREM.
  881.   pose (Functor_Equal Symbolic_ARR_Functor s) as GIFT.
  882.   apply GIFT.
  883.   Defined.
  884.  
  885. (* FAIL *)
  886.  
  887. End SYMBOLIC.
  888.  
  889. Print Assumptions NASTY_THEOREM_easy_proof.
  890.  
  891.  
  892.  
  893.  
  894.  
  895. (*
  896. *** Local Variables: ***
  897. *** coq-prog-args: ("-emacs-U" "-nois") ***
  898. *** End: ***
  899. *)
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