API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Sep 9th, 2017
205
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
OCaml Brief 40.25 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 Bits.
  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.   Theorem Equivalence_Product {T} (R R' : Relation T) :
  74.     Equivalence R -> Equivalence R' -> Equivalence (fun x y => And (R x y) (R' x y)).
  75.     intros E1 E2; destruct E1; destruct E2.
  76.     apply Build_Equivalence;
  77.       intros; constructor;
  78.         try match goal with H : _ |- _ => solve [ apply H;
  79.           match goal with H : _ |- _ => solve [ apply H ] end ] end.
  80.   destruct X; eapply equivalence_transitivity0; hypothesis.
  81.   destruct X0; eapply equivalence_transitivity1; hypothesis.
  82.   Defined.
  83.  
  84.   Theorem Equivalence_Fiber {X T} (R : Relation T) : Equivalence R -> Equivalence (fun f g => forall x : X, R (f x) (g x)).
  85.   intro E; apply Build_Equivalence.
  86.   intros; apply (equivalence_reflexivity E).
  87.   intros; apply (equivalence_symmetry E); hypothesis.
  88.   intros; eapply (equivalence_transitivity E); hypothesis.
  89.   Defined.
  90.  
  91. End Bits.
  92.  
  93. Section CategoryTheory.
  94.  
  95. Record Category
  96.   (Ob : Type)
  97.   (Hom : Ob -> Ob -> Type)
  98.   (Hom_eq : forall X Y, Relation (Hom X Y))
  99.  
  100.   := { identity : forall X, Hom X X
  101.      ; compose : forall X Y Z, Hom X Y -> Hom Y Z -> Hom X Z
  102.      ; Compose_respectful_left : forall X Y Z (f f' : Hom X Y) (g : Hom Y Z),
  103.        Hom_eq _ _ f f' ->
  104.        Hom_eq _ _ (compose f g) (compose f' g)
  105.      ; Compose_respectful_right : forall X Y Z (f : Hom X Y) (g g' : Hom Y Z),
  106.        Hom_eq _ _ g g' ->
  107.        Hom_eq _ _ (compose f g) (compose f g')
  108.      ; category_equivalence : forall X Y, Equivalence (Hom_eq X Y)
  109.      ; category_left_identity : forall X Y (f : Hom X Y),
  110.        Hom_eq _ _ (compose (identity _) f) f
  111.      ; category_right_identity : forall X Y (f : Hom X Y),
  112.        Hom_eq _ _ (compose f (identity _)) f
  113.      ; category_associativity : forall X Y Z W (f : Hom X Y) (g : Hom Y Z) (h : Hom Z W),
  114.        Hom_eq _ _ (compose f (compose g h))
  115.                   (compose (compose f g) h)
  116.      }.
  117.  
  118. End CategoryTheory.
  119.  
  120. Notation "f '[' C ']'  g" := (compose C _ _ _ f g) (at level 20).
  121. Notation "'Id[' C ']'" := (identity C _) (at level 20).
  122.  
  123. Section Functor.
  124.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  125.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  126.  
  127.   Record Functor
  128.     := { Map_Ob : C_Ob -> D_Ob
  129.        ; Map_Hom : forall X Y,
  130.          C_Hom X Y -> D_Hom (Map_Ob X) (Map_Ob Y)
  131.        ; functor_identity : forall X,
  132.          D_Hom_eq (Map_Hom (identity C X)) (identity D (Map_Ob X))
  133.        ; functor_compose : forall X Y Z (f : C_Hom X Y) (g : C_Hom Y Z),
  134.          D_Hom_eq (Map_Hom (compose C _ _ _ f g)) (compose D _ _ _ (Map_Hom f) (Map_Hom g))
  135.        ; Map_Hom_respectful : forall X Y (f f' : C_Hom X Y),
  136.          C_Hom_eq f f' -> D_Hom_eq (Map_Hom f) (Map_Hom f')
  137.        }.
  138.  
  139. End Functor.
  140.  
  141. Notation "F '@' x" := (Map_Ob F x) (at level 20).
  142. Notation "F '$' f" := (Map_Hom F _ _ f) (at level 20).  
  143.  
  144. Section SYMBOLIC.
  145.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
  146.  
  147.   Inductive Syntax : Ob -> Ob -> Type :=
  148.   | idSYM : forall X : Ob, Syntax X X
  149.   | compSYM : forall X Y Z : Ob, Syntax X Y -> Syntax Y Z -> Syntax X Z
  150.   | injSYM : forall X Y, Hom X Y -> Syntax X Y.
  151.  
  152.   Inductive Semantics : Ob -> Ob -> Type :=
  153.   | nilSYM : forall X : Ob, Semantics X X
  154.   | consSYM : forall X Y Z : Ob, Hom X Y -> Semantics Y Z -> Semantics X Z.
  155.  
  156.   Fixpoint append {X Y Z : Ob} (f : Semantics X Y) : Semantics Y Z -> Semantics X Z :=
  157.   match f with
  158.     | nilSYM _ => fun g => g
  159.     | consSYM _ _ _ s f => fun g => consSYM s (append f g)
  160.   end.
  161.  
  162.   Lemma append_nil :
  163.     forall (X Y : Ob) (x : Semantics X Y),
  164.       Identity (append x (nilSYM Y)) x.
  165.     induction x; simpl.
  166.     apply identical.
  167.     elim (equivalence_symmetry Equivalence_Identity _ _ IHx).
  168.     apply identical.
  169.   Defined.
  170.    
  171.   Lemma append_associative :
  172.   forall (X Y Z W : Ob) (f : Semantics X Y) (g : Semantics Y Z) (h : Semantics Z W),
  173.     Identity (append f (append g h))
  174.              (append (append f g) h).
  175.     intros; induction f; simpl.
  176.     apply identical.
  177.     elim (IHf _).
  178.     apply identical.
  179.   Defined.
  180.  
  181.   Fixpoint evalSYN {X Y} (s : Syntax X Y) : Semantics X Y :=
  182.     match s with
  183.       | idSYM _ => nilSYM _
  184.       | compSYM _ _ _ f g => append (evalSYN f) (evalSYN g)
  185.       | injSYM _ _ f => consSYM f (nilSYM _)
  186.     end.
  187.  
  188.   Fixpoint quoteSYN {X Y} (s : Semantics X Y) : Syntax X Y :=
  189.     match s with
  190.       | nilSYM _ => idSYM _
  191.       | consSYM _ _ _ f s => compSYM (injSYM f) (quoteSYN s)
  192.     end.
  193.  
  194.   Definition Syntax_eq {X Y : Ob} (f f' : Syntax X Y) :=
  195.     Identity (evalSYN f) (evalSYN f').
  196.   Theorem Equivalence_Syntax_eq {X Y} : Equivalence (@Syntax_eq X Y).
  197.     apply (Equivalence_Identity_Pullback evalSYN).
  198.   Defined.
  199.  
  200.   Definition SYNTAX_category : Category Syntax (@Syntax_eq).
  201.   apply (Build_Category Syntax (@Syntax_eq)
  202.     idSYM
  203.     compSYM); unfold Syntax_eq; simpl.
  204.   intros X Y Z f f' g E; elim E; apply identical.
  205.   intros X Y Z f g g' E; elim E; apply identical.
  206.   intros X Y; apply Equivalence_Syntax_eq.
  207.   intros X Y f; apply identical.
  208.   intros X Y f; apply append_nil.
  209.   intros X Y Z W f g h; apply append_associative.
  210.   Defined.
  211.  
  212.   Theorem quote_eval_equal {X Y : Ob} (f : Syntax X Y) :
  213.     Syntax_eq (quoteSYN (evalSYN f)) f.
  214.     induction f; simpl in *;
  215.       try apply identical.
  216.    
  217.     Lemma quote_eval_equal_lemma {X Y Z} (e1 : Semantics X Y) (e2 : Semantics Y Z) :
  218.       Syntax_eq (quoteSYN (append e1 e2)) (compSYM (quoteSYN e1) (quoteSYN e2)).
  219.       intros; induction e1; simpl.
  220.       apply identical.
  221.       elim (IHe1 e2).
  222.       eapply (equivalence_transitivity (category_equivalence SYNTAX_category _ _)).
  223.       Focus 2.
  224.       apply (category_associativity SYNTAX_category _ _).
  225.       apply (Compose_respectful_right SYNTAX_category).
  226.       apply IHe1.
  227.     Defined.
  228.    
  229.     eapply (equivalence_transitivity Equivalence_Syntax_eq).
  230.     apply quote_eval_equal_lemma.
  231.     eapply (equivalence_transitivity (category_equivalence SYNTAX_category _ _)).
  232.     apply (Compose_respectful_left SYNTAX_category).
  233.     apply IHf1.
  234.     eapply (equivalence_transitivity (category_equivalence SYNTAX_category _ _)).
  235.     apply (Compose_respectful_right SYNTAX_category).
  236.     apply IHf2.
  237.     apply (equivalence_reflexivity (category_equivalence SYNTAX_category _ _)).
  238.   Defined.
  239.  
  240.   Fixpoint interpret_Syntax {X Y} (f : Syntax X Y) : Hom X Y :=
  241.     match f with
  242.       | idSYM _ => identity C _
  243.       | compSYM _ _ _ f g => compose C _ _ _ (interpret_Syntax f) (interpret_Syntax g)
  244.       | injSYM _ _ f => f
  245.     end.
  246.  
  247.   Fixpoint interpret_Semantics {X Y} (f : Semantics X Y) : Hom X Y :=
  248.     match f with
  249.       | nilSYM _ => identity C _
  250.       | consSYM _ _ _ s f => compose C _ _ _ s (interpret_Semantics f)
  251.     end.
  252.  
  253.   Theorem interpretation_factors_through_evaluation {X Y} (f : Syntax X Y) :
  254.     Hom_eq (interpret_Syntax f)
  255.            (interpret_Semantics (evalSYN f)).
  256.     induction f; simpl.
  257.     apply (equivalence_reflexivity (category_equivalence C _ _)).
  258.     eapply (equivalence_transitivity (category_equivalence C _ _)).
  259.     apply Compose_respectful_left.
  260.     apply IHf1.
  261.     eapply (equivalence_transitivity (category_equivalence C _ _)).
  262.     apply Compose_respectful_right.
  263.     apply IHf2.
  264.     Lemma append_pushthrough_compose {X Y Z} (f : Semantics X Y) (g : Semantics Y Z) :
  265.       Hom_eq (compose C _ _ _ (interpret_Semantics f) (interpret_Semantics g))
  266.              (interpret_Semantics (append f g)).
  267.       induction f; simpl.
  268.       apply category_left_identity.
  269.       eapply (equivalence_transitivity (category_equivalence C _ _)).
  270.       apply (equivalence_symmetry (category_equivalence C _ _)).
  271.       apply (category_associativity C).
  272.       apply Compose_respectful_right.
  273.       apply IHf.
  274.     Defined.
  275.     apply append_pushthrough_compose.
  276.    
  277.     apply (equivalence_symmetry (category_equivalence C _ _)).
  278.     apply category_right_identity.
  279.   Defined.
  280.  
  281.   Definition Interpret : Functor SYNTAX_category C.
  282.   Print Build_Functor.
  283.   apply (Build_Functor
  284.     SYNTAX_category C
  285.     (fun X => X)
  286.     (fun X Y f => interpret_Syntax f)
  287.   ).
  288.  
  289.   intros; apply (equivalence_reflexivity (category_equivalence C _ _)).
  290.   intros; apply (equivalence_reflexivity (category_equivalence C _ _)).
  291.  
  292.   intros X Y f f' E.
  293.   pose (quote_eval_equal f) as A.
  294.   pose (quote_eval_equal f') as B.
  295.   pose (interpretation_factors_through_evaluation f) as U.
  296.   pose (interpretation_factors_through_evaluation f') as V.
  297.   unfold Syntax_eq in *.
  298.   assert (
  299.     Hom_eq (interpret_Syntax f) (interpret_Semantics (evalSYN f'))
  300.   ) as P.
  301.   elim E.
  302.   assumption.
  303.   eapply (equivalence_transitivity (category_equivalence C _ _)).
  304.   apply P.
  305.   apply (equivalence_symmetry (category_equivalence C _ _)).
  306.   apply V.
  307.   Defined.
  308.  
  309. End SYMBOLIC.
  310.  
  311.  
  312. Section Trinkets.
  313.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
  314.  
  315.   Definition Isomorphism (X Y : Ob) (f : Hom X Y) :=
  316.     @Sigma (Hom Y X)
  317.     (fun (g : Hom Y X) =>
  318.       And (Hom_eq (compose C _ _ _ f g) (identity C _))
  319.           (Hom_eq (compose C _ _ _ g f) (identity C _))).
  320.  
  321.   Definition Exists {X Y : Ob} (P : Hom X Y -> Type) :=
  322.     @Sigma (Hom X Y) P.
  323.  
  324.   Definition ExistsUnique {X Y : Ob} (P : Hom X Y -> Type) :=
  325.     And (Exists P)
  326.         (forall f f' : Hom X Y,
  327.           P f -> P f' -> Hom_eq f f').
  328.  
  329.   Definition Terminal (C : @Category Ob Hom Hom_eq) (T : Ob) :=
  330.     forall X, ExistsUnique (fun f : Hom X T => True).
  331.  
  332.   Definition Initial (C : @Category Ob Hom Hom_eq) (T : Ob) :=
  333.     forall X, ExistsUnique (fun f : Hom T X => True).
  334.  
  335. End Trinkets.
  336.  
  337. Section OppositeCategory.
  338.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  339.  
  340.   Definition OppositeCategory : @Category C_Ob (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f).
  341.   apply (Build_Category
  342.     (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f)
  343.     (fun X => identity C X)
  344.     (fun X Y Z f g => compose C Z Y X g f)).
  345.   intros; apply Compose_respectful_right; assumption.
  346.   intros; apply Compose_respectful_left; assumption.
  347.   intros;
  348.     apply Build_Equivalence; destruct (category_equivalence C X Y);
  349.       hypothesis.
  350.   intros; apply category_right_identity.
  351.   intros; apply category_left_identity.
  352.   intros.
  353.   apply (equivalence_symmetry (category_equivalence C _ _)).
  354.   apply category_associativity.
  355.   Defined.
  356. End OppositeCategory.
  357.  
  358. Section Terminal_Initial_Stuff.
  359.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  360.   Definition Cop := OppositeCategory C.
  361.  
  362.   Theorem TerminalOp_Initial (L : C_Ob) :
  363.     Terminal Cop L -> Initial C L.
  364.     unfold Terminal; unfold Initial.
  365.     intros f X; destruct (f X) as [[g IPrf] gPrf].
  366.     constructor.
  367.     apply (witness _ g).
  368.     constructor.
  369.     apply gPrf.
  370.   Defined.
  371.  
  372.   Theorem InitialOp_Terminal (L : C_Ob) :
  373.     Initial Cop L -> Terminal C L.
  374.     unfold Terminal; unfold Initial.
  375.     intros f X; destruct (f X) as [[g IPrf] gPrf].
  376.     constructor.
  377.     apply (witness _ g).
  378.     constructor.
  379.     apply gPrf.
  380.   Defined.
  381.  
  382.   Theorem Terminal_unique_up_to_unique_isomorphism (T T' : C_Ob) :
  383.     Terminal C T -> Terminal C T' ->
  384.     ExistsUnique (Hom_eq := C_Hom_eq) (Isomorphism C T T').
  385.     unfold Terminal; unfold ExistsUnique.
  386.     intros Tprf T'prf.
  387.     destruct (Tprf T') as [[TprfA _] TprfB].
  388.     destruct (T'prf T) as [[T'prfA _] T'prfB].
  389.     constructor.
  390.    
  391.     apply (witness _ T'prfA).
  392.     apply (witness _ TprfA).
  393.     constructor; hypothesis; apply I.
  394.    
  395.     intros f f'; intros.
  396.     apply (T'prfB f f'); apply I.
  397.   Defined.
  398.  
  399. End Terminal_Initial_Stuff.
  400.  
  401. Section BijectionSubcategory.
  402.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
  403.  
  404.   Definition Bijection (X Y : Ob) := Exists (Isomorphism C X Y).
  405.  
  406.   Definition Invert_Bijection (X Y : Ob) : Bijection X Y -> Bijection Y X.
  407.   intros [f [g [p1 p2]]].
  408.   apply (witness _ g).
  409.   apply (witness _ f).
  410.   constructor; assumption.
  411.   Defined.
  412.  
  413.   Definition Identity_Bijection (X : Ob) : Bijection X X.
  414.   apply (witness _ (identity C X)).
  415.   apply (witness _ (identity C X)).
  416.   apply And_idem.
  417.   apply category_left_identity.
  418.   Defined.
  419.  
  420.   Definition Compose_Bijection (X Y Z : Ob)
  421.     (f : Bijection X Y) (g : Bijection Y Z) :
  422.     Bijection X Z.
  423.   unfold Bijection in *.
  424.   destruct f as [fTo [fFrom [fPrf fPrf']]].
  425.   destruct g as [gTo [gFrom [gPrf gPrf']]].
  426.   apply (witness _ (compose C _ _ _ fTo gTo)).
  427.   apply (witness _ (compose C _ _ _ gFrom fFrom)).
  428.  
  429.   Lemma Compose_Bijection_Lemma
  430.     (X Y Z : Ob)
  431.     (fTo : Hom X Y)
  432.     (fFrom : Hom Y X)
  433.     (fPrf : Hom_eq (compose C X Y X fTo fFrom) (identity C X))
  434.     (fPrf' : Hom_eq (compose C Y X Y fFrom fTo) (identity C Y))
  435.     (gTo : Hom Y Z)
  436.     (gFrom : Hom Z Y)
  437.     (gPrf : Hom_eq (compose C Y Z Y gTo gFrom) (identity C Y))
  438.       :
  439.     (Hom_eq
  440.       (compose C X Z X (compose C X Y Z fTo gTo)
  441.         (compose C Z Y X gFrom fFrom)) (identity C X)).
  442.  
  443.   pose (@SYNTAX_category Ob Hom) as SYN.
  444.   assert (
  445.     Syntax_eq
  446.      (compose SYN X Z X (compose SYN X Y Z (injSYM _ _ fTo) (injSYM _ _ gTo)) (compose SYN Z Y X (injSYM _ _ gFrom) (injSYM _ _ fFrom)))
  447.      (compose SYN _ _ _ (injSYM _ _ fTo)
  448.        (compose SYN _ _ _
  449.          (compose SYN _ _ _ (injSYM _ _ gTo) (injSYM _ _ gFrom))
  450.          (injSYM _ _ fFrom)))
  451.   ) as EQUATION by apply identical.
  452.   pose (Map_Hom_respectful (Interpret C) _ _ _ _ EQUATION) as EQUATION'; simpl in EQUATION'.
  453.  
  454.   eapply (equivalence_transitivity (category_equivalence C _ _)).
  455.   apply EQUATION'.
  456.   clear EQUATION'; clear EQUATION.
  457.  
  458.   eapply (equivalence_transitivity (category_equivalence C _ _)).
  459.   apply Compose_respectful_right.
  460.   apply Compose_respectful_left.
  461.   apply gPrf.
  462.  
  463.   eapply (equivalence_transitivity (category_equivalence C _ _)).
  464.   apply Compose_respectful_right.
  465.   apply category_left_identity.
  466.   apply fPrf.
  467.   Defined.
  468.  
  469.   apply both; apply Compose_Bijection_Lemma;
  470.     assumption.
  471.   Defined.
  472.  
  473.   Definition BijectionSubcategory :
  474.     @Category Ob Bijection
  475.     (fun (X Y : Ob) (f g : Bijection X Y) =>
  476.       Hom_eq (pi1 f) (pi1 g)).
  477.   apply (Build_Category
  478.     Bijection
  479.     (fun (X Y : Ob) (f g : Bijection X Y) =>
  480.       Hom_eq (pi1 f) (pi1 g))
  481.     (fun X => Identity_Bijection X)
  482.     (fun X Y Z f g => Compose_Bijection f g)).
  483.  
  484.   intros X Y Z f f' g.
  485.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  486.   destruct f' as [f'To [f'From [f'PrfTo f'PrfFrom]]].
  487.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  488.   simpl.
  489.   apply Compose_respectful_left.
  490.  
  491.   intros X Y Z f f' g.
  492.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  493.   destruct f' as [f'To [f'From [f'PrfTo f'PrfFrom]]].
  494.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  495.   simpl.
  496.   apply Compose_respectful_right.
  497.  
  498.   intros; apply Equivalence_Pullback.
  499.   apply (category_equivalence C).
  500.  
  501.   intros X Y.
  502.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  503.   simpl.
  504.   apply category_left_identity.
  505.  
  506.   intros X Y.
  507.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  508.   simpl.
  509.   apply category_right_identity.
  510.  
  511.   intros X Y Z W.
  512.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  513.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  514.   destruct h as [hTo [hFrom [hPrfTo hPrfFrom]]].
  515.   simpl.
  516.   apply category_associativity.
  517.   Defined.
  518.  
  519.   Definition BijectionSubcategory_Embedding : Functor BijectionSubcategory C.
  520.   apply (Build_Functor BijectionSubcategory C
  521.     (fun X => X)
  522.     (fun X Y f => pi1 f)); simpl; intros.
  523.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  524.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  525.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  526.   simpl.
  527.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  528.   assumption.
  529.   Defined.
  530.  
  531. End BijectionSubcategory.
  532.  
  533. Section Functors.
  534.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  535.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  536.   Context {E_Ob E_Hom E_Hom_eq} (E : @Category E_Ob E_Hom E_Hom_eq).
  537.  
  538.   Definition Constant_Functor (V : D_Ob) : Functor C D.
  539.   apply (Build_Functor C D
  540.     (fun _ => V)
  541.     (fun _ _ _ => identity D V)); intros.
  542.   apply (equivalence_reflexivity (category_equivalence D _ _)).
  543.   apply (equivalence_symmetry (category_equivalence D _ _)).
  544.   apply category_left_identity.
  545.   apply (equivalence_reflexivity (category_equivalence D _ _)).
  546.   Defined.
  547.  
  548.   Definition Identity_Functor : Functor C C.
  549.   apply (Build_Functor C C
  550.     (fun X => X)
  551.     (fun _ _ f => f)); intros.
  552.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  553.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  554.   assumption.
  555.   Defined.
  556.  
  557.   Definition Compose_Functors (F : Functor C D) (G : Functor D E) : Functor C E.
  558.   apply (Build_Functor C E
  559.     (fun X => Map_Ob G (Map_Ob F X))
  560.     (fun _ _ f => Map_Hom G _ _ (Map_Hom F _ _ f))); intros.
  561.  
  562.   apply (equivalence_transitivity (category_equivalence E _ _))
  563.     with (y := Map_Hom G _ _ (identity D _)).
  564.   apply Map_Hom_respectful.
  565.   apply (functor_identity F).
  566.   apply (functor_identity G).
  567.  
  568.   apply (equivalence_transitivity (category_equivalence E _ _))
  569.     with (y := Map_Hom G _ _ (compose D _ _ _
  570.       (Map_Hom F _ _ f) (Map_Hom F _ _ g))).
  571.   apply Map_Hom_respectful.
  572.   apply (functor_compose F).
  573.   apply (functor_compose G).
  574.  
  575.   apply Map_Hom_respectful.
  576.   apply Map_Hom_respectful.
  577.   assumption.
  578.   Defined.
  579.  
  580.   Definition Equal_Functors (F F' : Functor C D) : Type :=
  581.     @Sigma (forall X, Exists (Isomorphism D (Map_Ob F X) (Map_Ob F' X)))
  582.     (fun iso =>
  583.       forall X Y (f : C_Hom X Y),
  584.         D_Hom_eq
  585.           (compose D _ _ _ (Map_Hom F _ _ f) (pi1 (iso Y)))
  586.           (compose D _ _ _ (pi1 (iso X)) (Map_Hom F' _ _ f))).
  587.  
  588.   Theorem Equivalence_Equal_Functors : Equivalence Equal_Functors.
  589.     unfold Equal_Functors; apply Build_Equivalence.
  590.    
  591.     intro F; apply (witness _ (fun X => identity (BijectionSubcategory D) (Map_Ob F X))); simpl.
  592.     intros X Y f.
  593.     eapply (equivalence_transitivity (category_equivalence D _ _)).
  594.     apply category_right_identity.
  595.     apply (equivalence_symmetry (category_equivalence D _ _)).
  596.     apply category_left_identity.
  597.    
  598.     intros F G [a b].
  599.     apply (witness _ (fun X => Invert_Bijection (a X))).
  600.     intros X Y f.
  601.     generalize (b _ _ f).
  602.     destruct (a X) as [ax' [ax'' [ax''' ax'''']]].
  603.     destruct (a Y) as [ay' [ay'' [ay''' ay'''']]].
  604.     simpl.
  605.     Lemma eq_functors_lemma1
  606.       (F : Functor C D) (G : Functor C D)
  607.       (X : C_Ob) (Y : C_Ob) (f : C_Hom X Y)
  608.       (ax' : D_Hom (F @ X) (G @ X))
  609.       (ax'' : D_Hom (G @ X) (F @ X))
  610.       (ax''' : D_Hom_eq (ax' [D] ax'') (Id[D]))
  611.       (ax'''' : D_Hom_eq (ax'' [D] ax') (Id[D]))
  612.       (ay' : D_Hom (F @ Y) (G @ Y))
  613.       (ay'' : D_Hom (G @ Y) (F @ Y))
  614.       (ay''' : D_Hom_eq (ay' [D] ay'') (Id[D]))
  615.       (ay'''' : D_Hom_eq (ay'' [D] ay') (Id[D])) :
  616.       D_Hom_eq ((F $ f) [D] ay') (ax' [D] (G $ f)) ->
  617.       D_Hom_eq ((G $ f) [D] ay'') (ax'' [D] (F $ f)).
  618.       pose (@SYNTAX_category D_Ob D_Hom) as SYN.
  619.      
  620.       intro Q.
  621.       assert (
  622.         D_Hom_eq (ax'' [D] (((F $ f) [D] ay') [D] ay''))
  623.                  (ax'' [D] ((ax' [D] (G $ f)) [D] ay''))
  624.       ).
  625.       apply Compose_respectful_right.
  626.       apply Compose_respectful_left.
  627.       apply Q.
  628.      
  629.       assert (
  630.         D_Hom_eq (ax'' [D] ((ax' [D] (G $ f)) [D] ay''))
  631.                  (ax'' [D] (((F $ f) [D] ay') [D] ay''))
  632.       ).
  633.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  634.       apply Compose_respectful_right.
  635.       apply Compose_respectful_left.
  636.       apply (equivalence_symmetry (category_equivalence D _ _)).
  637.       apply Q.
  638.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  639.       Focus 2.
  640.       apply Compose_respectful_right.
  641.       apply Compose_respectful_left.
  642.       apply (equivalence_symmetry (category_equivalence D _ _)).
  643.       apply Q.
  644.       assumption.
  645.      
  646.       assert (
  647.         D_Hom_eq (ax'' [D] (((F $ f) [D] ay') [D] ay''))
  648.                  (ax'' [D] (F $ f))
  649.       ).
  650.       assert (
  651.         Syntax_eq ((injSYM _ _ ax'') [SYN] (((injSYM _ _ ((F $ f))) [SYN] (injSYM _ _ ay')) [SYN] (injSYM _ _ ay'')))
  652.                   (((injSYM _ _ ax'') [SYN] (injSYM _ _ ((F $ f)))) [SYN] ((injSYM _ _ ay') [SYN] (injSYM _ _ ay'')))
  653.       ) as EQUATION by apply identical.
  654.       pose (Map_Hom_respectful (Interpret D) _ _ _ _ EQUATION) as EQUATION'; simpl in EQUATION'.
  655.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  656.       apply EQUATION'.
  657.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  658.       Focus 2.
  659.       apply category_right_identity.
  660.       apply Compose_respectful_right.
  661.       assumption.
  662.      
  663.       assert (
  664.         D_Hom_eq (ax'' [D] ((ax' [D] (G $ f)) [D] ay''))
  665.                  ((G $ f) [D] ay'')
  666.       ).
  667.       assert (
  668.         Syntax_eq ((injSYM _ _ ax'') [SYN] (((injSYM _ _ ax') [SYN] (injSYM _ _ ((G $ f)))) [SYN] (injSYM _ _ ay'')))
  669.                   (((injSYM _ _ ax'') [SYN] (injSYM _ _ ax')) [SYN] ((injSYM _ _ ((G $ f)) [SYN] (injSYM _ _ ay''))))
  670.       ) as EQUATION by apply identical.
  671.       pose (Map_Hom_respectful (Interpret D) _ _ _ _ EQUATION) as EQUATION'; simpl in EQUATION'.
  672.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  673.       apply EQUATION'.
  674.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  675.       Focus 2.
  676.       apply category_left_identity.
  677.       apply Compose_respectful_left.
  678.       assumption.
  679.      
  680.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  681.       eapply (equivalence_symmetry (category_equivalence D _ _)).
  682.       apply X3.
  683.       eapply (equivalence_transitivity (category_equivalence D _ _)).
  684.       apply X1.
  685.       assumption.
  686.      
  687.     Defined.
  688.     apply eq_functors_lemma1; assumption.
  689.    
  690.     intros F G H [fg FG] [gh GH].
  691.     apply (witness _ (fun X => compose (BijectionSubcategory D) _ _ _
  692.       (fg X) (gh X))); simpl.
  693.     intros X Y f.
  694.     generalize (FG _ _ f).
  695.     generalize (GH _ _ f).
  696.     destruct (fg X) as [fgXF [fgXG [fgXPrf fpXPrf']]].
  697.     destruct (gh X) as [ghXF [ghXG [ghXPrf ghXPrf']]].
  698.     destruct (fg Y) as [fgYF [fgYG [fgYPrf fpYPrf']]].
  699.     destruct (gh Y) as [ghYF [ghYG [ghYPrf ghYPrf']]].
  700.     simpl.
  701.    
  702.     intros A B.
  703.  
  704.     eapply (equivalence_transitivity (category_equivalence D _ _)).
  705.     apply (category_associativity D).
  706.     eapply (equivalence_transitivity (category_equivalence D _ _)).
  707.     Focus 2.
  708.     apply (category_associativity D).
  709.      
  710.     eapply (equivalence_transitivity (category_equivalence D _ _)).
  711.     apply Compose_respectful_left.
  712.    
  713.     apply B.
  714.    
  715.     eapply (equivalence_transitivity (category_equivalence D _ _)).
  716.     apply (equivalence_symmetry (category_equivalence D _ _)).
  717.     apply (category_associativity D).
  718.    
  719.     apply Compose_respectful_right.
  720.     apply A.
  721.   Defined.
  722. End Functors.
  723.  
  724. Section NaturalTransformation.
  725.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  726.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  727.  
  728.   Context (F G : Functor C D).
  729.  
  730.   Record NaturalTransformation
  731.     := { Component : forall X : C_Ob, D_Hom (Map_Ob F X) (Map_Ob G X)
  732.        ; naturality : forall X Y (f : C_Hom X Y),
  733.          D_Hom_eq ((F $ f) [D] Component Y)
  734.                   (Component X [D] (G $ f))
  735.        }.  
  736. End NaturalTransformation.
  737.  
  738. Section NaturalTransformations.
  739.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  740.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  741.  
  742.   Context (F G H : Functor C D).
  743.  
  744.   Definition Identity_NaturalTransformation : NaturalTransformation F F.
  745.   apply (Build_NaturalTransformation F F
  746.     (fun X => identity D (F @ X))).
  747.   intros X Y f.
  748.   eapply (equivalence_transitivity (category_equivalence D _ _)).
  749.   apply category_right_identity.
  750.   eapply (equivalence_symmetry (category_equivalence D _ _)).
  751.   apply category_left_identity.
  752.   Defined.
  753.  
  754.   Definition Compose_NaturalTransformations
  755.     (FG : NaturalTransformation F G)
  756.     (GH : NaturalTransformation G H) :
  757.     NaturalTransformation F H.
  758.   apply (Build_NaturalTransformation F H
  759.     (fun X => Component FG X [D] Component GH X)).
  760.   intros X Y f.
  761.   eapply (equivalence_transitivity (category_equivalence D _ _)).
  762.   apply (category_associativity D).
  763.   eapply (equivalence_transitivity (category_equivalence D _ _)).
  764.   Focus 2.
  765.   apply (category_associativity D).
  766.   eapply (equivalence_transitivity (category_equivalence D _ _)).
  767.   apply Compose_respectful_left.
  768.   apply (naturality FG).
  769.   eapply (equivalence_transitivity (category_equivalence D _ _)).
  770.   eapply (equivalence_symmetry (category_equivalence D _ _)).
  771.   apply (category_associativity D).
  772.   apply Compose_respectful_right.
  773.   apply (naturality GH).
  774.   Defined.
  775. End NaturalTransformations.
  776.  
  777. Section FunctorCategory.
  778.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  779.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  780.  
  781.   Definition Funct : @Category (Functor C D) (fun F G => NaturalTransformation F G)
  782.     (fun F G eta nu =>
  783.       forall X, D_Hom_eq (Component eta X) (Component nu X)).
  784.   apply (@Build_Category (Functor C D) (fun F G => NaturalTransformation F G)
  785.     (fun F G eta nu =>
  786.       forall X, D_Hom_eq (Component eta X) (Component nu X))
  787.    
  788.     (fun F => Identity_NaturalTransformation F)
  789.     (fun F G H eta nu => Compose_NaturalTransformations eta nu)); simpl.
  790.  
  791.   intros; apply Compose_respectful_left; hypothesis.
  792.  
  793.   intros; apply Compose_respectful_right; hypothesis.
  794.  
  795.   intros; apply Build_Equivalence.
  796.   intros; apply (equivalence_reflexivity (category_equivalence D _ _)).
  797.   intros; apply (equivalence_symmetry (category_equivalence D _ _));
  798.     hypothesis.
  799.   intros; eapply (equivalence_transitivity (category_equivalence D _ _));
  800.     hypothesis.
  801.  
  802.   intros; apply category_left_identity.
  803.  
  804.   intros; apply category_right_identity.
  805.  
  806.   intros; apply category_associativity.
  807.   Defined.
  808. End FunctorCategory.
  809.  
  810. Section NaturalIsomorphism.
  811.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  812.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  813.  
  814.   Definition AUX_Category := Funct C D.
  815.  
  816.   Context (F G : Functor C D).
  817.   Context (eta : NaturalTransformation F G).
  818.  
  819.   Definition NaturalIsomorphism :=
  820.     Isomorphism AUX_Category _ _ eta.
  821.  
  822.   Definition NaturalIsomorphism' :=
  823.     forall X, Isomorphism D _ _ (Component eta X).
  824.  
  825.   Theorem NaturalIsomorphism_imp_NaturalIsomorphism' :
  826.     NaturalIsomorphism -> NaturalIsomorphism'.
  827.     unfold NaturalIsomorphism; unfold NaturalIsomorphism'.
  828.     unfold Isomorphism; simpl.
  829.     intros [f [prfF prfG]].
  830.     intro X.
  831.     apply (witness _ (Component f X)).
  832.     constructor; hypothesis.
  833.   Defined.
  834.  
  835.   Theorem NaturalIsomorphism'_imp_NaturalIsomorphism :
  836.     NaturalIsomorphism' -> NaturalIsomorphism.
  837.   unfold NaturalIsomorphism'; unfold NaturalIsomorphism.
  838.   unfold Isomorphism; intros S.
  839.   Lemma NaturalIsomorphism'_imp_NaturalIsomorphism_lemma
  840.     (S : forall X : C_Ob,
  841.       Sigma
  842.         (fun g : D_Hom (G @ X) (F @ X) =>
  843.          And (D_Hom_eq (Component eta X [D] g) (Id[D]))
  844.            (D_Hom_eq (g [D] Component eta X) (Id[D])))) :
  845.     NaturalTransformation G F.
  846.   apply (Build_NaturalTransformation G F
  847.     (fun X => pi1 (S X))).
  848.   intros X Y f.
  849.  
  850.   pose (naturality eta _ _ f).
  851.   destruct (pi2 (S X)) as [p q].
  852.   simpl in *.
  853.   destruct (pi2 (S Y)) as [m n].
  854.   eapply (eq_functors_lemma1 F G); hypothesis.
  855.   Defined.
  856.  
  857.   apply (witness _ (NaturalIsomorphism'_imp_NaturalIsomorphism_lemma S)).
  858.   constructor; intro X;
  859.     unfold NaturalIsomorphism'_imp_NaturalIsomorphism_lemma; simpl;
  860.     destruct (S X) as [t [u v]]; simpl;
  861.       assumption.
  862.   Defined.
  863. End NaturalIsomorphism.
  864.  
  865. Section Cone.
  866.   Context {II_Ob II_Hom II_Hom_eq} (II : @Category II_Ob II_Hom II_Hom_eq).
  867.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  868.  
  869.   Definition Cone (U : C_Ob) (D : Functor II C) := NaturalTransformation (Constant_Functor II C U) D.
  870.  
  871.   Definition DiagonalFunctor : Functor C (Funct II C).
  872.   Lemma DiagonalFunctor_lemma X Y :
  873.     C_Hom X Y -> NaturalTransformation (Constant_Functor II C X) (Constant_Functor II C Y).
  874.     intro f.
  875.     apply (Build_NaturalTransformation (Constant_Functor II C X) (Constant_Functor II C Y)
  876.       (fun X => f)).
  877.     intros X' Y' f'.
  878.     unfold Constant_Functor; simpl.
  879.     eapply (equivalence_transitivity (category_equivalence C _ _)).
  880.     apply category_left_identity.
  881.     eapply (equivalence_symmetry (category_equivalence C _ _)).
  882.     eapply (equivalence_transitivity (category_equivalence C _ _)).
  883.     apply category_right_identity.
  884.     eapply (equivalence_reflexivity (category_equivalence C _ _)).
  885.   Defined.
  886.   apply (Build_Functor C (Funct II C)
  887.     (fun V => Constant_Functor II C V)
  888.     (fun X Y f => DiagonalFunctor_lemma f)); simpl.
  889.   intros; apply (equivalence_reflexivity (category_equivalence C _ _)).
  890.   intros; apply (equivalence_reflexivity (category_equivalence C _ _)).
  891.   intros; assumption.
  892.   Defined.
  893.  
  894. End Cone.
  895.  
  896. Section CommaCategory.
  897.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  898.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  899.   Context {E_Ob E_Hom E_Hom_eq} (E : @Category E_Ob E_Hom E_Hom_eq).
  900.  
  901.   Context (F : Functor C E) (G : Functor D E).
  902.  
  903.   Definition Comma_Ob :=
  904.     @Sigma C_Ob (fun X =>
  905.       @Sigma D_Ob (fun Y =>
  906.         E_Hom (F @ X) (G @ Y))).
  907.  
  908.   Definition Comma_Map (P Q : Comma_Ob) :=
  909.     @Sigma (C_Hom (pi1 P) (pi1 Q)) (fun x =>
  910.       @Sigma (D_Hom (pi1 (pi2 P)) (pi1 (pi2 Q))) (fun y =>
  911.         E_Hom_eq ((F $ x) [E] (pi2 (pi2 Q)))
  912.                  ((pi2 (pi2 P)) [E] (G $ y)))).
  913.  
  914.   Definition Comma_eq P Q (f g : Comma_Map P Q) :=
  915.     And (C_Hom_eq (pi1 f) (pi1 g))
  916.         (D_Hom_eq (pi1 (pi2 f)) (pi1 (pi2 g))).
  917.  
  918.   Definition Comma_identity : forall X : Comma_Ob, Comma_Map X X.
  919.   unfold Comma_Ob; unfold Comma_Map.
  920.   intros [c [d p]]; simpl in *.
  921.   apply (witness _ (identity C _)).
  922.   apply (witness _ (identity D _)).
  923.  
  924.   eapply (equivalence_transitivity (category_equivalence E _ _)).
  925.   apply Compose_respectful_left.
  926.   apply (functor_identity F).
  927.   eapply (equivalence_transitivity (category_equivalence E _ _)).
  928.   apply category_left_identity.
  929.  
  930.   eapply (equivalence_transitivity (category_equivalence E _ _)).
  931.   Focus 2.
  932.   apply Compose_respectful_right.
  933.   eapply (equivalence_symmetry (category_equivalence E _ _)).
  934.   apply (functor_identity G).
  935.   eapply (equivalence_transitivity (category_equivalence E _ _)).
  936.   Focus 2.
  937.   eapply (equivalence_symmetry (category_equivalence E _ _)).
  938.   apply category_right_identity.
  939.  
  940.   eapply (equivalence_reflexivity (category_equivalence E _ _)).
  941.   Defined.
  942.  
  943.   Definition Comma_compose : forall X Y Z : Comma_Ob,
  944.     Comma_Map X Y -> Comma_Map Y Z -> Comma_Map X Z.
  945.   unfold Comma_Ob; unfold Comma_Map.
  946.   intros
  947.     [X [X' X'']]
  948.     [Y [Y' Y'']]
  949.     [Z [Z' Z'']]
  950.     [f [f' f'']]
  951.     [g [g' g'']]; simpl in *.
  952.   apply (witness _ (f [C] g)).
  953.   apply (witness _ (f' [D] g')).
  954.  
  955.   eapply (equivalence_transitivity (category_equivalence E _ _)).
  956.   apply Compose_respectful_left.
  957.   apply (functor_compose F).
  958.   eapply (equivalence_transitivity (category_equivalence E _ _)).
  959.   eapply (equivalence_symmetry (category_equivalence E _ _)).
  960.   apply (category_associativity E).
  961.   eapply (equivalence_transitivity (category_equivalence E _ _)).
  962.   apply Compose_respectful_right.
  963.   hypothesis.
  964.   eapply (equivalence_transitivity (category_equivalence E _ _)).
  965.   apply (category_associativity E).
  966.   eapply (equivalence_transitivity (category_equivalence E _ _)).
  967.   apply Compose_respectful_left.
  968.   hypothesis.
  969.   eapply (equivalence_transitivity (category_equivalence E _ _)).
  970.   eapply (equivalence_symmetry (category_equivalence E _ _)).
  971.   apply (category_associativity E).
  972.   eapply (equivalence_transitivity (category_equivalence E _ _)).
  973.   apply Compose_respectful_right.
  974.   eapply (equivalence_symmetry (category_equivalence E _ _)).
  975.   apply (functor_compose G).
  976.   eapply (equivalence_reflexivity (category_equivalence E _ _)).
  977.   Defined.
  978.  
  979.   Definition Comma : @Category Comma_Ob Comma_Map Comma_eq.
  980.   apply (@Build_Category Comma_Ob Comma_Map Comma_eq
  981.     Comma_identity Comma_compose).
  982.  
  983.   intros
  984.     [X [X' X'']]
  985.     [Y [Y' Y'']]
  986.     [Z [Z' Z'']]
  987.     [f [f' f'']]
  988.     [fp [fp' fp'']]
  989.     [g [g' g'']]; unfold Comma_eq in *; simpl in *.
  990.   intros [q q'].
  991.   constructor;
  992.     apply Compose_respectful_left; assumption.
  993.  
  994.   intros
  995.     [X [X' X'']]
  996.     [Y [Y' Y'']]
  997.     [Z [Z' Z'']]
  998.     [f [f' f'']]
  999.     [g [g' g'']]
  1000.     [gp [gp' gp'']]; unfold Comma_eq in *; simpl in *.
  1001.   intros [q q'].
  1002.   constructor;
  1003.     apply Compose_respectful_right; assumption.
  1004.  
  1005.   intros X Y.
  1006.   apply (Equivalence_Product
  1007.     (Equivalence_Pullback (fun f : Comma_Map X Y => pi1 f) (category_equivalence C _ _))
  1008.     (Equivalence_Pullback (fun f : Comma_Map X Y => pi1 (pi2 f)) (category_equivalence D _ _))).
  1009.  
  1010.   intros
  1011.     [X [X' X'']]
  1012.     [Y [Y' Y'']]
  1013.     [f [f' f'']]; unfold Comma_eq in *; simpl in *.
  1014.    constructor; apply category_left_identity.
  1015.  
  1016.    intros
  1017.      [X [X' X'']]
  1018.      [Y [Y' Y'']]
  1019.      [f [f' f'']]; unfold Comma_eq in *; simpl in *.
  1020.    constructor; apply category_right_identity.
  1021.    
  1022.    intros
  1023.      [X [X' X'']]
  1024.      [Y [Y' Y'']]
  1025.      [Z [Z' Z'']]
  1026.      [W [W' W'']]
  1027.      [f [f' f'']]
  1028.      [g [g' g'']]
  1029.      [h [h' h'']]; unfold Comma_eq in *; simpl in *.
  1030.    constructor; apply category_associativity.
  1031.    Defined.
  1032.    
  1033. End CommaCategory.
  1034.  
  1035. Section ONE.
  1036.   Definition ONE : @Category True (fun _ _ => True) (fun _ _ _ _ => True).
  1037.   apply Build_Category; try solve [ intros; apply I ].
  1038.   intros; apply Build_Equivalence; try solve [ intros; apply I ].
  1039.   Defined.
  1040. End ONE.
  1041.  
  1042. Section CONES.
  1043.   Context {II_Ob II_Hom II_Hom_eq} (II : @Category II_Ob II_Hom II_Hom_eq).
  1044.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  1045.  
  1046.   Context (F : Functor II C).
  1047.  
  1048.   Print DiagonalFunctor.
  1049.   Definition CONES := Comma (DiagonalFunctor II C) (Constant_Functor ONE (Funct II C) F).
  1050.  
  1051.   Definition CATEGORY_OBJECT {Ob Hom Hom_eq} : @Category Ob Hom Hom_eq -> Type := fun _ => Ob.
  1052.  
  1053.   Theorem Cone_CONE V : Cone V F -> (CATEGORY_OBJECT CONES).
  1054.     unfold CATEGORY_OBJECT.
  1055.     intros [c K].
  1056.     apply (witness _ V).
  1057.     apply (witness _ I).
  1058.     unfold DiagonalFunctor; simpl.
  1059.     apply (Build_NaturalTransformation _ _ c).
  1060.     apply K.
  1061.   Defined.
  1062.  
  1063.   Theorem CONE_Cone : CATEGORY_OBJECT CONES -> @Sigma C_Ob (fun V => Cone V F).
  1064.     unfold CATEGORY_OBJECT.
  1065.     unfold Comma_Ob.
  1066.     simpl.
  1067.     intros [x [_ p]].
  1068.     apply (witness _ x).
  1069.     apply p.
  1070.   Defined.
  1071.  
  1072.   Definition UniversalCone := Initial CONES.
  1073.  
  1074. End CONES.
  1075.  
  1076. Inductive Bool := TT | FF.
  1077.  
  1078. Section TWO.
  1079.   Definition TWO : @Category Bool (fun a b =>
  1080.     match a with
  1081.       | TT => match b with
  1082.                 | TT => True
  1083.                 | FF => False
  1084.               end
  1085.       | FF => match b with
  1086.                 | TT => False
  1087.                 | FF => True
  1088.               end
  1089.     end) (fun _ _ _ _ => True).
  1090.   apply Build_Category; try solve [ intros;
  1091.     repeat match goal with b : Bool |- _ => destruct b end;
  1092.       constructor ].
  1093.   intros X Y Z; destruct X; destruct Y; destruct Z; intros; try constructor;
  1094.     match goal with f : False |- _ => elim f end.
  1095.   intros; apply Build_Equivalence; intros; apply I.
  1096.   Defined.
  1097. End TWO.
  1098.  
  1099. (*
  1100. Section TWO.
  1101.   Definition TWO : @Category Bool (fun _ _ => Bool -> Bool) (fun _ _ f g => And (Identity (f TT) (g TT)) (Identity (f FF) (g FF))).
  1102.   apply (@Build_Category Bool (fun _ _ => Bool -> Bool) (fun _ _ f g => And (Identity (f TT) (g TT)) (Identity (f FF) (g FF)))
  1103.     (fun _ b => b)
  1104.     (fun _ _ _ f g x => g (f x)));
  1105.   intros;
  1106.     repeat match goal with H : And _ _ |- _ => destruct H end;
  1107.       try solve [ constructor;
  1108.         do 2 repeat match goal with H : Identity _ _ |- _ => elim H; clear H end;
  1109.           constructor ].
  1110.  
  1111.   constructor.
  1112.   destruct (f TT); assumption.
  1113.   destruct (f FF); assumption.
  1114.  
  1115.   apply (Equivalence_Product);
  1116.     apply Equivalence_Pullback;
  1117.       apply Equivalence_Identity.
  1118.   Defined.
  1119. End TWO.
  1120. *)
  1121.  
  1122. Section PRODUCT_Limit.
  1123.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  1124.   Context (A B : C_Ob).
  1125.  
  1126.   Definition FOB := (fun b =>
  1127.       match b with
  1128.         | TT => A
  1129.         | FF => B
  1130.       end).
  1131.   Definition F : Functor TWO C.
  1132.   apply (Build_Functor TWO C
  1133.     FOB
  1134.     (fun X Y =>
  1135.       match X,Y with
  1136.         | TT,TT => fun _ => identity C A
  1137.         | FF,FF => fun _ => identity C B
  1138.         | TT,FF => fun f => False_rect _ f
  1139.         | FF,TT => fun f => False_rect _ f
  1140.       end)); simpl; intros;
  1141.   repeat match goal with b : Bool |- _ => destruct b end; simpl;
  1142.     repeat match goal with f : False |- _ => elim f end.
  1143.  
  1144.   apply (equivalence_reflexivity).
  1145.   apply (category_equivalence C).
  1146.  
  1147.   apply (equivalence_reflexivity).
  1148.   apply (category_equivalence C).
  1149.  
  1150.   apply (equivalence_symmetry).
  1151.   apply (category_equivalence C).
  1152.   apply category_left_identity.
  1153.  
  1154.   apply (equivalence_symmetry).
  1155.   apply (category_equivalence C).
  1156.   apply category_left_identity.
  1157.  
  1158.   apply (equivalence_reflexivity).
  1159.   apply (category_equivalence C).
  1160.  
  1161.   apply (equivalence_reflexivity).
  1162.   apply (category_equivalence C).
  1163.   Defined.
  1164.  
  1165.   Definition Product := UniversalCone (F := F).
  1166. End PRODUCT_Limit.
  1167.  
  1168. Section Nat.
  1169.  
  1170.   Inductive Nat : Set :=
  1171.   | Z : Nat
  1172.   | S : Nat -> Nat.
  1173.  
  1174. End Nat.
  1175.  
  1176. Section Fin.
  1177.  
  1178.   Inductive Fin : Nat -> Set :=
  1179.   | FZ : forall {n}, Fin (S n)
  1180.   | FS : forall {n}, Fin n -> Fin (S n).
  1181.  
  1182.   Definition FIN : @Category
  1183.     Nat
  1184.     (fun n m => Fin n -> Fin m)
  1185.     (fun n m i j => forall k, Identity (i k) (j k)).
  1186.   apply (Build_Category
  1187.     (fun n m => Fin n -> Fin m)
  1188.     (fun n m i j => forall k, Identity (i k) (j k))
  1189.     (fun n i => i)
  1190.     (fun n m w i j k => j (i k))).
  1191.  
  1192.   intros X Y Z f f' g H k.
  1193.   elim (H k).
  1194.   constructor.
  1195.  
  1196.   intros X Y Z f g g' H k.
  1197.   elim (H (f k)).
  1198.   constructor.
  1199.  
  1200.   intros; apply (Equivalence_Fiber).
  1201.   apply Equivalence_Identity.
  1202.  
  1203.   intros; constructor.
  1204.  
  1205.   intros; constructor.
  1206.  
  1207.   intros; constructor.
  1208.   Defined.
  1209.  
  1210. End Fin.
  1211.  
  1212.  
  1213.  
  1214. (*
  1215. *** Local Variables: ***
  1216. *** coq-prog-args: ("-emacs-U" "-nois") ***
  1217. *** End: ***
  1218. *)
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!