Need a unique gift idea?
A Pastebin account makes a great Christmas gift
SHARE
TWEET

Untitled

a guest Jul 7th, 2017 69 Never
Upgrade to PRO!
ENDING IN00days00hours00mins00secs
 
  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. Section Trinkets.
  293.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
  294.  
  295.   Definition Isomorphism (X Y : Ob) (f : Hom X Y) :=
  296.     @Sigma (Hom Y X)
  297.     (fun (g : Hom Y X) =>
  298.       And (Hom_eq (compose C _ _ _ f g) (identity C _))
  299.           (Hom_eq (compose C _ _ _ g f) (identity C _))).
  300.  
  301.   Definition Exists {X Y : Ob} (P : Hom X Y -> Type) :=
  302.     @Sigma (Hom X Y) P.
  303.  
  304.   Definition ExistsUnique {X Y : Ob} (P : Hom X Y -> Type) :=
  305.     And (Exists P)
  306.         (forall f f' : Hom X Y,
  307.           P f -> P f' -> Hom_eq f f').
  308.  
  309.   Definition Terminal (C : @Category Ob Hom Hom_eq) (T : Ob) :=
  310.     forall X, ExistsUnique (fun f : Hom X T => True).
  311.  
  312.   Definition Initial (C : @Category Ob Hom Hom_eq) (T : Ob) :=
  313.     forall X, ExistsUnique (fun f : Hom T X => True).
  314.  
  315. End Trinkets.
  316.  
  317. Section OppositeCategory.
  318.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  319.  
  320.   Definition OppositeCategory : @Category C_Ob (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f).
  321.   apply (Build_Category
  322.     (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f)
  323.     (fun X => identity C X)
  324.     (fun X Y Z f g => compose C Z Y X g f)).
  325.   intros; apply Compose_respectful_right; assumption.
  326.   intros; apply Compose_respectful_left; assumption.
  327.   intros;
  328.     apply Build_Equivalence; destruct (category_equivalence C X Y);
  329.       hypothesis.
  330.   intros; apply category_right_identity.
  331.   intros; apply category_left_identity.
  332.   intros.
  333.   apply (equivalence_symmetry (category_equivalence C _ _)).
  334.   apply category_associativity.
  335.   Defined.
  336. End OppositeCategory.
  337.  
  338. Section Terminal_Initial_Dual.
  339.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  340.   Definition Cop := OppositeCategory C.
  341.  
  342.   Theorem TerminalOp_Initial (L : C_Ob) :
  343.     Terminal Cop L -> Initial C L.
  344.     unfold Terminal; unfold Initial.
  345.     intros f X; destruct (f X) as [[g IPrf] gPrf].
  346.     constructor.
  347.     apply (witness _ g).
  348.     constructor.
  349.     apply gPrf.
  350.   Defined.
  351.  
  352.   Theorem InitialOp_Terminal (L : C_Ob) :
  353.     Initial Cop L -> Terminal C L.
  354.     unfold Terminal; unfold Initial.
  355.     intros f X; destruct (f X) as [[g IPrf] gPrf].
  356.     constructor.
  357.     apply (witness _ g).
  358.     constructor.
  359.     apply gPrf.
  360.   Defined.
  361.  
  362. End Terminal_Initial_Dual.
  363.  
  364. Section BijectionSubcategory.
  365.   Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).
  366.  
  367.   Definition Bijection (X Y : Ob) := Exists (Isomorphism C X Y).
  368.  
  369.   Definition Invert_Bijection (X Y : Ob) : Bijection X Y -> Bijection Y X.
  370.   intros [f [g [p1 p2]]].
  371.   apply (witness _ g).
  372.   apply (witness _ f).
  373.   constructor; assumption.
  374.   Defined.
  375.  
  376.   Definition Identity_Bijection (X : Ob) : Bijection X X.
  377.   apply (witness _ (identity C X)).
  378.   apply (witness _ (identity C X)).
  379.   apply And_idem.
  380.   apply category_left_identity.
  381.   Defined.
  382.  
  383.   Definition Compose_Bijection (X Y Z : Ob)
  384.     (f : Bijection X Y) (g : Bijection Y Z) :
  385.     Bijection X Z.
  386.   unfold Bijection in *.
  387.   destruct f as [fTo [fFrom [fPrf fPrf']]].
  388.   destruct g as [gTo [gFrom [gPrf gPrf']]].
  389.   apply (witness _ (compose C _ _ _ fTo gTo)).
  390.   apply (witness _ (compose C _ _ _ gFrom fFrom)).
  391.  
  392.   Lemma Compose_Bijection_Lemma
  393.     (X Y Z : Ob)
  394.     (fTo : Hom X Y)
  395.     (fFrom : Hom Y X)
  396.     (fPrf : Hom_eq (compose C X Y X fTo fFrom) (identity C X))
  397.     (fPrf' : Hom_eq (compose C Y X Y fFrom fTo) (identity C Y))
  398.     (gTo : Hom Y Z)
  399.     (gFrom : Hom Z Y)
  400.     (gPrf : Hom_eq (compose C Y Z Y gTo gFrom) (identity C Y))
  401.       :
  402.     (Hom_eq
  403.       (compose C X Z X (compose C X Y Z fTo gTo)
  404.         (compose C Z Y X gFrom fFrom)) (identity C X)).
  405.  
  406.   pose (@SYNTAX_category Ob Hom) as SYN.
  407.   assert (
  408.     Syntax_eq
  409.      (compose SYN X Z X (compose SYN X Y Z (injSYM _ _ fTo) (injSYM _ _ gTo)) (compose SYN Z Y X (injSYM _ _ gFrom) (injSYM _ _ fFrom)))
  410.      (compose SYN _ _ _ (injSYM _ _ fTo)
  411.        (compose SYN _ _ _
  412.          (compose SYN _ _ _ (injSYM _ _ gTo) (injSYM _ _ gFrom))
  413.          (injSYM _ _ fFrom)))
  414.   ) as EQUATION by apply identical.
  415.   pose (Map_Hom_respectful (Interpret C) _ _ _ _ EQUATION) as EQUATION'; simpl in EQUATION'.
  416.  
  417.   eapply (equivalence_transitivity (category_equivalence C _ _)).
  418.   apply EQUATION'.
  419.   clear EQUATION'; clear EQUATION.
  420.  
  421.   eapply (equivalence_transitivity (category_equivalence C _ _)).
  422.   apply Compose_respectful_right.
  423.   apply Compose_respectful_left.
  424.   apply gPrf.
  425.  
  426.   eapply (equivalence_transitivity (category_equivalence C _ _)).
  427.   apply Compose_respectful_right.
  428.   apply category_left_identity.
  429.   apply fPrf.
  430.   Defined.
  431.  
  432.   apply both; apply Compose_Bijection_Lemma;
  433.     assumption.
  434.   Defined.
  435.  
  436.   Definition BijectionSubcategory :
  437.     @Category Ob Bijection
  438.     (fun (X Y : Ob) (f g : Bijection X Y) =>
  439.       Hom_eq (pi1 f) (pi1 g)).
  440.   apply (Build_Category
  441.     Bijection
  442.     (fun (X Y : Ob) (f g : Bijection X Y) =>
  443.       Hom_eq (pi1 f) (pi1 g))
  444.     (fun X => Identity_Bijection X)
  445.     (fun X Y Z f g => Compose_Bijection f g)).
  446.  
  447.   intros X Y Z f f' g.
  448.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  449.   destruct f' as [f'To [f'From [f'PrfTo f'PrfFrom]]].
  450.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  451.   simpl.
  452.   apply Compose_respectful_left.
  453.  
  454.   intros X Y Z f f' g.
  455.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  456.   destruct f' as [f'To [f'From [f'PrfTo f'PrfFrom]]].
  457.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  458.   simpl.
  459.   apply Compose_respectful_right.
  460.  
  461.   intros; apply Equivalence_Pullback.
  462.   apply (category_equivalence C).
  463.  
  464.   intros X Y.
  465.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  466.   simpl.
  467.   apply category_left_identity.
  468.  
  469.   intros X Y.
  470.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  471.   simpl.
  472.   apply category_right_identity.
  473.  
  474.   intros X Y Z W.
  475.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  476.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  477.   destruct h as [hTo [hFrom [hPrfTo hPrfFrom]]].
  478.   simpl.
  479.   apply category_associativity.
  480.   Defined.
  481.  
  482.   Definition BijectionSubcategory_Embedding : Functor BijectionSubcategory C.
  483.   apply (Build_Functor BijectionSubcategory C
  484.     (fun X => X)
  485.     (fun X Y f => pi1 f)); simpl; intros.
  486.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  487.   destruct f as [fTo [fFrom [fPrfTo fPrfFrom]]].
  488.   destruct g as [gTo [gFrom [gPrfTo gPrfFrom]]].
  489.   simpl.
  490.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  491.   assumption.
  492.   Defined.
  493.  
  494. End BijectionSubcategory.
  495.  
  496. Section Functors.
  497.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  498.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  499.   Context {E_Ob E_Hom E_Hom_eq} (E : @Category E_Ob E_Hom E_Hom_eq).
  500.  
  501.   Definition Constant_Functor (V : C_Ob) : Functor C C.
  502.   apply (Build_Functor C C
  503.     (fun _ => V)
  504.     (fun _ _ _ => identity C V)); intros.
  505.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  506.   apply (equivalence_symmetry (category_equivalence C _ _)).
  507.   apply category_left_identity.
  508.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  509.   Defined.
  510.  
  511.   Definition Identity_Functor : Functor C C.
  512.   apply (Build_Functor C C
  513.     (fun X => X)
  514.     (fun _ _ f => f)); intros.
  515.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  516.   apply (equivalence_reflexivity (category_equivalence C _ _)).
  517.   assumption.
  518.   Defined.
  519.  
  520.   Definition Compose_Functors (F : Functor C D) (G : Functor D E) : Functor C E.
  521.   apply (Build_Functor C E
  522.     (fun X => Map_Ob G (Map_Ob F X))
  523.     (fun _ _ f => Map_Hom G _ _ (Map_Hom F _ _ f))); intros.
  524.  
  525.   apply (equivalence_transitivity (category_equivalence E _ _))
  526.     with (y := Map_Hom G _ _ (identity D _)).
  527.   apply Map_Hom_respectful.
  528.   apply (functor_identity F).
  529.   apply (functor_identity G).
  530.  
  531.   apply (equivalence_transitivity (category_equivalence E _ _))
  532.     with (y := Map_Hom G _ _ (compose D _ _ _
  533.       (Map_Hom F _ _ f) (Map_Hom F _ _ g))).
  534.   apply Map_Hom_respectful.
  535.   apply (functor_compose F).
  536.   apply (functor_compose G).
  537.  
  538.   apply Map_Hom_respectful.
  539.   apply Map_Hom_respectful.
  540.   assumption.
  541.   Defined.
  542.  
  543.   Definition Equal_Functors (F F' : Functor C D) : Type :=
  544.     @Sigma (forall X, Exists (Isomorphism D (Map_Ob F X) (Map_Ob F' X)))
  545.     (fun iso =>
  546.       forall X Y (f : C_Hom X Y),
  547.         D_Hom_eq
  548.           (compose D _ _ _ (Map_Hom F _ _ f) (pi1 (iso Y)))
  549.           (compose D _ _ _ (pi1 (iso X)) (Map_Hom F' _ _ f))).
  550.  
  551.   Theorem Equivalence_Equal_Functors : Equivalence Equal_Functors.
  552.     unfold Equal_Functors; apply Build_Equivalence.
  553.    
  554.     intro F; apply (witness _ (fun X => identity (BijectionSubcategory D) (Map_Ob F X))); simpl.
  555.     intros X Y f.
  556.     eapply (equivalence_transitivity (category_equivalence D _ _)).
  557.     apply category_right_identity.
  558.     apply (equivalence_symmetry (category_equivalence D _ _)).
  559.     apply category_left_identity.
  560.    
  561.     intros F G [a b].
  562.     apply (witness _ (fun X => Invert_Bijection (a X))).
  563.     intros X Y f.
  564.     generalize (b _ _ f).
  565.     destruct (a X) as [ax' [ax'' [ax''' ax'''']]].
  566.     destruct (a Y) as [ay' [ay'' [ay''' ay'''']]].
  567.     simpl.
  568.     Lemma eq_functors_lemma1
  569.       (F : Functor C D) (G : Functor C D)
  570.       (X : C_Ob) (Y : C_Ob) (f : C_Hom X Y)
  571.       (ax' : D_Hom (F @ X) (G @ X))
  572.       (ax'' : D_Hom (G @ X) (F @ X))
  573.       (ax''' : D_Hom_eq (ax' [D] ax'') (Id[D]))
  574.       (ax'''' : D_Hom_eq (ax'' [D] ax') (Id[D]))
  575.       (ay' : D_Hom (F @ Y) (G @ Y))
  576.       (ay'' : D_Hom (G @ Y) (F @ Y))
  577.       (ay''' : D_Hom_eq (ay' [D] ay'') (Id[D]))
  578.       (ay'''' : D_Hom_eq (ay'' [D] ay') (Id[D])) :
  579.       D_Hom_eq ((F $ X) Y f [D] ay') (ax' [D] (G $ X) Y f) ->
  580.       D_Hom_eq ((G $ X) Y f [D] ay'') (ax'' [D] (F $ X) Y f).
  581.     Admitted.
  582.     apply eq_functors_lemma1; assumption.
  583.    
  584.     intros F G H [fg FG] [gh GH].
  585.     apply (witness _ (fun X => compose (BijectionSubcategory D) _ _ _
  586.       (fg X) (gh X))); simpl.
  587.     intros X Y f.
  588.     destruct (fg X) as [fgXF [fgXG [fgXPrf fpXPrf']]].
  589.     destruct (gh X) as [ghXF [ghXG [ghXPrf ghXPrf']]].
  590.     destruct (fg Y) as [fgYF [fgYG [fgYPrf fpYPrf']]].
  591.     destruct (gh Y) as [ghYF [ghYG [ghYPrf ghYPrf']]].
  592.     simpl.
  593.     Lemma eq_functors_lemma2
  594.       (F : Functor C D) (G : Functor C D) (H : Functor C D)
  595.       (X : C_Ob) (Y : C_Ob) (f : C_Hom X Y)
  596.       (fgXF : D_Hom (F @ X) (G @ X))
  597.       (fgXG : D_Hom (G @ X) (F @ X))
  598.       (fgXPrf : D_Hom_eq (fgXF [D] fgXG) (Id[D]))
  599.       (fpXPrf' : D_Hom_eq (fgXG [D] fgXF) (Id[D]))
  600.       (ghXF : D_Hom (G @ X) (H @ X))
  601.       (ghXG : D_Hom (H @ X) (G @ X))
  602.       (ghXPrf : D_Hom_eq (ghXF [D] ghXG) (Id[D]))
  603.       (ghXPrf' : D_Hom_eq (ghXG [D] ghXF) (Id[D]))
  604.       (fgYF : D_Hom (F @ Y) (G @ Y))
  605.       (fgYG : D_Hom (G @ Y) (F @ Y))
  606.       (fgYPrf : D_Hom_eq (fgYF [D] fgYG) (Id[D]))
  607.       (fpYPrf' : D_Hom_eq (fgYG [D] fgYF) (Id[D]))
  608.       (ghYF : D_Hom (G @ Y) (H @ Y))
  609.       (ghYG : D_Hom (H @ Y) (G @ Y))
  610.       (ghYPrf : D_Hom_eq (ghYF [D] ghYG) (Id[D]))
  611.       (ghYPrf' : D_Hom_eq (ghYG [D] ghYF) (Id[D])) :
  612.       D_Hom_eq ((F $ X) Y f [D] (fgYF [D] ghYF))
  613.       ((fgXF [D] ghXF) [D] (H $ X) Y f).
  614.     Admitted.
  615.     eapply eq_functors_lemma2; hypothesis.
  616.   Defined.
  617. End Functors.
  618.  
  619.  
  620.  
  621. (*
  622. *** Local Variables: ***
  623. *** coq-prog-args: ("-emacs-U" "-nois") ***
  624. *** End: ***
  625. *)
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top