API tools faq
paste
Advertisement
Guest User

Untitled

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