limits.v

   1 Require Import Morphisms.
   2 Require Import RelationClasses.
   3 Require Import Equivalence.
   4 Require Import Setoid.
   5
   6 (* Eelis *)
   7 Require Import categories abstract_algebra functors.
   8 (* me *)
   9 Require Import constant_functor unit_category.
  10 Require functor_category.
  11
  12 Set Automatic Introduction.
  13
  14 Section yonedad.
  15 Context `{Category A} `{Category J}.
  16
  17 Import functor_category.
  18 (*Let Object := functor_category.Object J A.*)
  19 (*Let Arrow (F G : Object) := functor_category.Arrow F G.*)
  20
  21 Definition F (a:A) : Object J A := functor_category.object (fun _:J=>a) _ _.
  22
  23 Global Instance F': Fmap F := fun (a a':A) (f:a ⟶ a') => functor_category.arrow (F a) (F a')
  24   (fun (j:J) => f) constant_transformation.
  25
  26 Existing Instance functor_category.Category_instance_0.
  27
  28 Global Instance: Functor F F'.
  29 Proof. do 4 stuff; [stuff | stuff| do 4 stuff| do 3 stuff ]. Qed.
  30
  31 End yonedad.
  32
  33 Require categories.setoid.
  34 Require comma.
  35
  36 Section lim.
  37 Context `{Category J}.
  38 Context `{!Functor (X:J->setoid.Object) X'}.
  39
  40 Let l := fun x:setoid.Object => functor_category.object (F x) _ _.
  41 Let r := fun _:unit => functor_category.object X X' Functor0.
  42
  43 Let Slice := comma.Object (l:=l) (r:=r).
  44
  45 Require Import theory.setoids.
  46 Let x_t := {u :forall j:J, X j | forall (j k: J) (f:j⟶k), proj1_sig (fmap X f) (u j) =  u k}.
  47 Let sss : Setoid x_t := sig_Setoid _.
  48 Existing Instance sss.
  49
  50 Let x := setoid.object x_t _ sss.
  51
  52 Ltac apply_head := repeat intro; match goal with [ H:_ |- _] => idtac H; apply H end.
  53  Ltac stuff := simpl || apply_head || intuition || trivial || constructor || reflexivity || id_rewrite || comp_rewrite || hyp_rewrite || intro.
  54
  55 Let Fx := fun j:J, x.
  56 Let etaj (j:J) (a:x) : X j := proj1_sig a j.
  57 Section etaj.
  58 Context (j:J).
  59 Global Instance: Setoid_Morphism (etaj j).
  60 Proof. repeat stuff. Qed.
  61 End etaj.
  62
  63 Let eta : Fx ⇛ X :=  (fun j:J => exist Setoid_Morphism (etaj j) _).
  64 Global Instance: NaturalTransformation eta.
  65 Proof.
  66 intros j j' f; intros m n Hmn.
  67 simpl. unfold Basics.compose.
  68 unfold etaj.
  69 rewrite (proj2_sig n j j').
  70 intuition.
  71 Qed.
  72
  73 Let Feta := (functor_category.arrow (F x) (functor_category.object X X' _) eta _).
  74 Let co := comma.object (r:= fun _ => functor_category.object X _ _) x tt  Feta.
  75
  76 Section initarrow.
  77 Context (y:Slice).
  78 Let xinx_t (a: comma.Lobj y) (j:J) : X j := proj1_sig (comma.Cmap y j) a.
  79
  80 Lemma inx_t (a: comma.Lobj y) (j k: J) (f:j⟶k) : (` (fmap X f)) (xinx_t a j) = (xinx_t a k).
  81 Proof.
  82   unfold xinx_t.
  83   set (Cmap := (comma.Cmap y)).
  84   set (Robj := r (comma.Robj y)).
  85   set (Lobj := l (comma.Lobj y)).
  86   assert (eq (fmap X f) (fmap Robj f)) by reflexivity; hyp_rewrite.
  87   change (` (fmap Robj f ◎ Cmap j) a = ` (Cmap k) a).
  88   transitivity (` (Cmap k ◎ fmap Lobj f) a).
  89     symmetry; apply (natural (η:=functor_category.eta _ _ (comma.Cmap y)) _ _ _ a); auto.
  90     stuff; stuff. reflexivity.
  91 Qed.
  92
  93 Definition aa (a : comma.Lobj y) : x_t := exist _ _ (inx_t a).
  94 Global Instance: Setoid_Morphism (Beq:= sig_equiv _) aa.
  95 Proof.
  96   stuff. stuff.
  97   constructor; apply _.
  98   apply _.
  99   intros b b' Hb j. simpl.
 100   unfold xinx_t.
 101   pose (proj2_sig (comma.Cmap y j)); rewrite Hb.
 102   reflexivity.
 103 Qed.
 104
 105 Program Let aaE : l (comma.Lobj y) ⇛ Fx :=  (fun j:J => exist Setoid_Morphism aa _).
 106 Global Instance: NaturalTransformation aaE.
 107 Proof.
 108   intros s t f g g' Hg j; simpl.
 109   unfold xinx_t.
 110   pose (proj2_sig (comma.Cmap y j)); rewrite Hg.
 111   reflexivity.
 112 Qed.
 113
 114 End initarrow.
 115
 116
 117 Require dual.
 118
 119
 120
 121 Let II : initial (Arrows0:=dual.flipA) co.
 122 Proof.
 123   intro y.
 124
 125
 126
 127