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

Untitled

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