API tools faq
paste
Advertisement
Guest User

Untitled

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