API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Jul 7th, 2017
145
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
OCaml Brief 24.39 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. 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.  
  294. Section Trinkets.
  295.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
  296.  
  297.   Definition Isomorphism (X Y : Ob) (f : Hom X Y) :=
  298.     @Sigma (Hom Y X)
  299.     (fun (g : Hom Y X) =>
  300.       And (Hom_eq (compose C _ _ _ f g) (identity C _))
  301.           (Hom_eq (compose C _ _ _ g f) (identity C _))).
  302.  
  303.   Definition Exists {X Y : Ob} (P : Hom X Y -> Type) :=
  304.     @Sigma (Hom X Y) P.
  305.  
  306.   Definition ExistsUnique {X Y : Ob} (P : Hom X Y -> Type) :=
  307.     And (Exists P)
  308.         (forall f f' : Hom X Y,
  309.           P f -> P f' -> Hom_eq f f').
  310.  
  311.   Definition Terminal (C : @Category Ob Hom Hom_eq) (T : Ob) :=
  312.     forall X, ExistsUnique (fun f : Hom X T => True).
  313.  
  314.   Definition Initial (C : @Category Ob Hom Hom_eq) (T : Ob) :=
  315.     forall X, ExistsUnique (fun f : Hom T X => True).
  316.  
  317. End Trinkets.
  318.  
  319. Section OppositeCategory.
  320.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  321.  
  322.   Definition OppositeCategory : @Category C_Ob (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f).
  323.   apply (Build_Category
  324.     (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f)
  325.     (fun X => identity C X)
  326.     (fun X Y Z f g => compose C Z Y X g f)).
  327.   intros; apply Compose_respectful_right; assumption.
  328.   intros; apply Compose_respectful_left; assumption.
  329.   intros;
  330.     apply Build_Equivalence; destruct (category_equivalence C X Y);
  331.       hypothesis.
  332.   intros; apply category_right_identity.
  333.   intros; apply category_left_identity.
  334.   intros.
  335.   apply (equivalence_symmetry (category_equivalence C _ _)).
  336.   apply category_associativity.
  337.   Defined.
  338. End OppositeCategory.
  339.  
  340. Section Terminal_Initial_Dual.
  341.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  342.   Definition Cop := OppositeCategory C.
  343.  
  344.   Theorem TerminalOp_Initial (L : C_Ob) :
  345.     Terminal Cop L -> Initial C L.
  346.     unfold Terminal; unfold Initial.
  347.     intros f X; destruct (f X) as [[g IPrf] gPrf].
  348.     constructor.
  349.     apply (witness _ g).
  350.     constructor.
  351.     apply gPrf.
  352.   Defined.
  353.  
  354.   Theorem InitialOp_Terminal (L : C_Ob) :
  355.     Initial Cop L -> Terminal C L.
  356.     unfold Terminal; unfold Initial.
  357.     intros f X; destruct (f X) as [[g IPrf] gPrf].
  358.     constructor.
  359.     apply (witness _ g).
  360.     constructor.
  361.     apply gPrf.
  362.   Defined.
  363.  
  364. End Terminal_Initial_Dual.
  365.  
  366. Section BijectionSubcategory.
  367.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
  368.  
  369.   Definition Bijection (X Y : Ob) := Exists (Isomorphism C X Y).
  370.  
  371.   Definition Invert_Bijection (X Y : Ob) : Bijection X Y -> Bijection Y X.
  372.   intros [f [g [p1 p2]]].
  373.   apply (witness _ g).
  374.   apply (witness _ f).
  375.   constructor; assumption.
  376.   Defined.
  377.  
  378.   Definition Identity_Bijection (X : Ob) : Bijection X X.
  379.   apply (witness _ (identity C X)).
  380.   apply (witness _ (identity C X)).
  381.   apply And_idem.
  382.   apply category_left_identity.
  383.   Defined.
  384.  
  385.   Definition Compose_Bijection (X Y Z : Ob)
  386.     (f : Bijection X Y) (g : Bijection Y Z) :
  387.     Bijection X Z.
  388.   unfold Bijection in *.
  389.   destruct f as [fTo [fFrom [fPrf fPrf']]].
  390.   destruct g as [gTo [gFrom [gPrf gPrf']]].
  391.   apply (witness _ (compose C _ _ _ fTo gTo)).
  392.   apply (witness _ (compose C _ _ _ gFrom fFrom)).
  393.  
  394.   Lemma Compose_Bijection_Lemma
  395.     (X Y Z : Ob)
  396.     (fTo : Hom X Y)
  397.     (fFrom : Hom Y X)
  398.     (fPrf : Hom_eq (compose C X Y X fTo fFrom) (identity C X))
  399.     (fPrf' : Hom_eq (compose C Y X Y fFrom fTo) (identity C Y))
  400.     (gTo : Hom Y Z)
  401.     (gFrom : Hom Z Y)
  402.     (gPrf : Hom_eq (compose C Y Z Y gTo gFrom) (identity C Y))
  403.       :
  404.     (Hom_eq
  405.       (compose C X Z X (compose C X Y Z fTo gTo)
  406.         (compose C Z Y X gFrom fFrom)) (identity C X)).
  407.  
  408.   pose (@SYNTAX_category Ob Hom) as SYN.
  409.   assert (
  410.     Syntax_eq
  411.      (compose SYN X Z X (compose SYN X Y Z (injSYM _ _ fTo) (injSYM _ _ gTo)) (compose SYN Z Y X (injSYM _ _ gFrom) (injSYM _ _ fFrom)))
  412.      (compose SYN _ _ _ (injSYM _ _ fTo)
  413.        (compose SYN _ _ _
  414.          (compose SYN _ _ _ (injSYM _ _ gTo) (injSYM _ _ gFrom))
  415.          (injSYM _ _ fFrom)))
  416.   ) as EQUATION by apply identical.
  417.   pose (Map_Hom_respectful (Interpret C) _ _ _ _ EQUATION) as EQUATION'; simpl in EQUATION'.
  418.  
  419.   eapply (equivalence_transitivity (category_equivalence C _ _)).
  420.   apply EQUATION'.
  421.   clear EQUATION'; clear EQUATION.
  422.  
  423.   eapply (equivalence_transitivity (category_equivalence C _ _)).
  424.   apply Compose_respectful_right.
  425.   apply Compose_respectful_left.
  426.   apply gPrf.
  427.  
  428.   eapply (equivalence_transitivity (category_equivalence C _ _)).
  429.   apply Compose_respectful_right.
  430.   apply category_left_identity.
  431.   apply fPrf.
  432.   Defined.
  433.  
  434.   apply both; apply Compose_Bijection_Lemma;
  435.     assumption.
  436.   Defined.
  437.  
  438.   Definition BijectionSubcategory :
  439.     @Category Ob Bijection
  440.     (fun (X Y : Ob) (f g : Bijection X Y) =>
  441.       Hom_eq (pi1 f) (pi1 g)).
  442.   apply (Build_Category
  443.     Bijection
  444.     (fun (X Y : Ob) (f g : Bijection X Y) =>
  445.       Hom_eq (pi1 f) (pi1 g))
  446.     (fun X => Identity_Bijection X)
  447.     (fun X Y Z f g => Compose_Bijection f g)).
  448.  
  449.   intros X Y Z f f' g.
  450.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  451.   destruct f' as [f'To [f'From [f'PrfTo f'PrfFrom]]].
  452.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  453.   simpl.
  454.   apply Compose_respectful_left.
  455.  
  456.   intros X Y Z f f' g.
  457.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  458.   destruct f' as [f'To [f'From [f'PrfTo f'PrfFrom]]].
  459.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  460.   simpl.
  461.   apply Compose_respectful_right.
  462.  
  463.   intros; apply Equivalence_Pullback.
  464.   apply (category_equivalence C).
  465.  
  466.   intros X Y.
  467.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  468.   simpl.
  469.   apply category_left_identity.
  470.  
  471.   intros X Y.
  472.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  473.   simpl.
  474.   apply category_right_identity.
  475.  
  476.   intros X Y Z W.
  477.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  478.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  479.   destruct h as [hTo [hFrom [hPrfTo hPrfFrom]]].
  480.   simpl.
  481.   apply category_associativity.
  482.   Defined.
  483.  
  484.   Definition BijectionSubcategory_Embedding : Functor BijectionSubcategory C.
  485.   apply (Build_Functor BijectionSubcategory C
  486.     (fun X => X)
  487.     (fun X Y f => pi1 f)); simpl; intros.
  488.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  489.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  490.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  491.   simpl.
  492.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  493.   assumption.
  494.   Defined.
  495.  
  496. End BijectionSubcategory.
  497.  
  498. Section Functors.
  499.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  500.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  501.   Context {E_Ob E_Hom E_Hom_eq} (E : @Category E_Ob E_Hom E_Hom_eq).
  502.  
  503.   Definition Constant_Functor (V : C_Ob) : Functor C C.
  504.   apply (Build_Functor C C
  505.     (fun _ => V)
  506.     (fun _ _ _ => identity C V)); intros.
  507.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  508.   apply (equivalence_symmetry (category_equivalence C _ _)).
  509.   apply category_left_identity.
  510.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  511.   Defined.
  512.  
  513.   Definition Identity_Functor : Functor C C.
  514.   apply (Build_Functor C C
  515.     (fun X => X)
  516.     (fun _ _ f => f)); intros.
  517.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  518.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  519.   assumption.
  520.   Defined.
  521.  
  522.   Definition Compose_Functors (F : Functor C D) (G : Functor D E) : Functor C E.
  523.   apply (Build_Functor C E
  524.     (fun X => Map_Ob G (Map_Ob F X))
  525.     (fun _ _ f => Map_Hom G _ _ (Map_Hom F _ _ f))); intros.
  526.  
  527.   apply (equivalence_transitivity (category_equivalence E _ _))
  528.     with (y := Map_Hom G _ _ (identity D _)).
  529.   apply Map_Hom_respectful.
  530.   apply (functor_identity F).
  531.   apply (functor_identity G).
  532.  
  533.   apply (equivalence_transitivity (category_equivalence E _ _))
  534.     with (y := Map_Hom G _ _ (compose D _ _ _
  535.       (Map_Hom F _ _ f) (Map_Hom F _ _ g))).
  536.   apply Map_Hom_respectful.
  537.   apply (functor_compose F).
  538.   apply (functor_compose G).
  539.  
  540.   apply Map_Hom_respectful.
  541.   apply Map_Hom_respectful.
  542.   assumption.
  543.   Defined.
  544.  
  545.   Definition Equal_Functors (F F' : Functor C D) : Type :=
  546.     @Sigma (forall X, Exists (Isomorphism D (Map_Ob F X) (Map_Ob F' X)))
  547.     (fun iso =>
  548.       forall X Y (f : C_Hom X Y),
  549.         D_Hom_eq
  550.           (compose D _ _ _ (Map_Hom F _ _ f) (pi1 (iso Y)))
  551.           (compose D _ _ _ (pi1 (iso X)) (Map_Hom F' _ _ f))).
  552.  
  553.   Theorem Equivalence_Equal_Functors : Equivalence Equal_Functors.
  554.     unfold Equal_Functors; apply Build_Equivalence.
  555.    
  556.     intro F; apply (witness _ (fun X => identity (BijectionSubcategory D) (Map_Ob F X))); simpl.
  557.     intros X Y f.
  558.     eapply (equivalence_transitivity (category_equivalence D _ _)).
  559.     apply category_right_identity.
  560.     apply (equivalence_symmetry (category_equivalence D _ _)).
  561.     apply category_left_identity.
  562.    
  563.     intros F G [a b].
  564.     apply (witness _ (fun X => Invert_Bijection (a X))).
  565.     intros X Y f.
  566.     generalize (b _ _ f).
  567.     destruct (a X) as [ax' [ax'' [ax''' ax'''']]].
  568.     destruct (a Y) as [ay' [ay'' [ay''' ay'''']]].
  569.     simpl.
  570.     Lemma eq_functors_lemma1
  571.       (F : Functor C D) (G : Functor C D)
  572.       (X : C_Ob) (Y : C_Ob) (f : C_Hom X Y)
  573.       (ax' : D_Hom (F @ X) (G @ X))
  574.       (ax'' : D_Hom (G @ X) (F @ X))
  575.       (ax''' : D_Hom_eq (ax' [D] ax'') (Id[D]))
  576.       (ax'''' : D_Hom_eq (ax'' [D] ax') (Id[D]))
  577.       (ay' : D_Hom (F @ Y) (G @ Y))
  578.       (ay'' : D_Hom (G @ Y) (F @ Y))
  579.       (ay''' : D_Hom_eq (ay' [D] ay'') (Id[D]))
  580.       (ay'''' : D_Hom_eq (ay'' [D] ay') (Id[D])) :
  581.       D_Hom_eq ((F $ f) [D] ay') (ax' [D] (G $ f)) ->
  582.       D_Hom_eq ((G $ f) [D] ay'') (ax'' [D] (F $ f)).
  583.       pose (@SYNTAX_category D_Ob D_Hom) as SYN.
  584.      
  585.       intro Q.
  586.       assert (
  587.         D_Hom_eq (ax'' [D] (((F $ f) [D] ay') [D] ay''))
  588.                  (ax'' [D] ((ax' [D] (G $ f)) [D] ay''))
  589.       ).
  590.       apply Compose_respectful_right.
  591.       apply Compose_respectful_left.
  592.       apply Q.
  593.      
  594.       assert (
  595.         D_Hom_eq (ax'' [D] ((ax' [D] (G $ f)) [D] ay''))
  596.                  (ax'' [D] (((F $ f) [D] ay') [D] ay''))
  597.       ).
  598.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  599.       apply Compose_respectful_right.
  600.       apply Compose_respectful_left.
  601.       apply (equivalence_symmetry (category_equivalence D _ _)).
  602.       apply Q.
  603.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  604.       Focus 2.
  605.       apply Compose_respectful_right.
  606.       apply Compose_respectful_left.
  607.       apply (equivalence_symmetry (category_equivalence D _ _)).
  608.       apply Q.
  609.       assumption.
  610.      
  611.       assert (
  612.         D_Hom_eq (ax'' [D] (((F $ f) [D] ay') [D] ay''))
  613.                  (ax'' [D] (F $ f))
  614.       ).
  615.       assert (
  616.         Syntax_eq ((injSYM _ _ ax'') [SYN] (((injSYM _ _ ((F $ f))) [SYN] (injSYM _ _ ay')) [SYN] (injSYM _ _ ay'')))
  617.                   (((injSYM _ _ ax'') [SYN] (injSYM _ _ ((F $ f)))) [SYN] ((injSYM _ _ ay') [SYN] (injSYM _ _ ay'')))
  618.       ) as EQUATION by apply identical.
  619.       pose (Map_Hom_respectful (Interpret D) _ _ _ _ EQUATION) as EQUATION'; simpl in EQUATION'.
  620.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  621.       apply EQUATION'.
  622.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  623.       Focus 2.
  624.       apply category_right_identity.
  625.       apply Compose_respectful_right.
  626.       assumption.
  627.      
  628.       assert (
  629.         D_Hom_eq (ax'' [D] ((ax' [D] (G $ f)) [D] ay''))
  630.                  ((G $ f) [D] ay'')
  631.       ).
  632.       assert (
  633.         Syntax_eq ((injSYM _ _ ax'') [SYN] (((injSYM _ _ ax') [SYN] (injSYM _ _ ((G $ f)))) [SYN] (injSYM _ _ ay'')))
  634.                   (((injSYM _ _ ax'') [SYN] (injSYM _ _ ax')) [SYN] ((injSYM _ _ ((G $ f)) [SYN] (injSYM _ _ ay''))))
  635.       ) as EQUATION by apply identical.
  636.       pose (Map_Hom_respectful (Interpret D) _ _ _ _ EQUATION) as EQUATION'; simpl in EQUATION'.
  637.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  638.       apply EQUATION'.
  639.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  640.       Focus 2.
  641.       apply category_left_identity.
  642.       apply Compose_respectful_left.
  643.       assumption.
  644.      
  645.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  646.       eapply (equivalence_symmetry (category_equivalence D _ _)).
  647.       apply X3.
  648.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  649.       apply X1.
  650.       assumption.
  651.      
  652.     Defined.
  653.     apply eq_functors_lemma1; assumption.
  654.    
  655.     intros F G H [fg FG] [gh GH].
  656.     apply (witness _ (fun X => compose (BijectionSubcategory D) _ _ _
  657.       (fg X) (gh X))); simpl.
  658.     intros X Y f.
  659.     generalize (FG _ _ f).
  660.     generalize (GH _ _ f).
  661.     destruct (fg X) as [fgXF [fgXG [fgXPrf fpXPrf']]].
  662.     destruct (gh X) as [ghXF [ghXG [ghXPrf ghXPrf']]].
  663.     destruct (fg Y) as [fgYF [fgYG [fgYPrf fpYPrf']]].
  664.     destruct (gh Y) as [ghYF [ghYG [ghYPrf ghYPrf']]].
  665.     simpl.
  666.    
  667.     intros A B.
  668.  
  669.     eapply (equivalence_transitivity (category_equivalence D _ _)).
  670.     apply (category_associativity D).
  671.     eapply (equivalence_transitivity (category_equivalence D _ _)).
  672.     Focus 2.
  673.     apply (category_associativity D).
  674.      
  675.     eapply (equivalence_transitivity (category_equivalence D _ _)).
  676.     apply Compose_respectful_left.
  677.    
  678.     apply B.
  679.    
  680.     eapply (equivalence_transitivity (category_equivalence D _ _)).
  681.     apply (equivalence_symmetry (category_equivalence D _ _)).
  682.     apply (category_associativity D).
  683.    
  684.     apply Compose_respectful_right.
  685.     apply A.
  686.   Defined.
  687. End Functors.
  688.  
  689. Section NaturalTransformation.
  690.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  691.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  692.  
  693.   Context (F G : Functor C D).
  694.  
  695.   Record NaturalTransformation
  696.     := { Component : forall X : C_Ob, D_Hom (Map_Ob F X) (Map_Ob G X)
  697.        ; naturality : forall X Y (f : C_Hom X Y),
  698.          D_Hom_eq ((F $ f) [D] Component Y)
  699.                   (Component X [D] (G $ f))
  700. (*
  701.        ; Component_respectful : forall X X' : C_Ob,
  702.          Exists (Isomorphism C X X') ->
  703.          (Component X) ~ (Component X')
  704. *)
  705.        }.
  706.  
  707. Section FunctorCategory.
  708.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  709.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  710.  
  711.   Context (F G : Functor C D).
  712.  
  713.  
  714. (*
  715. *** Local Variables: ***
  716. *** coq-prog-args: ("-emacs-U" "-nois") ***
  717. *** End: ***
  718. *)
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!