Merge pull request #117 from patrick-nicodemus/UniversalProperty

Functor/Hom.v

@@ -2,6 +2,7 @@ Require Import Category.Lib.
 Require Import Category.Theory.Category.
 Require Import Category.Theory.Functor.
 Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Theory.Isomorphism.
 Require Import Category.Construction.Product.
 Require Import Category.Construction.Opposite.
 Require Import Category.Instance.Fun.
@@ -74,6 +75,23 @@ Proof.
     now rewrite Fnat, id_right).
 Defined.
 
+Corollary Yoneda_Embedding' (C: Category) (c d : C) :
+  @IsIsomorphism Sets {| carrier := hom d c |}
+                 {| carrier := hom (fobj[C] c) (fobj[C] d) |}
+                 {| morphism := @fmap _ _ (Curried_Hom C) c d;
+                            proper_morphism := fmap_respects _ _ |}.
+Proof.
+  apply bijective_is_iso.
+  - abstract(assert (H := Yoneda_Faithful C); constructor;
+             intros x y eq; apply H; exact eq).
+  - constructor. simpl. 
+    intro A; exists (@prefmap _ _ _ (Yoneda_Full C) _ _ A ).
+    abstract(intros x f; unfold op;
+             assert (M := @fmap_sur _ _ _ (Yoneda_Full C));
+             specialize M with _ _ A; simpl in M;
+             unfold op in M; apply M).
+Defined.
+
 Program Definition CoHom_Alt `(C : Category) : C ∏ C^op ⟶ Sets :=
   Hom C ◯ Swap.
 
@@ -83,23 +101,9 @@ Program Definition CoHom `(C : Category) : C ∏ C^op ⟶ Sets := {|
   fmap := fun x y (f : x ~{C ∏ C^op}~> y) =>
     {| morphism := fun g => snd f ∘ g ∘ fst f |}
 |}.
+Next Obligation. now rewrite <- ! comp_assoc. Qed.
 
-Program Definition Curried_CoHom `(C : Category) : C ⟶ [C^op, Sets] := {|
-  fobj := fun x => {|
-    fobj := fun y => {| carrier := @hom (C^op) x y
-                      ; is_setoid := @homset (C^op) x y |};
-    fmap := fun y z (f : y ~{C^op}~> z) =>
-              {| morphism := fun (g : x ~{C^op}~> y) =>
-                               (f ∘ g) : x ~{C^op}~> z |}
-  |};
-  fmap := fun x y (f : x ~{C}~> y) => {|
-    transform := fun _ => {| morphism := fun g => g ∘ op f |}
-  |}
-|}.
-Next Obligation.
-  simpl; intros.
-  symmetry.
-  now rewrite !comp_assoc.
-Qed.
+Definition Curried_CoHom `(C : Category) : C ⟶ [C^op, Sets] :=
+  Curried_Hom C^op.
 
 Notation "[Hom ─ , A ]" := (@Curried_CoHom _ A) : functor_scope.

Instance/Fun/Cartesian.v

@@ -0,0 +1,107 @@
+Require Import Category.Lib.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Functor.
+Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Instance.Sets.
+Require Import Category.Instance.Fun.
+Require Import Category.Structure.Cartesian.
+Require Import Category.Lib.Tactics2.
+
+Proposition fmap_respects' (C D : Category) (F : C ⟶ D) : forall (x y : C) (f g: hom x y),
+    f ≈ g -> fmap[F] f ≈ fmap[F] g.
+Proof. now apply fmap_respects. Defined.
+#[export] Hint Resolve fmap_respects' : cat.
+
+Proposition ump_product' (C : Category) `{@Cartesian C} (x y z: C)
+  (h h': z ~> x × y) : (exl ∘ h) ≈ (exl ∘ h') -> (exr ∘ h) ≈ (exr ∘ h') -> h ≈ h'.
+Proof.
+  intros.
+  assert (RW: h ≈ fork (exl ∘ h) (exr ∘ h)). {
+  apply (snd (ump_products _ _ _)); split; reflexivity.
+  }
+  rewrite RW; symmetry.
+  apply (snd (ump_products _ _ _)); split; symmetry; assumption. 
+Qed.
+
+Proposition ump_product_auto1 (C : Category) `{@Cartesian C} (x y z: C)
+  (h : z ~> x × y) (f : z ~> x) (g : z ~> y) : (exl ∘ h) ≈ f -> (exr ∘ h) ≈ g -> h ≈ fork f g.
+Proof.
+  intros. apply (snd (ump_products _ _ _)); split; trivial.
+Qed.
+
+Proposition ump_product_auto2 (C : Category) `{@Cartesian C} (x y z: C)
+  (h : z ~> x × y) (f : z ~> x) (g : z ~> y) : (exl ∘ h) ≈ f -> (exr ∘ h) ≈ g -> fork f g ≈ h.
+Proof.
+  intros. symmetry. apply (snd (ump_products _ _ _)); split; trivial.
+Qed.
+
+#[export] Hint Resolve ump_product_auto1 : cat.
+#[export] Hint Resolve ump_product_auto2 : cat.
+(* #[export] Hint Resolve ump_product' : cat. *)
+
+#[export] Hint Rewrite @exl_fork_assoc  : categories.
+#[export] Hint Rewrite @exl_fork_comp : categories.
+#[export] Hint Rewrite @exr_fork_assoc  : categories.
+#[export] Hint Rewrite @exr_fork_comp : categories.
+
+Proposition ump_product_auto3 (C : Category) `{@Cartesian C}
+ (c d p q: C) (h : c ~> d) (f : d ~> p) (g : d ~> q) (k : c ~> p × q) :
+ f ∘ h ≈ exl ∘ k -> g ∘ h ≈ exr ∘ k -> (fork f g ∘ h) ≈ k.
+Proof.
+  intros H1 H2.
+  rewrite <- fork_comp.
+  apply ump_product_auto2; symmetry; assumption.
+Qed.
+
+Proposition ump_product_auto4 (C : Category) `{@Cartesian C}
+ (c d p q: C) (h : c ~> d) (f : d ~> p) (g : d ~> q) (k : c ~> p × q) :
+ f ∘ h ≈ exl ∘ k -> g ∘ h ≈ exr ∘ k -> k ≈ (fork f g ∘ h).
+Proof.
+  intros H1 H2.
+  rewrite <- fork_comp.
+  apply ump_product_auto1; symmetry; assumption.
+Qed.
+
+#[export] Hint Resolve ump_product_auto3 : cat.
+#[export] Hint Resolve ump_product_auto4 : cat.
+
+Ltac component_of_nat_trans :=
+  match goal with
+  | [ H : @Transform ?C ?D ?F ?G |- @hom ?D (fobj[?F] ?x) (fobj[?G] ?x) ] => apply H
+  end.
+#[export] Hint Extern 1 (hom (fobj[ _ ] ?x) (fobj[ _ ] ?x)) => component_of_nat_trans : cat.
+#[local] Hint Rewrite @fmap_comp : categories.
+#[local] Hint Rewrite @exl_split : categories.
+#[local] Hint Rewrite @exr_split : categories.
+
+#[export]
+Instance Functor_Category_Cartesian (C D : Category) (_ : @Cartesian D) : @Cartesian (@Fun C D).
+Proof.
+  unshelve econstructor.
+  - simpl. intros F G. unshelve econstructor.
+    + exact (fun c => fobj[F] c × fobj[G] c).
+    + exact (fun x y f => Cartesian.split (fmap[F] f) (fmap[G] f)).
+    + abstract(intros x y; repeat(intro); apply split_respects; auto with cat).
+    + abstract(intro; simpl; unfold split; auto with cat).
+    + abstract(intros x y z f g; simpl; unfold split; auto with cat).
+  - intros F G H σ τ. cbn in *.
+    unshelve econstructor; simpl.
+    + intro x. simpl. auto with cat.
+    + abstract(intros x y f;
+      unfold split; autorewrite with categories;
+      apply ump_product_auto3; autorewrite with categories;
+        destruct σ, τ; auto). 
+    + abstract(intros x y f; destruct σ, τ; unfold split; auto with cat).
+  - simpl. intros F G; unshelve econstructor.
+    + intro a. simpl. exact exl.
+    + abstract(simpl; intros; now autorewrite with categories).
+    + abstract(simpl; intros; now autorewrite with categories).
+  - simpl; intros F G. unshelve econstructor.
+    + intro a. simpl. exact exr.
+    + abstract(simpl; intros; now autorewrite with categories).
+    + abstract(simpl; intros; now autorewrite with categories).
+  - abstract(simpl; repeat(intro); simpl; auto with cat).
+  - simpl. intros F G H s t fk. split.
+    + abstract(intro l; split; intro; rewrite l; now autorewrite with categories).
+    + abstract(intros [l1 l2] x; rewrite <- l1, <- l2; auto with cat).
+Defined.

Instance/Sets.v

@@ -267,6 +267,18 @@ Proof.
     constructor.
 Qed.
 
+Lemma bijective_is_iso {A B : SetoidObject} (h : A ~{Sets}~> B) :
+  injective h -> surjective h -> IsIsomorphism h.
+Proof.
+  intros [i] [lift] ; unshelve econstructor.
+  - exists (fun b => `1 (lift b)).
+    abstract(intros a b eq; simpl;
+    apply i; now rewrite `2 (lift a), `2 (lift b)).
+  - abstract(intro x; now rewrite `2 (lift x)).
+  - abstract(intro x; apply i; now rewrite `2 (lift (h x))).
+Defined.
+
+
 Lemma surjectivity_is_epic@{h p} {A B : SetoidObject@{p p}}
   (h : A ~{Sets}~> B) :
   (∀ b, ∃ a, h a ≈ b)%type ↔ Epic@{h p} h.
@@ -284,7 +296,7 @@ Proof.
        aws (https://mathoverflow.net/users/30790/aws)
        In the category of sets epimorphisms are surjective - Constructive Proof?
        URL (version: 2014-08-18): https://mathoverflow.net/q/178786 *)
-    intros [epic] ?.
+    intros [epic] ?. 
     given (C : SetoidObject). {
       refine {|
         carrier := Type;
@@ -294,25 +306,24 @@ Proof.
       |}.
       equivalence.
     }
-(*
-    given (f : B ~{Sets}~> C). {
-      refine {|
-        morphism := λ b, ∃ a, h a ≈ b
-      |}.
-    }
-    given (g : B ~{Sets}~> C). {
-      refine {|
-        morphism := λ _, True
-      |}.
-    }
-    specialize (epic C f g).
-    enough ((f ∘[Sets] h) ≈ (g ∘[Sets] h)). {
-      specialize (epic X b); clear X.
-      unfold f, g in epic.
-      simpl in *.
-      now rewrite epic.
-    }
-    intro.
-    unfold f, g; simpl.
-*)
+
+    (* given (f : B ~{Sets}~> C). { *)
+    (*   refine {| *)
+    (*     morphism := λ b, ∃ a, h a ≈ b *)
+    (*   |}. *)
+    (* } *)
+    (* given (g : B ~{Sets}~> C). { *)
+    (*   refine {| *)
+    (*     morphism := λ _, True *)
+    (*   |}. *)
+    (* } *)
+    (* specialize (epic C f g). *)
+    (* enough ((f ∘[Sets] h) ≈ (g ∘[Sets] h)). { *)
+    (*   specialize (epic X b); clear X. *)
+    (*   unfold f, g in epic. *)
+    (*   simpl in *. *)
+    (*   now rewrite epic. *)
+    (* } *)
+    (* intro. *)
+    (* unfold f, g; simpl. *)
 Abort.

Lib/Setoid.v

@@ -64,3 +64,11 @@ Arguments uniqueness {_ _ _} _.
 
 Notation "∃! x .. y , P" := (Unique (fun x => .. (Unique (fun y => P)) ..))
   (at level 200, x binder, y binder, right associativity) : category_theory_scope.
+
+Local Set Warnings "-not-a-class".
+Class injective {A : Type} `{Setoid A} {B : Type} `{Setoid B} (f : A -> B) :=
+  { inj {x y} :> f x ≈ f y -> x ≈ y }.
+
+Class surjective {A : Type} {B : Type} `{Setoid B} (f : A -> B) :=
+  { surj {y} :> { x & f x ≈ y} }.
+Local Set Warnings "not-a-class".

Lib/Tactics2.v

@@ -0,0 +1,74 @@
+Require Import Category.Lib.
+Require Import Category.Instance.Sets.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Functor.
+Require Import Category.Structure.Cartesian.
+
+#[export] Hint Extern 1 => reflexivity : core.
+
+Ltac compose_reduce :=
+  multimatch goal with
+  | [ f : @hom ?C ?x ?y  |- @hom ?C ?x ?z ] => refine (@compose C x y z _ f)
+  | [ f : @hom ?C ?y ?z  |- @hom ?C ?x ?z ] => apply (@compose C x y z f)
+  end.
+
+Create HintDb cat discriminated.
+
+#[export]
+Hint Extern 1 (@hom _ _ _) => compose_reduce : cat.
+
+Ltac apply_setoid_morphism := 
+  match goal with
+  | [ H : context[SetoidMorphism ] |- _ ] =>  apply H
+  end.
+
+#[export]
+Hint Extern 20 => apply_setoid_morphism : cat.
+
+(* This is tempting but the "proper" script calls
+   intuition, which calls auto with *, so "proper" 
+   should probably be a top-level command only. *)
+(* Hint Extern 1 (Proper _ _) => proper : cat. *)
+(* Similarly with cat_simpl. *)
+(* Hint Extern 20 => progress(cat_simpl) : cat. *)
+(* Hint Extern 40 (@hom _ _ _) => hom_to_homset : cat. *)
+#[export] Hint Immediate id : cat.
+
+Ltac split_exists := unshelve eapply existT.
+#[export] Hint Extern 1 (@sigT _ _) => split_exists : cat.
+
+Ltac functor_simpl :=
+  match goal with
+  | [ |- context[@fobj _ _ (Build_Functor _ _ _ _ _ _ _)]] => unfold fobj
+  | [ |- context[@fmap _ _ (Build_Functor _ _ _ _ _ _ _)]] => unfold fmap
+  end.
+#[export] Hint Extern 10 => functor_simpl : cat.
+#[export] Hint Extern 10 (hom _ _ _) => progress(simpl hom) : cat.
+#[export] Hint Extern 40 => progress(cbn in *) : cat.
+#[export] Hint Extern 4 (SetoidMorphism _ _) => unshelve eapply Build_SetoidMorphism : cat.
+#[export] Hint Extern 4 (hom _ (_ × _)) => apply fork : cat.
+#[export] Hint Unfold forall_relation : cat.
+#[export] Hint Extern 1 (@equiv _ _ _ _) => reflexivity : cat.
+#[export] Hint Extern 1 (@equiv _ (@homset _ _ _) (@compose _ _ _ _ _ _) (@compose _ _ _ _ _ _))
+     => simple apply compose_respects : cat.
+
+Ltac compose_respects_script :=
+first [repeat(rewrite <- comp_assoc);
+       apply compose_respects; try(reflexivity)
+      |repeat(rewrite -> comp_assoc);
+       apply compose_respects; try(reflexivity)].
+
+#[export] Hint Extern 20 (@equiv _ (@homset _ _ _) (@compose _ _ _ _ _ _) (@compose _ _ _ _ _ _))
+     => compose_respects_script : cat.    
+
+#[export] Hint Extern 10 => progress(autorewrite with categories) : cat.
+#[export] Hint Extern 5 => (progress(simplify)) : cat.
+#[export] Hint Rewrite <- @comp_assoc : categories.
+Ltac unfold_proper :=
+  match goal with
+  | [ H : Proper _ ?f |- ?f _ ≈ ?f _ ] => unfold Proper, "==>" in H; simpl in H; assert (QQ:= H)
+  | [ H : Proper _ ?f |- ?f _ _ ≈ ?f _ _ ] => unfold Proper, "==>", forall_relation in H;
+                                              simpl in H; assert (QQ:= H)
+  end; solve [auto with cat].
+#[export] Hint Extern 4 (@equiv _ _ (?f _) (?f _)) => unfold_proper : cat.
+

Structure/Cartesian.v

@@ -25,7 +25,27 @@ Class Cartesian := {
 
   ump_products {x y z} (f : x ~> y) (g : x ~> z) (h : x ~> y × z) :
     h ≈ fork f g ↔ (exl ∘ h ≈ f) * (exr ∘ h ≈ g)
-}.
+  }.
+
+Class IsCartesianProduct (x y z : C) := {
+  fork' {a} (f : a ~> x) (g : a ~> y) : a ~> z;
+
+  exl'  : z ~> x;
+  exr'  : z ~> y;
+
+  fork'_respects : ∀ a,
+    Proper (equiv ==> equiv ==> equiv) (@fork' a);
+
+  ump_product {a} (f : a ~> x) (g : a ~> y) (h : a ~> z) :
+    h ≈ fork' f g ↔ (exl' ∘ h ≈ f) * (exr' ∘ h ≈ g)
+  }.
+
+Program Instance CartesianProductStructuresEquiv (x y z : C) :
+  Setoid (IsCartesianProduct x y z) :=
+  ({|
+             equiv := fun p q => (@exl' _ _ _ p) ≈ (@exl' _ _ _ q) ∧
+                                 (@exr' _ _ _ p) ≈ (@exr' _ _ _ q) |}).
+
 #[export] Existing Instance fork_respects.
 
 Infix "×" := product_obj (at level 41, right associativity) : object_scope.
@@ -378,3 +398,29 @@ Ltac unfork :=
   unfold swap, split, first, second; simpl;
   repeat (rewrite <- !fork_comp; cat;
           rewrite <- !comp_assoc; cat).
+
+Section ACartesian.
+  Proposition exl'_fork {C : Category} {w x y z: C} {H : IsCartesianProduct x y z}
+    (f : w ~> x) (g : w ~> y) :
+    exl' ∘ fork' f g ≈ f.
+  Proof.
+    intros. now apply (ump_product f g ).
+  Qed.
+
+  Proposition exr'_fork {C : Category} {w x y z: C} {H : IsCartesianProduct x y z}
+    (f : w ~> x) (g : w ~> y) :
+    exr' ∘ fork' f g ≈ g.
+  Proof.
+    intros. now apply (ump_product f g).
+  Qed.
+
+  Proposition fork'_natural (C: Category) (v w x y z: C) (H: IsCartesianProduct x y z)
+    (f : v ~> w) (a : w ~> x) (b : w ~> y) :
+    fork' a b ∘ f ≈ fork' (a ∘ f) (b ∘ f).
+  Proof.
+    apply ump_product; split; rewrite comp_assoc.
+    - now rewrite exl'_fork.
+    - now rewrite exr'_fork.
+  Qed.
+
+End ACartesian.