Merge pull request #113 from patrick-nicodemus/Quiver

Quiver

Instance/StrictCat.v

@@ -0,0 +1,32 @@
+Require Import Category.Lib.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Isomorphism.
+Require Import Category.Theory.Functor.
+
+Generalizable All Variables.
+
+(* StrictCat is the category of categories, with setoid structure given by
+   objectwise equality.
+
+    objects               Categories
+    arrows                Functors
+    arrow equivalence     Pointwise equality of objects
+    identity              Identity Functor
+    composition           Horizontal composition of Functors
+ *)
+
+#[export]
+Instance StrictCat : Category := {
+  obj     := Category;
+  hom     := @Functor;
+  homset  := @Functor_StrictEq_Setoid;
+  id      := @Id;
+  compose := @Compose;
+
+  compose_respects := @Compose_respects_stricteq;
+  id_left          := @fun_strict_equiv_id_left;
+  id_right         := @fun_strict_equiv_id_right;
+  comp_assoc       := @fun_strict_equiv_comp_assoc;
+  comp_assoc_sym   := fun a b c d f g h =>
+    symmetry (@fun_strict_equiv_comp_assoc a b c d f g h)
+}.

Lib/TList.v

@@ -11,31 +11,32 @@ Open Scope lazy_bool_scope.
 
 Set Transparent Obligations.
 
-Inductive tlist {A : Type} (B : A → A → Type) : A → A → Type :=
-  | tnil : ∀ i : A, tlist i i
-  | tcons : ∀ i j k : A, B i j → tlist j k → tlist i k.
+Inductive tlist' {A :Type} {B : A → A → Type} (k : A) : A -> Type :=
+| tnil : tlist' k
+| tcons : ∀ i j : A, B i j -> tlist' j -> tlist' i.
 
-Derive Signature NoConfusion Subterm for tlist.
+Definition tlist {A : Type} (B : A → A → Type) (i j : A) := @tlist' A B j i.
+
+Derive Signature NoConfusion Subterm for tlist'.
 Next Obligation.
   apply Transitive_Closure.wf_clos_trans.
   intros a.
-  destruct a as [[] pr0].
+  destruct a as [? pr0].
+  (* destruct a as [[] pr0]. *)
   simpl in pr0.
   induction pr0.
   - (* tnil *)
     constructor.
     intros y H.
     inversion H; subst; clear H.
   - (* tcons *)
-    constructor.
-    intros [[l m] pr1] H.
-    simpl in *.
-    dependent induction H.
+    constructor. intros [ l m] pr1 . simpl in *.
+    dependent induction pr1.
     assumption.
 Defined.
 
-Arguments tnil {A B i}.
-Arguments tcons {A B i} j {k} _ _.
+Arguments tnil {A B k}.
+Arguments tcons {A B k} i {j} x xs.
 
 Notation "x ::: xs" := (tcons _ x xs) (at level 60, right associativity).
 
@@ -50,6 +51,12 @@ Fixpoint tlist_length {i j} (xs : tlist B i j) : nat :=
   | tcons x _ xs => 1 + tlist_length xs
   end.
 
+Definition tlist_singleton {i j} (x : B i j) : tlist B i j := x ::: tnil.
+
+Equations tlist_rcons {i j k} (xs : tlist B i j) (y : B j k) : tlist B i k :=
+  tlist_rcons tnil y := y ::: (@tnil _ B k);
+  tlist_rcons (@tcons _ _ _ _ _ x xs) y := x ::: tlist_rcons xs y.
+
 Equations tlist_app {i j k} (xs : tlist B i j) (ys : tlist B j k) :
   tlist B i k :=
   tlist_app tnil ys := ys;
@@ -122,8 +129,8 @@ Equations tlist_eq_dec {i j : A} (x y : tlist B i j) : {x = y} + {x ≠ y} :=
   tlist_eq_dec tnil tnil := left eq_refl;
   tlist_eq_dec tnil _ := in_right;
   tlist_eq_dec _ tnil := in_right;
-  tlist_eq_dec (@tcons _ _ _ m _ x xs) (@tcons _ _ _ o _ y ys)
-    with @eq_dec _ AE m o := {
+  tlist_eq_dec (@tcons _ _ _ _ m x xs) (@tcons _ _ _ _ o y ys)
+  with @eq_dec _ AE m o := {
       | left H with @eq_dec _ (BE _ _) x (rew <- [fun x => B _ x] H in y) := {
           | left _ with tlist_eq_dec xs (rew <- [fun x => tlist B x _] H in ys) := {
              | left _ => left _;
@@ -137,9 +144,7 @@ Next Obligation.
   simpl_eq; intros.
   apply n.
   inv H.
-  apply Eqdep_dec.inj_pair2_eq_dec in H1; [|apply eq_dec].
-  apply Eqdep_dec.inj_pair2_eq_dec in H1; [|apply eq_dec].
-  assumption.
+  apply Eqdep_dec.inj_pair2_eq_dec in H1; [ assumption |apply eq_dec].
 Defined.
 Next Obligation.
   simpl_eq; intros.
@@ -181,7 +186,7 @@ Equations tlist_equiv {i j : A} (x y : tlist B i j) : Type :=
   tlist_equiv tnil tnil := True;
   tlist_equiv tnil _ := False;
   tlist_equiv _ tnil := False;
-  tlist_equiv (@tcons _ _ _ m _ x xs) (@tcons _ _ _ o _ y ys)
+  tlist_equiv (@tcons _ _ _ _ m x xs) (@tcons _ _ _ _ o y ys)
     with eq_dec m o := {
       | left H =>
          equiv x (rew <- [fun x => B _ x] H in y) *
@@ -203,12 +208,12 @@ Next Obligation.
     + apply IHx.
 Qed.
 Next Obligation.
-  repeat intro.
+  intros x y X.
   induction x; simpl.
   - dependent elimination y as [tnil]; auto.
   - dependent elimination y as [tcons _ y ys]; auto.
     rewrite tlist_equiv_equation_4 in *.
-    destruct (eq_dec j _); [|contradiction].
+    destruct (eq_dec j0 _); [|contradiction].
     subst.
     rewrite EqDec.peq_dec_refl.
     destruct X.
@@ -224,7 +229,7 @@ Next Obligation.
     simpl; intros.
     dependent elimination z as [tcons _ z zs]; auto.
     rewrite tlist_equiv_equation_4 in *.
-    destruct (eq_dec j _); [|contradiction].
+    destruct (eq_dec j0 _); [|contradiction].
     destruct (eq_dec _ _); [|contradiction].
     subst.
     rewrite EqDec.peq_dec_refl.
@@ -260,7 +265,7 @@ Next Obligation.
   - contradiction.
   - rewrite <- !tlist_app_comm_cons.
     rewrite tlist_equiv_equation_4 in *.
-    destruct (eq_dec j j0); [|contradiction].
+    destruct (eq_dec j0 j1); [|contradiction].
     subst.
     destruct X.
     split; auto.

Theory/Adjunction.v

@@ -57,6 +57,40 @@ Class Adjunction@{o3 h3 p3 so sh sp} := {
     ⌈fmap[U] f ∘ g⌉ ≈ f ∘ ⌈g⌉
 }.
 
+Definition Build_Adjunction'
+  (adj : forall x y,
+    @Isomorphism Sets
+      {| carrier := @hom C (F x) y; is_setoid := @homset C (F x) y |}
+      {| carrier := @hom D x (U y); is_setoid := @homset D x (U y) |})
+  (to_adj_nat_l : forall x y z (f : F y ~> z) (g : x ~> y),
+      (to (adj _ _)  (f ∘ fmap[F] g) ≈ (to (adj _ _) f) ∘ g))
+  (to_adj_nat_r : forall x y z (f : y ~> z) (g : F x ~> y),
+      (to (adj _ _) (f ∘ g) ≈ fmap[U] f ∘ (to (adj _ _) g)))
+  : Adjunction.
+Proof.
+  unshelve eapply Build_Adjunction.
+  + apply to_adj_nat_l.
+  + apply to_adj_nat_r.
+  + intros x y z f g.
+    set (f' := from (adj y z) f).
+    apply ((snd (@injectivity_is_monic _ _ (adj x z))) _).
+    change (to (adj x z) (from (adj x z) _)) with
+      (((adj x z) ∘ (from (adj x z))) (f ∘ g)).
+    rewrite ((iso_to_from (adj x z)) (f ∘ g)); simpl;
+    rewrite to_adj_nat_l.
+    refine (compose_respects _ _ _ g _ (Equivalence_Reflexive _)).
+    unfold f'; symmetry.
+    exact ((iso_to_from (adj y z)) f).
+  + intros x y z f g.
+    set (g' :=  from (adj x y) g).
+    apply ((snd (@injectivity_is_monic _ _ (adj x z))) _).
+    rewrite (iso_to_from (adj x z) (fmap[U] f ∘ g)); simpl.
+    rewrite to_adj_nat_r.
+    apply (compose_respects (fmap[U] f) _ (Equivalence_Reflexive _)).
+    unfold g'; symmetry;
+      apply (iso_to_from (adj x y) g).
+Defined.
+
 Context `{@Adjunction}.
 
 Notation "⌊ f ⌋" := (to adj f).

Theory/Functor.v

@@ -1,6 +1,7 @@
 Require Import Category.Lib.
 Require Import Category.Theory.Category.
 Require Import Category.Theory.Isomorphism.
+Require Import Equations.Prop.Logic.
 
 Generalizable All Variables.
 
@@ -317,3 +318,171 @@ Corollary ToAFunctor_FromAFunctor `{H : AFunctor F} :
 Proof. reflexivity. Qed.
 
 End AFunctor.
+
+Section StrictEq.
+ Lemma transport_adjunction (A : Type) (B : A -> Type) (R: forall a :A, crelation (B a)) :
+   forall (a a' : A) (p : a = a') (x : B a) (y : B a'),
+    ((R _ x (transport_r B p y) -> R _ (transport B p x) y)) *
+      (R _ (transport B p x) y -> (R _ x (transport_r B p y))).
+  intros a a' p x y. split.
+  - destruct p. now unfold transport_r.
+  - destruct p. now unfold transport_r.
+Defined.
+
+Lemma transport_relation_exchange (A : Type) (R : crelation A) :
+  forall (a a' b b': A) (p : a = b) (q : a' = b') (t : R a a'),
+    transport (fun z => R b z) q
+      (transport (fun k => R k a') p t) =
+      transport (fun k => R k b') p
+        (transport (fun z => R a z) q t).
+Proof.
+  intros a a' b b' p q t; destruct p, q; reflexivity.
+Defined.
+
+Lemma transport_trans (A : Type) (B : A -> Type) :
+  forall (a0 a1 a2 : A) (x : B a0) (p : a0 = a1) (q : a1 = a2),
+    transport B q (transport B p x) = transport B (eq_trans p q) x.
+Proof.
+  intros a0 a1 a2 x p q; destruct p, q; reflexivity.
+Defined.
+
+Lemma transport_r_trans (A : Type) (B : A -> Type) :
+  forall (a0 a1 a2 : A) (x : B a2) (p : a0 = a1) (q : a1 = a2),
+    transport_r B p (transport_r B q x) = transport_r B (eq_trans p q) x.
+Proof.
+  intros a0 a1 a2 x p q; destruct p, q; reflexivity.
+Defined.
+
+Global Instance proper_transport (A : Type) (B : A -> Type) (S : forall a : A, Setoid (B a)) :
+  forall (a a' : A) (p : a = a'), Proper (equiv ==> equiv) (transport B p).
+Proof.
+  intros a b p. destruct p. now unfold transport.
+Defined.
+
+Global Instance proper_transport_r (A : Type) (B : A -> Type) (S : forall a : A, Setoid (B a)) :
+  forall (a a' : A) (p : a = a'), Proper (equiv ==> equiv) (transport_r B p).
+Proof.
+  intros a b p. destruct p. now (unfold transport_r).
+Defined.
+
+(* Global Instance proper_transport_hom_cod (C : Category) (c d d': C) (p : d = d')  *)
+(*   : Proper (equiv ==> equiv) (transport (fun z => hom c z) p). *)
+(* Proof. *)
+(*   destruct p. now trivial. *)
+(* Defined. *)
+
+(* Global Instance proper_transport_hom_dom (C : Category) (c c' d: C) (p : c = c')  *)
+(*   : Proper (equiv ==> equiv) (transport (fun z => hom z d) p). *)
+(* Proof. *)
+(*   destruct p. now trivial. *)
+(* Defined. *)
+
+#[export] Instance proper_transport_dom (A: Type) (B : A -> A -> Type)
+  (S : forall i j, Setoid (B i j)) (c c' d : A) (p : c = c') :
+  Proper (equiv ==> equiv) (Logic.transport (fun z => B z d) p).
+Proof.
+  destruct p. now trivial.
+Defined.
+
+#[export] Instance proper_transport_cod (A: Type) (B : A -> A -> Type)
+  (S : forall i j, Setoid (B i j)) (c d d' : A) (p : d = d') :
+  Proper (equiv ==> equiv) (Logic.transport (fun z => B c z) p).
+Proof.
+  destruct p. now trivial.
+Defined.
+
+Program Instance Functor_StrictEq_Setoid {C D : Category} : Setoid (C ⟶ D) := {
+    equiv := fun F G =>
+      { eq_on_obj : ∀ x : C, F x = G x
+                  & ∀ (x y : C) (f : x ~> y),
+            transport (fun z => hom (fobj[ F ] x) z) (eq_on_obj y) (fmap[F] f) ≈ 
+                   (transport_r (fun z => hom z (fobj[G] y)) (eq_on_obj x) (fmap[G] f)) }
+}.
+Next Obligation.
+  equivalence.
+  - unfold transport_r. rewrite eq_sym_involutive.
+    fold (transport_r (λ z : obj[D], fobj[y] x1 ~{ D }~> z) (x0 y0)).
+    symmetry. 
+    rename x into F, y into G, x0 into eq_ob, x1 into x, y0 into y. 
+    refine ((snd
+               (transport_adjunction D (hom (fobj[G] x))
+                  (fun d t s => t ≈ s) _ _ _ _ _)) _).
+    rewrite transport_relation_exchange.
+    refine ((fst
+               (transport_adjunction D (fun d' => hom d' (fobj[G] y))
+                  (fun d t s => t ≈ s) _ _ _ _ _)) _).
+    exact (e _ _ _).
+  - exact(eq_trans (x1 x2) (x0 x2)).
+  - rename x into F, y into G, z into H, x1 into F_eq_ob_G,
+      e0 into F_eq_ob_G_resp_mor, x0 into G_eq_ob_H,
+      e into G_eq_ob_H_resp_mor, x2 into domf, y0 into codf.
+    simpl.
+    rewrite <- transport_trans, <- transport_r_trans.
+    rewrite F_eq_ob_G_resp_mor.
+    unfold transport_r at 1 2. rewrite transport_relation_exchange.
+    apply proper_transport_dom.
+    apply G_eq_ob_H_resp_mor.
+Defined.
+
+Lemma transport_f_equal (A B : Type) (C : B -> Type) (f : A -> B)
+  (x y : A) (p : x = y) (t : C (f x))
+  : transport (fun a => C (f a)) p t = transport (fun b => C b) (f_equal f p) t.
+Proof.
+  destruct p. reflexivity.
+Defined.
+
+Lemma transport_functorial_dom (C D: Category) (F : @Functor C D) (c c' d : C)
+  (p : c = c') (f : hom c d)
+  : fmap[F] (transport (fun z => hom z d) p f) =
+      transport (fun z => hom z (fobj[F] d)) (f_equal (fobj[F]) p) (fmap[F] f).
+Proof.
+  destruct p. reflexivity.
+Defined.
+
+Lemma transport_functorial_cod (C D: Category) (F : @Functor C D) (c d d': C)
+  (p : d = d') (f : hom c d)
+  : fmap[F] (transport (fun z => hom c z) p f) =
+      transport (fun z => hom (fobj[F] c) z) (f_equal (fobj[F]) p) (fmap[F] f).
+Proof.
+  destruct p. reflexivity.
+Defined.
+
+#[export]
+ Program Instance Compose_respects_stricteq {C D E : Category} :
+   Proper (equiv ==> equiv ==> equiv) (@Compose C D E).
+ Next Obligation.
+  intros F G [FG_eq_on_obj FG_morphismcoherence] H K [HK_eq_on_obj HK_morphismcoherence].
+  unshelve eapply (_ ; _).
+  - intro c; simpl. 
+      exact(eq_trans (f_equal (fobj[F]) (HK_eq_on_obj c)) (FG_eq_on_obj (fobj[K] c))).
+  - intros c c' f.
+    simpl.
+    rewrite <- transport_trans, <- transport_r_trans.
+    rewrite <- transport_functorial_cod.
+    rewrite HK_morphismcoherence.
+    unfold transport_r at 1 2.
+    rewrite transport_functorial_dom.
+    rewrite transport_relation_exchange.
+    rewrite <- eq_sym_map_distr.
+    apply proper_transport_dom.
+    now trivial.
+ Defined.
+
+ Lemma fun_strict_equiv_id_right {A B} (F : A ⟶ B) : F ◯ Id ≈ F.
+ Proof. construct; cat. Qed.
+
+ Arguments fun_strict_equiv_id_right {A B} F.
+
+ Lemma fun_strict_equiv_id_left {A B} (F : A ⟶ B) : Id ◯ F ≈ F.
+ Proof. construct; cat. Qed.
+
+ Arguments fun_equiv_id_left {A B} F.
+
+ Lemma fun_strict_equiv_comp_assoc {A B C D} (F : C ⟶ D) (G : B ⟶ C) (H : A ⟶ B)  :
+   F ◯ (G ◯ H) ≈ (F ◯ G) ◯ H.
+ Proof. construct; cat. Qed.
+
+ Arguments fun_equiv_comp_assoc {A B C D} F G H.
+
+End StrictEq.
+