diff --git a/Construction/Free/Quiver.v b/Construction/Free/Quiver.v
new file mode 100644
index 00000000..ac979bd5
--- /dev/null
+++ b/Construction/Free/Quiver.v
@@ -0,0 +1,566 @@
+Require Import Category.Lib.
+Require Import Category.Lib.TList.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Isomorphism.
+Require Import Category.Theory.Functor.
+Require Import Category.Theory.Adjunction.
+Require Import Category.Theory.Universal.Arrow.
+Require Import Category.Instance.StrictCat.
+Require Import Category.Construction.Groupoid.
+Require Import Category.Construction.Opposite.
+Require Import Category.Construction.Product.
+Require Import Category.Instance.Sets.
+
+Generalizable All Variables.
+
+Section Quiver.
+  Class Quiver@{o h p} := {
+      nodes : Type@{o};
+      uedges := Type@{h} : Type@{h+1};
+      edges : nodes → nodes → uedges;
+      edgeset : ∀ X Y, Setoid@{h p} (edges X Y)
+    }.
+  Coercion nodes : Quiver >-> Sortclass.
+  Context (G : Quiver).
+  Existing Instance edgeset.
+
+  Fixpoint tlist'_quiver_equiv (k i j : G) 
+    (f : @tlist' _ edges k i) (g : @tlist' _ edges k j) ( p : i = j ) : Type :=
+    match f in (tlist' _ i_t) return (tlist' _ j) -> i_t = j -> Type with
+    | tnil => fun g' q => tnil = Logic.transport_r (fun z => @tlist' _ edges k z) q g'
+    | @tcons _ _ _ i0 i1 fhead ftail =>
+        fun g' : tlist' _ j  => 
+          match g' in tlist' _ j return @tlist' _ edges k i1 -> i0 = j -> Type with
+          | tnil => fun _ _ => False
+           | @tcons _ _ _ j0 j1 ghead gtail =>
+               fun ftail' p' =>
+                 { q : i1 = j1 &
+                      (Logic.transport (fun t => edges i0 t) q fhead ≈
+                         Logic.transport_r (fun t => edges t j1) p' ghead) &
+                      tlist'_quiver_equiv k i1 j1 ftail' gtail q }
+          end ftail
+    end g p.
+
+  Inductive tlist'_quiver_inductive (i : G) :
+    forall (j : G), (@tlist' _ edges i j) -> (@tlist' _ edges i j) -> Type :=
+  | tlist_both_empty : tlist'_quiver_inductive i tnil tnil
+  | tlist_both_cons (k : G) :
+    forall (j : G) (ftail gtail : @tlist' _ edges i j) (fhead ghead : edges k j),
+           (tlist'_quiver_inductive j ftail gtail) ->
+           fhead ≈ ghead ->
+           tlist'_quiver_inductive k (tcons _ fhead ftail)
+                                   (tcons _ ghead gtail).
+
+  Proposition fixpoint_implies_inductive (i j : G) (f g : tlist edges i j) :
+    tlist'_quiver_equiv _ _ _ f g eq_refl -> (tlist'_quiver_inductive _ _ f g).
+  Proof.
+    revert g; induction f.
+    - intros g H. simpl in H; unfold Logic.transport_r in H; simpl in H; destruct H.
+      constructor.
+    - intro g; destruct g; [ now apply False_rect |].
+      intro H. simpl in H; destruct H as [q t t0].
+      destruct q.
+      constructor.
+      + apply IHf. assumption.
+      + unfold Logic.transport_r in t. simpl in t. exact t.
+  Defined.
+
+  Proposition inductive_implies_fixpoint (i j : G) (f g : tlist edges i j) :
+    (tlist'_quiver_inductive _ _ f g) -> tlist'_quiver_equiv _ _ _ f g eq_refl.
+  Proof.
+    intro H.
+    induction H; [ now simpl | simpl ].
+    exists eq_refl; assumption.
+  Defined.
+  
+  Lemma tlist'_equiv_lengths (i j k : G) (f : tlist' k i) (g : tlist' k j) (p : i = j) :
+    tlist'_quiver_equiv _ _ _ f g p -> tlist_length f = tlist_length g.
+    revert j g p; induction f.
+    - intros j g p H. destruct g; [ reflexivity | ].
+      simpl in H. destruct p. unfold Logic.transport_r in H; simpl in H;
+        now inversion H.
+    - intros j' g p; destruct g; [ now apply False_rect | simpl ].
+      intros [j_eq_j0 X]; apply eq_S; unshelve eapply IHf; [ exact j_eq_j0 | assumption ].
+  Defined.
+  
+  Proposition tlist'_quiver_equiv_reflexive (k i: G) :
+    forall f : tlist edges i k, tlist'_quiver_equiv k i i f f eq_refl.
+  Proof.
+    intro f; induction f; [ now constructor |].
+    unshelve econstructor; easy.
+  Defined.
+
+  Arguments Logic.transport_r /.
+
+  Proposition tlist'_quiver_equiv_transitive (k i1 i2 i3: G) :
+      forall (f : tlist edges i1 k) (g : tlist edges i2 k) (h : tlist edges i3 k)
+             (p : i1 = i2) (q : i2 = i3),
+        tlist'_quiver_equiv k i1 i2 f g p ->
+        tlist'_quiver_equiv k i2 i3 g h q->
+        tlist'_quiver_equiv k i1 i3 f h (eq_trans p q).
+  Proof.
+    intro f; revert i2 i3.
+    induction f as [ | i0 i1 fhead ftail ]; 
+      [ intros i2 i3 g h p q equiv1 equiv2;
+        destruct p, q;
+        simpl in *; destruct equiv1; now simpl in equiv2 |].
+ 
+      (* [ intros; destruct g; [ easy | now apply False_rect ] |]. *)
+    intros i2 i3 g h p q equiv1 equiv2.
+    destruct g as [ | j0 j1 ghead gtail ]; [ now apply False_rect |]. 
+    simpl in equiv1. destruct equiv1 as [j_eq_j0 fhead_eq_ghead].
+    destruct h as [ | k0 k1 hhead htail]; [ now apply False_rect |].
+    simpl; simpl in equiv2; destruct equiv2 as [j1_eq_k1 gtail_eq_htail].
+    unshelve esplit; [ exact (eq_trans j_eq_j0 j1_eq_k1) | |].
+    - destruct j1_eq_k1, p, q, j_eq_j0.
+      unfold Logic.transport_r in *.
+      simpl Logic.transport in *. now apply (@Equivalence_Transitive _ _ _ _ ghead).
+    - unshelve eapply IHftail; [ exact gtail | assumption | assumption ].
+  Defined.
+
+  Proposition tlist'_quiver_equiv_symmetric (k i j: G) (p : i = j) : 
+    forall (f : tlist edges i k) (g: tlist edges j k),
+      tlist'_quiver_equiv k i j f g p -> tlist'_quiver_equiv k j i g f (eq_sym p).
+  Proof.
+    intro f; revert j p; induction f as [| i0 i1 fhead ftail];
+      intros j p g; destruct g as [|j0 j1 ghead gtail].
+    - unfold tlist'_quiver_equiv. intro H.
+      rewrite H at 2. unfold Logic.transport_r. simpl.
+      clear H. destruct p. reflexivity.
+    - intro H; simpl in H. apply False_rect. destruct p; simpl in H.
+      inversion H.
+    - now apply False_rect.
+    - simpl. intros [q e t].
+      exists (eq_sym q).
+      + simpl. apply Equivalence_Symmetric. destruct p, q. simpl in *.
+        assumption.
+      + now apply IHftail, t.
+  Defined.
+
+  Definition tlist_quiver_equiv (i k : G) : crelation (tlist edges i k) :=
+    fun f g => tlist'_quiver_equiv _ _ _ f g eq_refl.
+
+#[export]
+  Instance tlist_quiver_equiv_is_equiv (i k : G) : Equivalence (tlist_quiver_equiv i k).
+  Proof.
+    unshelve eapply Build_Equivalence.
+    + intro; apply tlist'_quiver_equiv_reflexive.
+    + intros f g H;
+      unfold tlist_quiver_equiv; change (@eq_refl _ i) with (eq_sym (@eq_refl _ i));
+      apply tlist'_quiver_equiv_symmetric; exact H.
+    + intros f g h equiv1 equiv2. unfold tlist_quiver_equiv.
+      change (@eq_refl _ i) with (eq_trans (@eq_refl _ i) (@eq_refl _ i)).
+      unshelve eapply tlist'_quiver_equiv_transitive; [ exact g | |]; assumption.
+  Defined.
+End Quiver.
+
+Definition Build_Quiver_Standard_Eq ( node_type : Type )
+  ( edge_type : node_type -> node_type -> Type ) : Quiver :=
+  {|
+    nodes := node_type ;
+    edges := edge_type;
+    edgeset := fun _ _ => {| equiv := eq; setoid_equiv := eq_equivalence |}                       
+  |}.
+
+Class QuiverHomomorphism@{o1 h1 p1 o2 h2 p2}
+  (G : Quiver@{o1 h1 p1}) (G' : Quiver@{o2 h2 p2}) := {
+    fnodes : @nodes G -> @nodes G';
+    fedgemap : ∀ x y : @nodes G, edges x y -> edges (fnodes x) (fnodes y);
+    fedgemap_respects : ∀ x y,
+    Proper@{h2 p2} (respectful@{h1 p1 h2 p2 h2 p2}
+                      (@equiv@{h1 p1} _ (edgeset _ _))
+                      (@equiv@{h2 p2} _ (edgeset _ _))) (@fedgemap x y)
+  }.
+
+Coercion fnodes : QuiverHomomorphism >-> Funclass.
+Local Existing Instance edgeset.
+
+Section QuiverCategory.
+Definition QuiverHomomorphismEquivalence
+  (Q : Quiver) (Q' : Quiver) (F G : QuiverHomomorphism Q Q') : Type :=
+  { node_equiv : forall x : Q, (@fnodes _ _ F x) = (@fnodes _ _ G x)
+        & forall (x y : Q) (f : edges x y),
+          let eqx := node_equiv x in
+          let eqy := node_equiv y in
+          let Ff := @fedgemap _ _ F x y f in
+          let Gf := @fedgemap _ _ G x y f in
+          (Logic.transport (fun t => edges (F x) t) eqy Ff ≈
+             Logic.transport_r (fun t => edges t (G y)) eqx Gf) }.
+
+Proposition QuiverHomomorphismEquivalence_Reflexive (Q Q' : Quiver)
+  : Reflexive (QuiverHomomorphismEquivalence Q Q').
+Proof.
+  intro F. unfold QuiverHomomorphismEquivalence.
+  exists (fun _ => eq_refl). reflexivity.
+Qed.
+
+Proposition transport_id (C : Category) (c c' : C) (p : c = c') :
+  Logic.transport (hom c) p (@id C c) = Logic.transport_r (fun z => hom z c') p (@id C c').
+Proof.
+  now destruct p.
+Defined.
+
+Proposition transport_comp (C : Category) (c d e e' : C) (p : e = e')
+  (f : hom c d) (g : hom d e)
+  : Logic.transport (hom c) p (g ∘ f) = (Logic.transport (hom d) p g) ∘ f.
+Proof.
+  now destruct p.
+Defined.
+
+Proposition transport_r_comp (C : Category) (c c' d e : C) (p : c = c')
+  (f : hom c' d) (g : hom d e)
+  : Logic.transport_r (fun z => hom z e) p (g ∘ f) =
+      g ∘ (Logic.transport_r (fun z => hom z d) p f).
+Proof.
+  now destruct p.
+Defined.
+
+Proposition transport_comp_mid (C : Category) (c d d' e : C) (p : d = d')
+  (f : hom c d) (g : hom d' e)
+  : g ∘ (Logic.transport (hom c) p f) =
+      (Logic.transport_r (fun z => hom z e) p g) ∘ f.
+Proof.
+  now destruct p.
+Defined.
+
+Proposition QuiverHomomorphismEquivalence_Transitive (Q Q' : Quiver)
+  : Transitive (QuiverHomomorphismEquivalence Q Q').
+Proof.
+  intros F G H
+    [F_eq_G_on_obj FG_coherent_transport]
+    [G_eq_H_on_obj GH_coherent_transport].
+  unfold QuiverHomomorphismEquivalence in *.
+  exists (fun x => eq_trans (F_eq_G_on_obj x) (G_eq_H_on_obj x)).
+  intros c c' f.
+  unfold Logic.transport_r.
+  rewrite eq_trans_sym_distr.
+  rewrite <- 2! transport_trans.
+  rewrite (FG_coherent_transport c c' f).
+  unfold Logic.transport_r in *.
+  rewrite <- (GH_coherent_transport c c' f).
+  rewrite transport_relation_exchange.
+  reflexivity.
+Qed.
+
+Proposition QuiverHomomorphismEquivalence_Symmetric (Q Q' : Quiver)
+  : Symmetric (QuiverHomomorphismEquivalence Q Q').
+Proof.
+  intros F G [F_eq_G_on_obj FG_coherent_transport].
+  simpl in FG_coherent_transport.
+  exists (fun x => eq_sym (F_eq_G_on_obj x)).
+  simpl.
+  intros c c' f. unfold Logic.transport_r in *.
+  rewrite eq_sym_involutive.
+  specialize FG_coherent_transport with c c' f.
+  apply (proper_transport_dom Q' edges _ (F c) (G c) (G c') (F_eq_G_on_obj c)) in
+    FG_coherent_transport.
+  rewrite transport_trans, eq_trans_sym_inv_l
+    in FG_coherent_transport;
+    simpl in FG_coherent_transport.
+  apply (proper_transport_cod Q' edges _ (G c) (G c') (F c') (eq_sym (F_eq_G_on_obj c'))) in
+    FG_coherent_transport.
+  rewrite transport_relation_exchange, transport_trans,
+    eq_trans_sym_inv_r in FG_coherent_transport;
+    simpl in FG_coherent_transport.
+  symmetry; exact FG_coherent_transport.
+Defined.
+
+Program Definition QuiverId (Q : Quiver) : QuiverHomomorphism Q Q :=
+  {|
+    fnodes := Datatypes.id;
+    fedgemap := fun _ _ => Datatypes.id;
+    fedgemap_respects := _
+  |}.
+
+Arguments fedgemap {G G' QuiverHomomorphism x y}.
+
+Lemma transport_quiver_dom
+  (C D: Type) (ArrC : forall c c' : C, Type) (ArrD : forall d d' : D, Type)
+  (Fobj : C -> D) (Fmap : forall c c' : C, (ArrC c c') -> (ArrD (Fobj c) (Fobj c')))
+  (c c' d: C) (p : c = c') (f : ArrC c d)
+  : Fmap _ _ (Logic.transport (fun z => ArrC z d) p f) =
+      Logic.transport (fun z => ArrD z (Fobj d)) (f_equal (Fobj) p) (Fmap _ _ f).
+Proof.
+  destruct p. reflexivity.
+Defined.
+
+Lemma transport_quiver_cod
+  (C D: Type) (ArrC : forall c c' : C, Type) (ArrD : forall d d' : D, Type)
+  (Fobj : C -> D) (Fmap : forall c c' : C, (ArrC c c') -> (ArrD (Fobj c) (Fobj c')))
+  (c d d': C) (p : d = d') (f : ArrC c d)
+  : Fmap _ _ (Logic.transport (fun z => ArrC c z) p f) =
+      Logic.transport (fun z => ArrD (Fobj c) z) (f_equal (Fobj) p) (Fmap _ _ f).
+Proof.
+  destruct p. reflexivity.
+Defined.
+
+Local Notation "Q ⇨ Q'" := (QuiverHomomorphism Q Q') (at level 40).
+Definition QuiverComp {Q1 Q2 Q3: Quiver} (F : Q1 ⇨ Q2) (G : Q2 ⇨ Q3) : Q1 ⇨ Q3.
+Proof.
+  unshelve refine
+    (Build_QuiverHomomorphism Q1 Q3 (Basics.compose (@fnodes _ _ G) (@fnodes _ _ F)) _ _).
+  unshelve eapply Build_SetoidMorphism.
+  + exact (fun f => (fedgemap (fedgemap f))).
+  + cat_simpl.
+Defined.
+
+#[export] Instance QuiverHomomorphismEquivalence_IsEquivalence (Q Q': Quiver)
+  : @Equivalence (QuiverHomomorphism Q Q') (QuiverHomomorphismEquivalence Q Q') :=
+  {|
+    Equivalence_Reflexive := QuiverHomomorphismEquivalence_Reflexive Q Q';
+    Equivalence_Symmetric := QuiverHomomorphismEquivalence_Symmetric Q Q';
+    Equivalence_Transitive := QuiverHomomorphismEquivalence_Transitive Q Q'
+  |}.
+Local Existing Instance fedgemap_respects.
+#[export] Instance QuiverCategory : Category.
+Proof.
+  unshelve eapply
+    (Build_Category'
+       QuiverHomomorphism
+       QuiverId
+       (fun Q1 Q2 Q3 F G => @QuiverComp Q1 Q2 Q3 G F) ).
+  + exact (fun Q Q' =>
+             {| equiv := QuiverHomomorphismEquivalence Q Q';
+               setoid_equiv := QuiverHomomorphismEquivalence_IsEquivalence Q Q'
+             |}).
+  + intros Q1 Q2 Q3 G1 G2 [G_equiv_on_obj G_arrow_coher]
+      F1 F2 [F_equiv_on_obj F_arrow_coher].
+    exists (fun x => eq_trans (f_equal (@fnodes _ _ G1) (F_equiv_on_obj x))
+                       (G_equiv_on_obj (F2 x))).
+    intros x y f; simpl in *.
+    unfold Logic.transport_r in *.
+    rewrite eq_trans_sym_distr.
+    rewrite <- 2! transport_trans.
+    rewrite <- (G_arrow_coher _ _ (fedgemap f)).
+    rewrite <- transport_relation_exchange.
+    rewrite eq_sym_map_distr.
+    rewrite <- 2! transport_f_equal.
+    apply (proper_transport_cod _ edges _ (G1 (F1 x)) _ _ (G_equiv_on_obj (F2 y))).
+    rewrite transport_f_equal.
+    rewrite <- transport_quiver_cod.
+    rewrite (F_arrow_coher _ _ f).
+    rewrite (transport_f_equal _ _ (fun b => edges b (G1 (F2 y)))).
+    rewrite <- transport_quiver_dom.
+    apply fedgemap_respects.
+    reflexivity.
+  + intros x y f; now exists (fun x =>  eq_refl). 
+  + intros x y f; now exists (fun x =>  eq_refl). 
+  + intros w x y z f g h; now exists (fun x => eq_refl). 
+Defined.
+End QuiverCategory.
+
+Section Underlying.
+  Universes o h p.
+
+  Program Definition QuiverOfCat (C : Category@{o h p}) : Quiver@{o h p} :=
+    {|
+      nodes     := obj;
+      edges     := hom
+    |}.
+  Local Notation "Q ⇨ Q'" := (QuiverHomomorphism Q Q') (at level 40).
+  Program Definition QuiverHomomorphismOfFunctor
+    (C D: Category) (F : @Functor C D) : (QuiverOfCat C) ⇨ (QuiverOfCat D).
+  unshelve eapply Build_QuiverHomomorphism.
+  - exact fobj.
+  - exact (@fmap C D F).
+  - exact fmap_respects.
+  Defined.
+
+  Definition Forgetful : @Functor StrictCat QuiverCategory.
+  Proof.
+    unshelve eapply Build_Functor.
+    + exact QuiverOfCat.
+    + exact QuiverHomomorphismOfFunctor.
+    + intros x y f g f_eq_g. destruct f_eq_g as [fg_eq_on_obj arrow_coherence].
+      exists fg_eq_on_obj. simpl; intros c c' k.
+      apply arrow_coherence.
+    + intro C. exists (fun x => eq_refl). now trivial.
+    + intros x y z f g. exists (fun x => eq_refl). now trivial.
+  Defined.
+
+End Underlying.
+
+Section Free.
+  Universes o h p.
+  Context (G : Quiver@{o h p}).
+
+  Arguments Logic.transport_r /.
+  Program Definition FreeOnQuiver : Category@{o h p} :=
+    {|
+      obj     := @nodes G;
+      hom     := tlist edges;
+      homset  := fun i j => {| equiv := tlist_quiver_equiv _ _ _  ;
+                              setoid_equiv := tlist_quiver_equiv_is_equiv _ _ _ |};
+      id      := fun _ => tnil;
+      compose := fun _ _ _ f g => g +++ f
+|}.
+Next Obligation.
+  revert z x0 y0 X y1 X0.
+  induction x1.
+  - intros z f g f_eq_g ghead H.
+    unfold tlist_quiver_equiv in H.
+    unfold tlist'_quiver_equiv in H. simpl in H. destruct H.
+    destruct (eq_sym (tlist_app_tnil_l f)).
+    destruct (eq_sym (tlist_app_tnil_l g)).
+    assumption.
+  - intros z f g f_eq_g ghead H.
+    destruct (tlist_app_comm_cons b x1 f).
+    unfold tlist_quiver_equiv.
+    destruct ghead as [| i k e ghead]; [ now apply False_rect| ].
+    destruct (tlist_app_comm_cons e ghead g).
+    simpl tlist'_quiver_equiv. unfold tlist_quiver_equiv in H.
+    simpl in H. destruct H as [q tr t]; exists q; [ exact tr |].
+    unfold tlist_quiver_equiv in IHx1. destruct q.
+    apply IHx1; [ exact f_eq_g | exact t ].
+  Defined. 
+  Next Obligation. rewrite tlist_app_tnil_r. apply Equivalence_Reflexive. Qed.
+  Next Obligation. rewrite tlist_app_tnil_l. apply Equivalence_Reflexive. Qed.
+  Next Obligation. rewrite tlist_app_assoc. apply Equivalence_Reflexive.  Qed.
+  Next Obligation. rewrite tlist_app_assoc. apply Equivalence_Reflexive.  Qed.
+  
+  Definition InducedFunctor {C : Category} 
+    (F : QuiverHomomorphism G (QuiverOfCat C)) : @Functor (FreeOnQuiver) C.
+  Proof.
+    unshelve eapply Build_Functor. 
+    { change obj[C] with (@nodes (QuiverOfCat C)). exact fnodes. }
+    { intros c c'; simpl; intro f; unfold tlist in f.
+      induction f as [| c c_mid fhead ftail IHftail] ; [ exact id | ].
+      refine (compose IHftail _).
+      change _ with (@edges (QuiverOfCat C) (fnodes c) (fnodes c_mid)).
+      exact (fedgemap _ _ fhead). }
+    { intros c1 c2; simpl; intro f; induction f as [| c1 c_mid fhead ftail IHf].
+      - intros a H; simpl in H; unfold tlist_quiver_equiv, tlist'_quiver_equiv in H. 
+        simpl in H; destruct H; reflexivity.
+      - intros g H. unfold tlist_quiver_equiv in H.
+        destruct g; [ now apply False_rect |].
+        simpl in H. destruct H as [q t t0]. simpl.
+        set (zm := tlist'_rect G edges c2 _ _ _) in *; clearbody zm.
+        destruct q.
+        refine (@compose_respects C
+                  (@fnodes _ _ F i)
+                  (@fnodes _ _ F c_mid)
+                  (@fnodes _ _ F c2)
+                  (zm c_mid ftail)
+                  (zm c_mid g)
+                  _
+                  ((@fedgemap _ _ F) i c_mid fhead)
+                  ((@fedgemap _ _ F) i c_mid e)
+                  _   ).
+        + apply IHf. assumption.
+        + apply (@fedgemap_respects _ _ F). exact t.
+    }
+    { reflexivity. }
+    { intros c1 c2 c3 f g. simpl.
+      induction g.
+      + simpl. destruct (eq_sym (tlist_app_tnil_l f)).
+        apply Equivalence_Symmetric, id_right.
+      + destruct (tlist_app_comm_cons b g f); simpl.
+        set (zm := tlist'_rect _ _ _ _ _ _) in *.
+        rewrite comp_assoc; set (k := fedgemap _ _ _).
+        change (edges _  _ ) with (@hom _ ((@fnodes _ _ F) i) ((@fnodes _ _ F) j)) in k.
+        refine  (compose_respects _ _ _ k k _); [ apply IHg | reflexivity]. }
+  Defined.
+
+  Definition UnitQuiverCatAdjunction :
+    QuiverHomomorphism G (QuiverOfCat (FreeOnQuiver)).
+  Proof.
+    unshelve eapply Build_QuiverHomomorphism.
+    { exact Datatypes.id. }
+    { exact (fun x y f => tlist_singleton f). }
+    { intros x y p q; unfold tlist_singleton;
+        simpl; unfold tlist_quiver_equiv, tlist'_quiver_equiv;
+        intros ?; exists eq_refl; [assumption | reflexivity]. }
+  Defined.
+  
+  Definition UniversalArrowQuiverCat : @UniversalArrow QuiverCategory StrictCat  G Forgetful.
+    unshelve eapply universal_arrow_from_UMP.
+    - exact FreeOnQuiver.
+    - exact UnitQuiverCatAdjunction.
+    - intros C F; unshelve esplit.
+      + exact (InducedFunctor F).
+      + simpl. exists (fun z => eq_refl). simpl. intros; now rewrite id_left.
+      + intros S [FS_eq_on_obj FS_arrow_coherence]; simpl in FS_arrow_coherence.
+        exists FS_eq_on_obj.
+        intros x y f. induction f.
+        * change (@tnil _ _ y) with (@id FreeOnQuiver y).
+          simpl; rewrite fmap_id. rewrite transport_id; reflexivity.
+        * change (fmap[InducedFunctor F] (b ::: f)) with
+            ((fmap[InducedFunctor F] f) ∘ (@fedgemap _ _ F _ _ b)).
+          assert (RW : @equiv (@hom FreeOnQuiver i y) _ (b ::: f)
+                         (@compose FreeOnQuiver _ _ _ f (tlist_singleton b)))
+                   by 
+                   (unfold tlist_singleton; simpl; now rewrite <- tlist_app_cons);
+          rewrite RW, fmap_comp.
+          rewrite transport_comp.
+          rewrite IHf.
+          rewrite <- transport_comp_mid.
+          rewrite transport_r_comp.
+          apply compose_respects; [ reflexivity |].
+          apply FS_arrow_coherence.
+  Defined.
+End Free.
+
+Definition FreeCatFunctor : @Functor QuiverCategory StrictCat :=
+  (LeftAdjointFunctorFromUniversalArrows Forgetful
+     (fun _ => @UniversalArrowQuiverCat _ )).
+
+Definition FreeForgetfulAdjunction : Adjunction FreeCatFunctor Forgetful :=
+  AdjunctionFromUniversalArrows _ _ .
+
+Section FreeQuiverSyntax.
+Context {G : Quiver}.
+
+Inductive Mor : nodes → nodes → Type :=
+  | Ident {x} : Mor x x
+  | Morph {x y} (f : edges x y) : Mor x y
+  | Comp  {x y z} (f : Mor y z) (g : Mor x y) : Mor x z.
+
+Fixpoint morDA `(t : Mor x y) : tlist edges x y :=
+  match t with
+  | Ident => tnil
+  | Morph f => tcons _ f tnil
+  | Comp f g => morDA g +++ morDA f
+  end.
+
+Program Instance Mor_Setoid {x y} : Setoid (Mor x y) := {
+  equiv f g := morDA f = morDA g
+  }.
+Next Obligation. equivalence; congruence. Qed.
+
+Fixpoint tlistDA `(t : tlist edges x y) : Mor x y :=
+  match t with
+  | tnil => Ident
+  | tcons _ f fs => Comp (tlistDA fs) (Morph f)
+  end.
+
+Lemma morDA_tlistDA `{f : tlist edges x y} :
+  morDA (tlistDA f) = f.
+Proof.
+  induction f; simpl; auto.
+  rewrite <- tlist_app_cons.
+  now rewrite IHf.
+Qed.
+
+(* While this is merely an equivalence. Such is the essence of adjointness
+   between pseudocategories. *)
+Lemma tlistDA_morDA `{f : Mor x y} :
+  tlistDA (morDA f) ≈ f.
+Proof.
+  induction f; simpl; auto.
+  rewrite <- IHf1, <- IHf2.
+  now rewrite morDA_tlistDA.
+Qed.
+
+Program Definition FreeSyntax : Category := {|
+  obj     := nodes ;
+  hom     := Mor;
+  homset  := @Mor_Setoid;
+  id      := fun _ => Ident;
+  compose := fun _ _ _ => Comp
+|}.
+Next Obligation. simpl. congruence. Qed.
+Next Obligation. now apply tlist_app_tnil_r. Qed.
+Next Obligation. now apply tlist_app_assoc. Qed.
+Next Obligation. now symmetry; apply tlist_app_assoc. Qed.
+
+End FreeQuiverSyntax.
diff --git a/Construction/Free/Quiver.v~ b/Construction/Free/Quiver.v~
new file mode 100644
index 00000000..e69de29b
diff --git a/Functor/Hom.v b/Functor/Hom.v
index 0279705f..748d2b40 100644
--- a/Functor/Hom.v
+++ b/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.
diff --git a/Instance/Comp.v b/Instance/Comp.v
index c45d469f..8364d5db 100644
--- a/Instance/Comp.v
+++ b/Instance/Comp.v
@@ -250,7 +250,7 @@ Section Examples.
    and long. *)
 
 (* Group operations *)
-Inductive Group_operation :=
+Inductive Group_operation : Set :=
   | one : Group_operation  (* unit *)
   | mul : Group_operation  (* multiplication *)
   | inv : Group_operation. (* inverse *)
@@ -283,7 +283,7 @@ Definition inv' {G : OpAlgebra GroupOp} (x : G) :=
   op G inv (fun _ => x).
 
 (* There are five group equations. *)
-Inductive Group_equation :=
+Inductive Group_equation : Set :=
   | assoc : Group_equation
   | unit_left : Group_equation
   | unit_right : Group_equation
diff --git a/Instance/Fun/Cartesian.v b/Instance/Fun/Cartesian.v
new file mode 100644
index 00000000..f7ba58d9
--- /dev/null
+++ b/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.
diff --git a/Instance/Lambda/Eval.v b/Instance/Lambda/Eval.v
index d015bddf..f30bc3e4 100644
--- a/Instance/Lambda/Eval.v
+++ b/Instance/Lambda/Eval.v
@@ -17,14 +17,14 @@ Section Eval.
 
 Import ListNotations.
 
-Inductive Closed : Ty → Type :=
+Inductive Closed : Ty → Set :=
   | Closure {Γ τ} : Exp Γ τ → ClEnv Γ → Closed τ
 
-with ClEnv : Env → Type :=
+with ClEnv : Env → Set :=
   | NoCl : ClEnv []
   | AddCl {Γ τ} : Value τ → ClEnv Γ → ClEnv (τ :: Γ)
 
-with Value : Ty → Type :=
+with Value : Ty → Set :=
   | Val {Γ τ} (x : Exp Γ τ) : ValueP x → ClEnv Γ → Value τ.
 
 Derive Signature NoConfusion NoConfusionHom Subterm for ClEnv Closed Value.
@@ -43,7 +43,7 @@ Fixpoint snoc {a : Type} (x : a) (xs : list a) : list a :=
   | x :: xs => x :: snoc x xs
   end.
 
-Inductive EvalContext : Ty → Ty → Type :=
+Inductive EvalContext : Ty → Ty → Set :=
   | MT {τ} : EvalContext τ τ
   | AR {dom cod τ} :
     Closed dom → EvalContext cod τ → EvalContext (dom ⟶ cod) τ
@@ -56,7 +56,7 @@ Inductive EvalContext : Ty → Ty → Type :=
 
 Derive Signature NoConfusion NoConfusionHom Subterm for EvalContext.
 
-Inductive Σ : Ty → Type :=
+Inductive Σ : Ty → Set :=
   | MkΣ {u    : Ty}
         (exp  : Closed u)
         {τ    : Ty}
diff --git a/Instance/Lambda/Exp.v b/Instance/Lambda/Exp.v
index e7ace8e4..1295869c 100644
--- a/Instance/Lambda/Exp.v
+++ b/Instance/Lambda/Exp.v
@@ -19,13 +19,13 @@ Open Scope Ty_scope.
 
 Definition Env := list Ty.
 
-Inductive Var : Env → Ty → Type :=
+Inductive Var : Env → Ty → Set :=
   | ZV {Γ τ}    : Var (τ :: Γ) τ
   | SV {Γ τ τ'} : Var Γ τ → Var (τ' :: Γ) τ.
 
 Derive Signature NoConfusion EqDec for Var.
 
-Inductive Exp Γ : Ty → Type :=
+Inductive Exp Γ : Ty → Set :=
   | EUnit         : Exp Γ TyUnit
 
   | Pair {τ1 τ2}  : Exp Γ τ1 → Exp Γ τ2 → Exp Γ (TyPair τ1 τ2)
diff --git a/Instance/Lambda/Full.v b/Instance/Lambda/Full.v
index 0db9263a..19a94ee0 100644
--- a/Instance/Lambda/Full.v
+++ b/Instance/Lambda/Full.v
@@ -24,7 +24,7 @@ Open Scope Ty_scope.
 
 (* A context defines a hole which, after substitution, yields an expression of
    the index type. *)
-Inductive Frame Γ : Ty → Ty → Type :=
+Inductive Frame Γ : Ty → Ty → Set :=
   | F_PairL {τ1 τ2}  : Exp Γ τ2 → Frame τ1 (τ1 × τ2)
   | F_PairR {τ1 τ2}  : Exp Γ τ1 → Frame τ2 (τ1 × τ2)
   | F_Fst {τ1 τ2}    : Frame (τ1 × τ2) τ1
@@ -34,7 +34,7 @@ Inductive Frame Γ : Ty → Ty → Type :=
 
 Derive Signature NoConfusion Subterm for Frame.
 
-Inductive Ctxt Γ : Ty → Ty → Type :=
+Inductive Ctxt Γ : Ty → Ty → Set :=
   | C_Nil {τ}         : Ctxt τ τ
   | C_Cons {τ τ' τ''} : Frame Γ τ' τ → Ctxt τ'' τ' → Ctxt τ'' τ.
 
@@ -65,7 +65,7 @@ Theorem Ctxt_comp_assoc {Γ τ τ' τ'' τ'''}
   Ctxt_comp C (Ctxt_comp C' C'') = Ctxt_comp (Ctxt_comp C C') C''.
 Proof. induction C; simpl; auto; now f_equal. Qed.
 
-Inductive Redex {Γ} : ∀ {τ}, Exp Γ τ → Exp Γ τ → Type :=
+Inductive Redex {Γ} : ∀ {τ}, Exp Γ τ → Exp Γ τ → Set :=
   | R_Beta {dom cod} (e : Exp (dom :: Γ) cod) v :
     ValueP v →
     Redex (APP (LAM e) v) (SubExp {|| v ||} e)
@@ -82,7 +82,7 @@ Derive Signature for Redex.
 
 Unset Elimination Schemes.
 
-Inductive Plug {Γ τ'} (e : Exp Γ τ') : ∀ {τ}, Ctxt Γ τ' τ → Exp Γ τ → Type :=
+Inductive Plug {Γ τ'} (e : Exp Γ τ') : ∀ {τ}, Ctxt Γ τ' τ → Exp Γ τ → Set :=
   | Plug_Hole : Plug (C_Nil _) e
 
   | Plug_PairL {τ1 τ2} {C : Ctxt Γ τ' τ1} {e' : Exp Γ τ1} {e2 : Exp Γ τ2} :
@@ -147,7 +147,7 @@ Theorem Plug_id_left {Γ τ τ'} {C : Ctxt Γ τ' τ} {x : Exp Γ τ'} {y : Exp
   Plug_comp Plug_id P ~= P.
 *)
 
-Inductive Step {Γ τ} : Exp Γ τ → Exp Γ τ → Type :=
+Inductive Step {Γ τ} : Exp Γ τ → Exp Γ τ → Set :=
   | StepRule {τ'} {C : Ctxt Γ τ' τ} {e1 e2 : Exp Γ τ'} {e1' e2' : Exp Γ τ} :
     Plug e1 C e1' →
     Plug e2 C e2' →
diff --git a/Instance/Lambda/Norm.v b/Instance/Lambda/Norm.v
index 549edfe5..6cdc67cc 100644
--- a/Instance/Lambda/Norm.v
+++ b/Instance/Lambda/Norm.v
@@ -100,6 +100,8 @@ Arguments SN_Sub {Γ Γ'} /.
 
 Definition SN_halts {Γ τ} {e : Γ ⊢ τ} : SN e → halts e := ExpP_P _.
 
+#[local] Transparent ExpP.
+
 Lemma step_preserves_SN {Γ τ} {e e' : Γ ⊢ τ} :
   (e ---> e') → SN e → SN e'.
 Proof.
diff --git a/Instance/Lambda/Ren.v b/Instance/Lambda/Ren.v
index a0990a52..ff81fad2 100644
--- a/Instance/Lambda/Ren.v
+++ b/Instance/Lambda/Ren.v
@@ -15,7 +15,7 @@ Section Ren.
 
 Import ListNotations.
 
-Inductive Ren : Env → Env → Type :=
+Inductive Ren : Env → Env → Set :=
   | NoRen : Ren [] []
   | Drop {τ Γ Γ'} : Ren Γ Γ' → Ren (τ :: Γ) Γ'
   | Keep {τ Γ Γ'} : Ren Γ Γ' → Ren (τ :: Γ) (τ :: Γ').
diff --git a/Instance/Lambda/Step.v b/Instance/Lambda/Step.v
index be30f8c1..42c4004b 100644
--- a/Instance/Lambda/Step.v
+++ b/Instance/Lambda/Step.v
@@ -25,7 +25,7 @@ Open Scope Ty_scope.
 
 Reserved Notation " t '--->' t' " (at level 40).
 
-Inductive Step : ∀ {Γ τ}, Exp Γ τ → Exp Γ τ → Type :=
+Inductive Step : ∀ {Γ τ}, Exp Γ τ → Exp Γ τ → Set :=
   | ST_Pair1 Γ τ1 τ2 (x x' : Exp Γ τ1) (y : Exp Γ τ2) :
     x ---> x' →
     Pair x y ---> Pair x' y
diff --git a/Instance/Lambda/Sub.v b/Instance/Lambda/Sub.v
index 3682a294..a3be8ad7 100644
--- a/Instance/Lambda/Sub.v
+++ b/Instance/Lambda/Sub.v
@@ -16,7 +16,7 @@ Section Sub.
 
 Import ListNotations.
 
-Inductive Sub (Γ : Env) : Env → Type :=
+Inductive Sub (Γ : Env) : Env → Set :=
   | NoSub : Sub []
   | Push {Γ' τ} : Exp Γ τ → Sub Γ' → Sub (τ :: Γ').
 
diff --git a/Instance/Lambda/Ty.v b/Instance/Lambda/Ty.v
index 22fb14f9..741ca879 100644
--- a/Instance/Lambda/Ty.v
+++ b/Instance/Lambda/Ty.v
@@ -7,7 +7,7 @@ Set Transparent Obligations.
 
 Section Ty.
 
-Inductive Ty : Type :=
+Inductive Ty : Set :=
   | TyUnit  : Ty
   | TyPair  : Ty → Ty → Ty
   | TyArrow : Ty → Ty → Ty.
diff --git a/Instance/Lambda/Value.v b/Instance/Lambda/Value.v
index 35d1091f..dde8fca1 100644
--- a/Instance/Lambda/Value.v
+++ b/Instance/Lambda/Value.v
@@ -16,7 +16,7 @@ Open Scope Ty_scope.
 
 (* [ValueP] is an inductive proposition that indicates whether an expression
    represents a value, i.e., that it does reduce any further. *)
-Inductive ValueP Γ : ∀ {τ}, Exp Γ τ → Type :=
+Inductive ValueP Γ : ∀ {τ}, Exp Γ τ → Set :=
   | UnitP : ValueP EUnit
   | PairP {τ1 τ2} {x : Exp Γ τ1} {y : Exp Γ τ2} :
     ValueP x → ValueP y → ValueP (Pair x y)
diff --git a/Instance/Parallel.v b/Instance/Parallel.v
index a1df091d..3038744c 100644
--- a/Instance/Parallel.v
+++ b/Instance/Parallel.v
@@ -12,9 +12,9 @@ Generalizable All Variables.
 
   This is used to build diagrams that identify equalizers. *)
 
-Inductive ParObj : Type := ParX | ParY.
+Inductive ParObj : Set := ParX | ParY.
 
-Inductive ParHom : bool → ParObj → ParObj → Type :=
+Inductive ParHom : bool → ParObj → ParObj → Set :=
   | ParIdX : ParHom true ParX ParX
   | ParIdY : ParHom true ParY ParY
   | ParOne : ParHom true ParX ParY
diff --git a/Instance/Roof.v b/Instance/Roof.v
index 3aa1b4b5..a57898eb 100644
--- a/Instance/Roof.v
+++ b/Instance/Roof.v
@@ -15,9 +15,9 @@ Generalizable All Variables.
 
   This is used to build diagrams that identify spans and pullbacks. *)
 
-Inductive RoofObj : Type := RNeg | RZero | RPos.
+Inductive RoofObj : Set := RNeg | RZero | RPos.
 
-Inductive RoofHom : RoofObj → RoofObj → Type :=
+Inductive RoofHom : RoofObj → RoofObj → Set :=
   | IdNeg   : RoofHom RNeg  RNeg
   | ZeroNeg : RoofHom RZero RNeg
   | IdZero  : RoofHom RZero RZero
diff --git a/Instance/Sets.v b/Instance/Sets.v
index 2e2d9020..fc4f480b 100644
--- a/Instance/Sets.v
+++ b/Instance/Sets.v
@@ -124,7 +124,7 @@ Ltac morphism :=
 Require Import Category.Structure.Terminal.
 
 #[export]
-Program Instance Unit_Setoid : Setoid poly_unit := {
+Program Instance Unit_Setoid@{u} : Setoid@{u u} poly_unit@{u} := {
   equiv := fun x y => x = y
 }.
 
@@ -139,7 +139,8 @@ Next Obligation. destruct (f x0), (g x0); reflexivity. Qed.
 Require Import Category.Structure.Initial.
 
 #[export]
-Program Instance False_Setoid : Setoid False.
+Program Instance False_Setoid@{u} : Setoid@{u u} False.
+Next Obligation. proper. Qed.
 
 #[export]
 Program Instance Sets_Initial : @Initial Sets := {
@@ -266,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.
@@ -283,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;
@@ -293,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.
diff --git a/Instance/Shapes.v b/Instance/Shapes.v
index aec78941..79a43222 100644
--- a/Instance/Shapes.v
+++ b/Instance/Shapes.v
@@ -78,7 +78,7 @@ Qed.
 
 (**************************************************************************)
 
-Inductive Shape :=
+Inductive Shape : Set :=
   | Bottom
   | Top
   | Plus (x y : Shape)
diff --git a/Instance/StrictCat.v b/Instance/StrictCat.v
new file mode 100644
index 00000000..34b29d83
--- /dev/null
+++ b/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)
+}.
diff --git a/Instance/Two.v b/Instance/Two.v
index c9bfede5..5169ad44 100644
--- a/Instance/Two.v
+++ b/Instance/Two.v
@@ -4,9 +4,9 @@ Require Import Category.Theory.Functor.
 
 Generalizable All Variables.
 
-Inductive TwoObj : Type := TwoX | TwoY.
+Inductive TwoObj : Set := TwoX | TwoY.
 
-Inductive TwoHom : TwoObj → TwoObj → Type :=
+Inductive TwoHom : TwoObj → TwoObj → Set :=
   | TwoIdX : TwoHom TwoX TwoX
   | TwoIdY : TwoHom TwoY TwoY
   | TwoXY  : TwoHom TwoX TwoY.
diff --git a/Instance/Two/Discrete.v b/Instance/Two/Discrete.v
index 8e563757..b941a8a9 100644
--- a/Instance/Two/Discrete.v
+++ b/Instance/Two/Discrete.v
@@ -4,9 +4,9 @@ Require Import Category.Theory.Functor.
 
 Generalizable All Variables.
 
-Inductive TwoDObj : Type := TwoDX | TwoDY.
+Inductive TwoDObj : Set := TwoDX | TwoDY.
 
-Inductive TwoDHom : TwoDObj → TwoDObj → Type :=
+Inductive TwoDHom : TwoDObj → TwoDObj → Set :=
   | TwoDIdX : TwoDHom TwoDX TwoDX
   | TwoDIdY : TwoDHom TwoDY TwoDY.
 
diff --git a/Lib/MapDecide.v b/Lib/MapDecide.v
index 701162ce..eff09be4 100644
--- a/Lib/MapDecide.v
+++ b/Lib/MapDecide.v
@@ -41,11 +41,11 @@ Notation "x && y" := (if x then Reduce y else No) : partial_scope.
  * A term language for theorems involving FMaps
  *)
 
-Record environment := {
+Record environment : Set := {
   vars : positive → N
 }.
 
-Inductive term :=
+Inductive term : Set :=
   | Var   : positive → term
   | Value : N → term.
 
@@ -118,7 +118,7 @@ Fixpoint map_expr_denote env (m : map_expr) : M.t N :=
                           (term_denote env  f) (map_expr_denote env m')
   end.
 
-Inductive formula :=
+Inductive formula : Set :=
   | Top    : formula
   | Bottom : formula
   | Maps   : term → term → term → map_expr → formula
diff --git a/Lib/NETList.v b/Lib/NETList.v
index 7ed6072e..1af5d07a 100644
--- a/Lib/NETList.v
+++ b/Lib/NETList.v
@@ -19,7 +19,7 @@ Inductive netlist {A : Type} (B : A → A → Type) : A → A → Type :=
 Derive Signature NoConfusion NoConfusionHom Subterm for netlist.
 
 Arguments tfin {A B i j} x.
-Arguments tadd {A B i} j {k} x xs.
+Arguments tadd {A B i} j {k} _ _.
 
 Notation "x :::: xs" := (tadd _ x xs) (at level 60, right associativity).
 
diff --git a/Lib/Setoid.v b/Lib/Setoid.v
index 7ca9739c..e6510dc2 100644
--- a/Lib/Setoid.v
+++ b/Lib/Setoid.v
@@ -1,3 +1,6 @@
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Setoids.Setoid.
+Require Import Coq.Vectors.Fin.
 Require Export Category.Lib.Foundation.
 
 Generalizable All Variables.
@@ -61,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".
diff --git a/Lib/TList.v b/Lib/TList.v
index dbaeb297..7c0a76b7 100644
--- a/Lib/TList.v
+++ b/Lib/TList.v
@@ -11,15 +11,18 @@ 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 *)
@@ -27,15 +30,13 @@ Next Obligation.
     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} x xs.
+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.
diff --git a/Lib/Tactics2.v b/Lib/Tactics2.v
new file mode 100644
index 00000000..ae1a751f
--- /dev/null
+++ b/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.
+
diff --git a/Structure/Cartesian.v b/Structure/Cartesian.v
index d16854cb..5898fd3e 100644
--- a/Structure/Cartesian.v
+++ b/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.
diff --git a/Structure/Cone.v b/Structure/Cone.v
index 2c03d783..ed7524c0 100644
--- a/Structure/Cone.v
+++ b/Structure/Cone.v
@@ -7,13 +7,16 @@ Require Import Category.Instance.Sets.
 
 Generalizable All Variables.
 
-Class ACone `(c : obj[C]) `(F : J ⟶ C) := {
+Class ACone@{u0 u1 u2 u3 u4 u5} {J : Category@{u0 u1 u2}}
+  {C : Category@{u3 u4 u5}} (c : obj[C]) (F : J ⟶ C) := {
     vertex_map (x : J) : c ~{C}~> F x;
     cone_coherence {x y : J} (f : x ~{J}~> y) :
     fmap[F] f ∘ vertex_map x ≈ vertex_map y
   }.
 
-#[export] Program Instance AConeEquiv {C J: Category}
+#[export]
+  Program Instance AConeEquiv@{u0 u1 u2 u3 u4 u5 +}
+  {J: Category@{u0 u1 u2}} {C: Category@{u3 u4 u5}}
   c (F : C ⟶ J) : Setoid (ACone c F) :=
   {| equiv := fun cone1 cone2 =>
                 forall j, @vertex_map _ _ _ _ cone1 j ≈ @vertex_map _ _ _ _ cone2 j |}.
@@ -21,9 +24,12 @@ Next Obligation.
   equivalence.
   specialize X with j. specialize X0 with j.
   exact (Equivalence_Transitive _ _ _ X X0).
-Qed.  
+Qed.
 
-Class Cone `(F : J ⟶ C) := {
+Class Cone@{u0 u1 u2 u3 u4 u5}
+  {J : Category@{u0 u1 u2}}
+  {C : Category@{u3 u4 u5}}
+  (F : J ⟶ C) := {
   vertex_obj : C;
   coneFrom : ACone vertex_obj F
 }.
@@ -42,8 +48,10 @@ Notation "Cone[ N ] F" := (ACone N F)(* . { ψ : Cone F | vertex_obj[ψ] = N } *
 Definition Cocone `(F : J ⟶ C) := Cone (F^op).
 
 #[export]
-Instance ConePresheaf `(F : J ⟶ C) : C^op ⟶ Sets.
-Proof.
+Instance ConePresheaf@{u0 u1 u2 u3 u4 u5 +}
+   {J : Category@{u0 u1 u2}} {C : Category@{u3 u4 u5}} (F : @Functor J C) :
+   @Functor C^op Sets.
+Proof. 
   unshelve eapply Build_Functor.
   - change obj[C^op] with obj[C]. 
     exact (fun c => {| carrier := Cone[c]F ; is_setoid := AConeEquiv _ _ |}).
@@ -59,5 +67,3 @@ Proof.
   - abstract(intro x; cbn; intros y j; now apply id_right).
   - abstract(cbn; intros; now apply comp_assoc).
 Defined.
-
-
diff --git a/Structure/Limit.v b/Structure/Limit.v
index 320d2c64..5d4c6e73 100644
--- a/Structure/Limit.v
+++ b/Structure/Limit.v
@@ -24,6 +24,20 @@ Class Limit `(F : J ⟶ C) := {
     vertex_map[limit_cone] ∘ u ≈ @vertex_map _ _ _ _ (@coneFrom _ _ _ N) x
 }.
 
+Class IsALimit `(F : J ⟶ C) (c : C) := {
+    limit_acone : ACone c F;
+    ump_limit : ∀ N : Cone F, ∃! u : N ~> c, ∀ x : J,
+    vertex_map _ ∘ u ≈ vertex_map x
+  }.
+
+Program Definition LimitSetoid `(F : J ⟶ C) (c : C) : Setoid (IsALimit F c) :=
+  {| equiv := fun l1 l2 => @limit_acone _ _ _ _ l1 ≈ @limit_acone _ _ _ _ l2 |}.
+Next Obligation.
+  abstract(equivalence;
+           specialize X with j; specialize X0 with j;
+           exact (Equivalence_Transitive _ _ _ X X0)).
+Defined.
+  
 Coercion limit_cone : Limit >-> Cone.
 
 Require Import Category.Functor.Opposite.
diff --git a/Structure/Limit/Cartesian.v b/Structure/Limit/Cartesian.v
index 9156bbbc..60dbdc9c 100644
--- a/Structure/Limit/Cartesian.v
+++ b/Structure/Limit/Cartesian.v
@@ -28,11 +28,12 @@ Proof.
       destruct (X (Pick_Two x y)).
       destruct limit_cone.
       simpl. change x with (fobj[Pick_Two x y] TwoDX).
-      apply (@vertex_map _ _ Two_Discrete (Pick_Two x y) _ TwoDX).
+      apply vertex_map.
     + simpl.
       destruct (X (Pick_Two x y)).
       destruct limit_cone.
-      apply (@vertex_map _ _ Two_Discrete (Pick_Two x y) _ TwoDY).
+      simpl. change y with (fobj[Pick_Two x y] TwoDY).
+      apply vertex_map.
     + proper.
       apply uniqueness; simpl; intros.
       destruct x2; simpl.
diff --git a/Structure/Pullback/Limit.v b/Structure/Pullback/Limit.v
index 29c7ffc8..15db9f87 100644
--- a/Structure/Pullback/Limit.v
+++ b/Structure/Pullback/Limit.v
@@ -25,10 +25,8 @@ Program Definition Pullback_to_Universal {C : Category}
   pullback_snd := (vertex_map _)
 |}.
 Next Obligation.
-  pose proof (@cone_coherence _ (@vertex_obj  _ _ _ (limit_cone)) _ F (coneFrom)).
   unfold unop.
-  rewrite !X.
-  reflexivity.
+  now rewrite 2 cone_coherence.
 Qed.
 Next Obligation.
   given (cone : Cone F). {
diff --git a/Structure/UniversalProperty.v b/Structure/UniversalProperty.v
new file mode 100644
index 00000000..564e2375
--- /dev/null
+++ b/Structure/UniversalProperty.v
@@ -0,0 +1,211 @@
+Require Import Category.Lib.
+Require Import Category.Lib.Tactics2.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Isomorphism.
+Require Import Category.Construction.Opposite.
+Require Import Category.Theory.Functor.
+Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Functor.Hom.
+Require Import Category.Functor.Hom.Yoneda.
+Require Import Category.Instance.Sets.
+Require Import Category.Construction.Groupoid.
+(* A predicate on objects of a category can be called a "universal property" *)
+(* if satisfying the predicate is equivalent to representing a certain functor. *)
+(* This definition of a universal property contains all examples that I am aware of
+   but I do not claim it is completely exhaustive. *)
+Class IsUniversalProperty (C : Category) (P : C → Type) (eqP : forall c, Setoid (P c)) :=
+  {
+    repr_functor : C ⟶ Sets ;
+    repr_equivalence : forall c : C,
+      @Isomorphism Sets 
+        (Build_SetoidObject (P c) (eqP c))
+        (Build_SetoidObject (Isomorphism [Hom c,─] repr_functor) _)
+  }.
+
+Lemma preyoneda {C : Category} {c d: C} {P : C^op ⟶ Sets} (τ : [Hom ─ , c] ⟹ P) :
+  forall f : d ~> c,
+    transform τ d f ≈ fmap[P] f (transform τ c id{C}).
+Proof.
+  intro f. rewrite <- (id_left f) at 1.
+  exact (symmetry (naturality τ _ d f) id{C}).
+Qed.
+ 
+#[local] Program Instance exists_setoid (A : Type) (B : Setoid A) (C : A -> Type) :
+  Setoid { x : A & C x } :=
+  { equiv := fun a b => `1 a ≈ `1 b }.
+Local Arguments morphism {x H y H0} s.
+Proposition representability_by_yoneda (C : Category) (F : C^op ⟶ Sets) (c : C):
+  @Isomorphism Sets
+    {| carrier := { x : F c & IsIsomorphism (from (Yoneda_Lemma C F c ) x) } |}
+                              
+    (Build_SetoidObject (Isomorphism [Hom ─,c] F) _) .
+Proof.
+  unshelve econstructor.
+  - unshelve econstructor.
+    + intros [elt yoneda_is_iso]. unshelve econstructor.
+      * exact (from (Yoneda_Lemma C F c) elt).
+      * exact (from (IsIsoToIso _ yoneda_is_iso)).
+      * apply is_right_inverse.
+      * apply is_left_inverse.
+    + abstract(intros [eltx x_is_iso] [elty y_is_iso] eltx_eq_elty;
+      simpl in eltx_eq_elty;
+      apply to_equiv_implies_iso_equiv; simpl;
+      intros; rewrite eltx_eq_elty; reflexivity).
+  - unshelve econstructor.
+    + simpl. intro X; simpl in X. destruct X as [Xto Xfrom tofromid fromtoid]; simpl in *.
+      exists (morphism (to (Yoneda_Lemma C F c)) Xto).
+      simpl. 
+      unshelve econstructor.
+      * exact Xfrom.
+      * abstract(simpl; intros; rewrite <- tofromid; symmetry; apply preyoneda).
+      * abstract(simpl; intros; rewrite <- preyoneda; apply fromtoid).
+    + abstract(intros x y eq; simpl; destruct eq as [e ?]; simpl in e; apply e).
+  - abstract(unshelve econstructor; simpl; intros ? ?;
+                   [ symmetry; apply preyoneda | reflexivity ]  ).
+  - abstract(simpl; intros [x f]; simpl; set (k := @fmap_id _ _ F);
+             simpl in k; apply k).
+Defined.
+
+Section UniversalProperty.
+  Context (C : Category) (P : obj[C] -> Type) (eqP : forall c, Setoid (P c))
+    (H : IsUniversalProperty C P eqP).
+
+  Proposition univ_property_unique (c : C) (t : P c) : @Unique obj[C] (ob_setoid) P.
+  Proof using eqP H.
+    exists c ; [exact t |].
+    intros v Pv.
+    set (a1 := to (repr_equivalence c)). set (a2 := to(repr_equivalence v)).
+    set (b1 := a1 t). set (b2 := a2 Pv). unfold a1, a2 in *. clear a1 a2;
+      unfold carrier in b1, b2.
+    unshelve econstructor. 
+    - exact (@two_sided_inverse _ _ _ _  (Yoneda_Embedding' C v c) (from b1 ∘ to b2)). 
+    - exact (@two_sided_inverse _ _ _ _ (Yoneda_Embedding' C c v) (from b2 ∘ to b1)). 
+    - abstract(apply (@fmap_inj _ _ (Curried_Hom C) _);
+      set (j := ( _ ( compose  _ _)));
+      set (j' := ( _ ( compose  _ _)));
+      change j with (op j);
+      change j' with (op j');
+      set (m := @fmap_comp _ _ C v c v (op j') (op j));
+      rewrite m;
+      unfold op, j, j';
+      rewrite (@is_right_inverse  _ _ _ _ (Yoneda_Embedding' C v c) (from b1 ∘ b2));
+      rewrite (@is_right_inverse  _ _ _ _ (Yoneda_Embedding' C c v) (from b2 ∘ b1));
+      simpl; intros x f; unfold op; rewrite id_right;
+      set (ab := (iso_to_from b1));
+      simpl in ab; rewrite ab;
+      rewrite (@fmap_id _ _ repr_functor x (to b2 x f));
+      simpl; clear ab;
+      set (ab' := (iso_from_to b2));
+      simpl in ab'; rewrite ab'; rewrite id_left;
+      reflexivity). 
+    - abstract(apply (@fmap_inj _ _ (Curried_Hom C) _);
+      set (j := ( _ ( compose  _ _)));
+      set (j' := ( _ ( compose  _ _)));
+      change j with (op j);
+      change j' with (op j');
+      set (m := @fmap_comp _ _ C c v c (op j') (op j));
+      rewrite m;
+      unfold op, j, j';
+      rewrite (@is_right_inverse  _ _ _ _ (Yoneda_Embedding' C v c) (from b1 ∘ b2));
+      rewrite (@is_right_inverse  _ _ _ _ (Yoneda_Embedding' C c v) (from b2 ∘ b1));
+      simpl; intros x f; unfold op; rewrite id_right;
+      set (ab := (iso_to_from b2));
+      simpl in ab; rewrite ab;
+      rewrite (@fmap_id _ _ repr_functor x (to b1 x f));
+      simpl; clear ab;
+      set (ab' := (iso_from_to b1));
+      simpl in ab'; rewrite ab'; rewrite id_left;
+      reflexivity).
+  Defined.
+
+  Proposition univ_property_respects_iso (c d : C) (iso : c ≅ d) : P c -> P d.
+  Proof using eqP H.
+    intro t.
+    rapply (from (repr_equivalence d)).
+    apply (Equivalence_Transitive (fobj[C] d) (fobj[C] c)).
+    - exact (fobj_iso _ _ _ (iso_sym (Isomorphism_Opposite iso))).
+    - apply (to (repr_equivalence c)). exact t.
+  Defined.
+
+  (* Let c, d be objects in C, and t : P c, s : P d.
+     Then there is a unique isomorphism p : c ≈ d 
+     such that the transport of p along t is equivalent to s. *)
+  Proposition univ_property_unique_up_to_unique_iso
+    (c d : C) (t : P c) (s : P d) :
+    Unique (fun p : (c ≅ d) => univ_property_respects_iso c d p t ≈ s).
+  Proof.
+    (* We have already constructed the isomorphism p.*)
+    (* We have isomorphisms Hom(c, -) ≅ repr_functor ≅ Hom(d,-)
+       corresponding to the choice of t and s, and we 
+       pull back this isomorphism Hom(c,-) ≅ Hom(d,-) along the
+       Yoneda embedding. *)
+    exists (uniqueness (univ_property_unique c t) d s).
+    - (* Why does this isomorphism respect the structure of P? *)
+      abstract(simpl; unfold univ_property_respects_iso; simpl;
+      (* Proofs of P d are in one to one correspondence 
+         with natural isomorphisms
+         Hom(d, - ) ≅ repr_functor. *)
+      (* So it suffices to show that these determine the same natural isomorphism. *)
+      rapply (snd (injectivity_is_monic _) (iso_to_monic (repr_equivalence d)));
+      set (M := (iso_to_from (repr_equivalence d)));
+        simpl in M; rewrite M; clear M;
+      apply to_equiv_implies_iso_equiv;
+      intros j u; simpl in u;
+      simpl;
+      set (ab :=  (to (repr_equivalence c )) );
+      assert (K := @naturality _ _ _ _ (to (ab t)) _ _ u);
+      simpl in K;
+      rewrite <- K;
+      clear K;
+      set (A := iso_to_from (ab t) d); simpl in A; unfold op; rewrite A; clear A;
+      set (aj := to (repr_equivalence d ));
+      set (aj' := to (aj s));
+      change (@id C d) with (@id (C^op) d);
+      rewrite <- 2 (@preyoneda (C^op) _ _ repr_functor aj');
+               reflexivity).
+    - (* The isomorphism is unique. *)
+      (* The canonical isomorphism c ≌ d "carrying" t to s is defined as follows: *)
+      (* rep_c : Hom(c, -) ≌ repr_functor *)
+      (* rep_d : Hom(d, -) ≌ repr_functor *)
+      (* rep_c ^-1 ∘ rep_d : Hom(d,-) -> repr_functor -> Hom(c, -) *)
+      (* " ... " d id_d : Hom(c, d) *)
+      (* p := rep_c^-1 ∘ rep_d d id_d. *)
+      (* OTOH, by assumption, we have - 
+         y(v) : Hom(d, -) ≌ Hom(c, -)
+         rep_c : Hom(c, -) ≌ repr_functor
+         rep_d : Hom(d, -) ≌ repr_functor *)
+      (* and the natural isomorphism Hom(d, -) ≌ repr_functor given by *)
+      (* rep_c ∘ y(v) : Hom(d, -)  ≌ Hom(c, -) ≌ repr_functor *)
+      (* corresonds to s across the bijection. *)
+      (* Of couse since by construction, s also corresponds to rep_d, *)
+      (* this means that  rep_c ∘ y(v) ≈ rep_d as isomorphisms Hom(d,-) ≈ repr_functor. *)
+      (* Thus y(v) ≈ rep_c^-1 ∘ rep_d : Hom(d,-) ≅ Hom(c,-) and in particular 
+         they agree at (d, id{C} d).  *)
+      abstract(intros v respects_iso;
+      simpl uniqueness;
+      apply to_equiv_implies_iso_equiv; simpl;
+      unfold univ_property_respects_iso, Equivalence_Transitive in respects_iso;
+        simpl in respects_iso;
+      set (v' := iso_sym (Isomorphism_Opposite v)) in *;
+      set (yv := fobj_iso C d c v') in *;
+      rewrite <- (id_left (to v));
+      change (id{C} ∘ to v) with (to yv d id{C});
+      change (from (to (repr_equivalence c) t) d (to (to (repr_equivalence d) s) d id)) with
+        (((from (to (repr_equivalence c) t)) ∘ (to (to (repr_equivalence d) s))) d id);
+      cut ((iso_sym (to (repr_equivalence c) t)) ⊙ ( (to (repr_equivalence d) s)) ≈ yv);
+               [ intro a; destruct a as [a _]; simpl in a; apply a |];
+      apply (@proper_morphism _ _ _ _ (to (repr_equivalence d))) in respects_iso;
+      assert (K := (iso_to_from (repr_equivalence d)));
+      simpl in K; rewrite K in respects_iso; clear K;
+      apply (@compose_respects (Groupoid (@Fun.Fun C Sets)) _ _ _
+               (iso_sym (to (repr_equivalence c) t)) (iso_sym (to (repr_equivalence c) t))
+               (Equivalence_Reflexive _ ))
+              in respects_iso;
+      rewrite comp_assoc in respects_iso; simpl in respects_iso;
+      rewrite iso_sym_left_inverse in respects_iso;
+      change iso_id with (@id (Groupoid (@Fun.Fun C Sets)) (fobj[C] c)) in respects_iso;
+      rewrite (@id_left (Groupoid (@Fun.Fun C Sets))) in respects_iso;
+      symmetry in respects_iso;
+      exact respects_iso).
+  Defined.      
+End UniversalProperty.
diff --git a/Structure/UniversalProperty/Cartesian'.v~ b/Structure/UniversalProperty/Cartesian'.v~
new file mode 100644
index 00000000..a6abd398
--- /dev/null
+++ b/Structure/UniversalProperty/Cartesian'.v~
@@ -0,0 +1,259 @@
+Require Import Category.Lib.
+Require Import Category.Lib.Tactics2.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Isomorphism.
+Require Import Category.Construction.Opposite.
+Require Import Category.Theory.Functor.
+Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Functor.Hom.
+Require Import Category.Instance.Sets.
+Require Import Category.Instance.Sets.Cartesian.
+Require Import Category.Instance.Fun.Cartesian.
+Require Import Category.Structure.Cartesian.
+Require Import Category.Structure.UniversalProperty.
+
+Local Hint Extern 5 (hom ?z ?x) => apply (@exl' _ x _ z (ltac:(typeclasses eauto))) : cat.
+Local Hint Extern 5 (hom ?z ?y) => apply (@exr' _ _ y z (ltac:(typeclasses eauto))) : cat.
+Local Hint Extern 5 (Proper _ _ ) => progress(repeat(intro)) : cat.
+    
+#[local] Hint Rewrite @exl_fork : categories.
+#[local] Hint Rewrite @exr_fork : categories.
+
+
+Section ACartesianProduct.
+  Lemma exl'_fork_comp {C : Category} {w x y z p} (f : x ~> y) (g : x ~> z) (h : w ~> x)
+    (H : IsCartesianProduct y z p) :
+    exl' ∘ (fork' f g ∘ h) ≈ f ∘ h.
+  Proof.
+    rewrite comp_assoc.
+    rewrite exl'_fork.
+    reflexivity.
+  Qed.
+  Lemma exr'_fork_comp {C : Category} {w x y z p} (f : x ~> y) (g : x ~> z) (h : w ~> x)
+    (H : IsCartesianProduct y z p) :
+    exr' ∘ (fork' f g ∘ h) ≈ g ∘ h.
+  Proof.
+    rewrite comp_assoc.
+    rewrite exr'_fork.
+    reflexivity.
+  Qed.
+End ACartesianProduct.
+
+Lemma preyoneda {C : Category} {c d: C} {P : C^op ⟶ Sets} (τ : [Hom ─ , c] ⟹ P) :
+  forall f : d ~> c,
+    transform τ d f ≈ fmap[P] f (transform τ c id{C}).
+Proof.
+  intro f. rewrite <- (id_left f) at 1.
+  exact (symmetry (naturality τ _ d f) id{C}).
+Qed.
+
+Section CartesianProductUniversalProperty.
+  Context (C : Category).
+  Context (x y : C).
+  
+  Set Warnings "-non-reversible-notation".
+  Notation next_field X
+    := ltac:(let c := type of X in match c with forall _ : ?A, _  => exact A end).
+  Set Warnings "non-reversible-notation".
+  
+  Let prod_is_univ_property :=
+      Build_IsUniversalProperty C^op
+       (fun z => IsCartesianProduct x y z)
+       (fun z => CartesianProductStructuresEquiv x y z)
+       ([Hom ─ , x ] × [Hom ─ , y ]).
+  Section allC.
+    Context (z : C).
+     (* IsCartesianProduct x y z
+       ≊ fobj[C^op] z ≅ fobj[Curried_CoHom C] x × fobj[Curried_CoHom C] y : Type] *)
+    Let master_iso := Eval hnf in ltac:(
+                      (let A := (eval hnf in (next_field prod_is_univ_property)) in
+                       match A with
+                       | forall a : _, @?B a => exact(B z)
+                       end)).
+    Let Build_Iso := Eval hnf in ltac:(let A := (eval hnf in master_iso) in
+                           match A with
+                           | @Isomorphism ?a ?b ?c => exact(@Build_Isomorphism a b c)
+                           end).
+    Let master_iso_to := next_field Build_Iso.
+
+    Let Build_to := Eval hnf in ltac:(let A := (eval hnf in master_iso_to) in
+                           match A with
+                           | @SetoidMorphism ?x ?sx ?y ?sy =>
+                               exact(@Build_SetoidMorphism x sx y sy)
+                           end).
+    Let master_iso_to_underlying := next_field Build_to.
+    Proposition cartesian_prod_struct_to_representable : master_iso_to_underlying.
+    Proof using Type.
+      clear prod_is_univ_property Build_Iso Build_to master_iso master_iso_to.
+      unfold master_iso_to_underlying; clear master_iso_to_underlying.
+      intro A; simpl in A.
+      cbn . 
+      unshelve econstructor.
+      - simpl. unshelve econstructor.
+        + intro a. simpl. unshelve econstructor.
+          * auto with cat. 
+          * abstract(auto with cat).
+        + abstract(simpl; intros; auto with cat).
+        + abstract(simpl; intros; auto with cat).
+      - simpl. unshelve econstructor.
+        + intro a. simpl. unshelve econstructor.
+          * intros [m n]. now apply fork'.
+          * abstract(eintros [? ?] [? ?] [eqm eqn]; now apply fork'_respects).
+        + abstract(simpl; intros ? ? ? [? ?]; simpl;
+          apply ump_product; split; 
+            [ exact (exl'_fork_comp _ _ _ _) | exact (exr'_fork_comp _ _ _ _) ]).
+        + abstract(simpl; intros ? ? ? [? ?]; simpl; symmetry; apply ump_product; split;
+                   [ exact (exl'_fork_comp _ _ _ _) | exact (exr'_fork_comp _ _ _ _) ]).
+      - abstract(simpl; intros t [p q]; split; 
+                 [ rewrite exl'_fork; now autorewrite with categories |
+                   rewrite exr'_fork; now autorewrite with categories ] ).
+      - abstract(simpl; intros a f; symmetry;
+                 apply ump_product; split; now autorewrite with categories).
+    Defined.
+
+    Let prod_to_representable_proper :=
+          next_field (Build_to cartesian_prod_struct_to_representable).
+    Proposition to_is_proper : prod_to_representable_proper.
+    Proof using Type.
+      unfold prod_to_representable_proper, cartesian_prod_struct_to_representable.
+      clear prod_to_representable_proper.
+      clear prod_is_univ_property Build_Iso Build_to master_iso master_iso_to
+        master_iso_to_underlying.
+      simpl. intros X Y [eq1 eq2]. unshelve econstructor.
+      + simpl; intros c f; split; auto with cat.
+      + simpl. intros c [f1 f2]. apply ump_product; split.
+        * rewrite <- eq1; apply exl'_fork.
+        * rewrite <- eq2; apply exr'_fork.
+    Qed.
+
+    Let to := Build_to cartesian_prod_struct_to_representable to_is_proper.
+    Let master_iso_from := Eval hnf in (next_field (Build_Iso to)).
+    Let Build_from := Eval hnf in ltac:(let A := (eval hnf in master_iso_from) in
+                           match A with
+                           | @SetoidMorphism ?x ?sx ?y ?sy =>
+                               exact(@Build_SetoidMorphism x sx y sy)
+                           end).
+    Let master_iso_from_underlying := next_field Build_from.
+    Proposition representable_to_cartesian_prod_struct : master_iso_from_underlying.
+    Proof using Type.
+      unfold master_iso_from_underlying; clear master_iso_from_underlying.
+      clear Build_from master_iso_from to prod_to_representable_proper
+        master_iso_to_underlying Build_to master_iso_to Build_Iso master_iso
+        prod_is_univ_property.
+      
+      intros [[to_trans to_nat ?] [from_trans from_nat ?] c d]. 
+              simpl in c, d.
+      simpl. (* set (j := trans z (@id _ z)). simpl in j; destruct j as [ll rr]. *)
+      unshelve econstructor.
+      - exact (fun a f g => from_trans a (f, g)).
+      - exact (fst (to_trans z (@id _ z))).
+      - exact (snd (to_trans z (@id _ z))).
+      - abstract(intro a; repeat(intro); now apply (proper_morphism (from_trans a))).
+      - intros a f g h; split; clear naturality_sym naturality_sym0; simpl in to_nat, from_nat. 
+        + abstract(
+            intro m; split; rewrite m; specialize c with a (f,g); destruct c as [feq geq];
+            simpl in feq, geq; rewrite id_right in feq; rewrite id_right in geq;
+            destruct (to_nat z a (from_trans a (f, g)) id{C}) as [fst_eq snd_eq];
+            symmetry; [ rewrite <- feq at 1 | rewrite <- geq at 1] ; symmetry;
+            rewrite id_left in fst_eq; rewrite id_left in snd_eq;
+            [ now apply fst_eq | now apply snd_eq ]).
+        + abstract(intros [t s];
+          rewrite <- id_right; symmetry; rewrite <- (d a h);
+          destruct (to_nat z a h id{C}) as [fst_eq snd_eq];
+          apply (proper_morphism (from_trans a)); split; simpl; symmetry;
+            rewrite <- (id_left h); [ now rewrite <- fst_eq | now rewrite <- snd_eq ]).
+    Defined.
+
+    Let representable_to_prod_proper :=
+          next_field (Build_from representable_to_cartesian_prod_struct).
+
+    (* Proper (equiv ==> equiv) representable_to_cartesian_prod_struct *)
+    Proposition from_is_proper : representable_to_prod_proper.
+    Proof using Type.
+      unfold representable_to_prod_proper; clear representable_to_prod_proper.
+      unfold representable_to_cartesian_prod_struct.
+      clear master_iso_from_underlying
+        Build_from
+        master_iso_from
+        to
+        prod_to_representable_proper
+        master_iso_to_underlying
+        Build_Iso
+        Build_to
+        master_iso_to
+        master_iso
+        prod_is_univ_property.
+      
+      intros a b eq; simpl; split; simpl in eq; unfold iso_equiv in eq;
+        destruct eq as [to_eq from_eq]; simpl in to_eq.
+      - exact (fst (to_eq z id{C})).
+      - exact (snd (to_eq z id{C})).
+    Qed.
+    Let from := Build_SetoidMorphism _ _ _ _ _ from_is_proper.
+
+    (* This proves that a Cartesian product structure is _logically_ equivalent
+       to the object representing a certain functor, but we need to construct the isomorphism. *)
+    (* Let tofrom_id := next_field (@Build_Isomorphism Sets _ _ to from). *)
+
+    Local Arguments transform {C D F G}.
+    
+    Proposition tofrom_id : @compose Sets _ _ _ to from ≈ id{Sets}.
+    Proof.
+      unfold to, from, representable_to_cartesian_prod_struct, Build_to,
+        cartesian_prod_struct_to_representable.
+      clear from.
+      intro T. simpl.
+      apply to_equiv_implies_iso_equiv; simpl.
+      intros c x1.
+      clear representable_to_prod_proper
+        master_iso_from_underlying
+        Build_from
+        master_iso_from
+        to
+        prod_to_representable_proper
+        master_iso_to_underlying
+        Build_to
+        master_iso_to
+        Build_Iso
+        master_iso
+        prod_is_univ_property.
+      split; destruct T as [Tto Tfrom T_tofromiso T_fromtoiso]; simpl;
+        rewrite (preyoneda _ x1);
+        set (X := fobj[Curried_CoHom C] x); set (Y := fobj[Curried_CoHom C] y).
+      - set (l := (@exl (@Fun.Fun C^op Sets) _ X Y)).
+        change (fst (fmap[X × Y] x1 (Tto z id{C}))) with
+          ((transform l _ ∘ (fmap[X × Y] x1)) (Tto z id{C})).
+        now rewrite <- (naturality l _ c x1 (Tto z id{C})).
+      - set (r := (@exr (@Fun.Fun C^op Sets) _ X Y)).
+        change (snd (fmap[X × Y] x1 (Tto z id{C}))) with
+          ((transform r _ ∘ (fmap[X × Y] x1)) (Tto z id{C})).
+        now rewrite <- (naturality r _ c x1 (Tto z id{C})).
+    Qed.
+
+    Proposition fromto_id : @compose Sets _ _ _ from to ≈ id{Sets}.
+    Proof using Type.
+      unfold to, from, representable_to_cartesian_prod_struct, Build_to,
+        cartesian_prod_struct_to_representable.
+      clear from.
+      intro T. simpl.
+      clear representable_to_prod_proper
+        master_iso_from_underlying
+        Build_from
+        master_iso_from
+        to
+        prod_to_representable_proper
+        master_iso_to_underlying
+        Build_to
+        master_iso_to
+        Build_Iso
+        master_iso
+        prod_is_univ_property.
+
+      split; rewrite id_right; reflexivity.
+      Qed.
+
+    Definition allC := Build_Iso to from tofrom_id fromto_id.
+  End allC.
+
+  Definition CartesianProductUniversalProperty := Eval hnf in prod_is_univ_property allC.
+End CartesianProductUniversalProperty.
diff --git a/Structure/UniversalProperty/Cartesian.v b/Structure/UniversalProperty/Cartesian.v
new file mode 100644
index 00000000..50cfa9af
--- /dev/null
+++ b/Structure/UniversalProperty/Cartesian.v
@@ -0,0 +1,89 @@
+Require Import Category.Lib.
+Require Import Category.Lib.Tactics2.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Isomorphism.
+Require Import Category.Construction.Opposite.
+Require Import Category.Theory.Functor.
+Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Functor.Hom.
+Require Import Category.Instance.Sets.
+Require Import Category.Instance.Sets.Cartesian.
+Require Import Category.Instance.Fun.Cartesian.
+Require Import Category.Structure.Cartesian.
+Require Import Category.Structure.UniversalProperty.
+
+Local Hint Extern 5 (hom ?z ?x) => apply (@exl' _ x _ z (ltac:(typeclasses eauto))) : cat.
+Local Hint Extern 5 (hom ?z ?y) => apply (@exr' _ _ y z (ltac:(typeclasses eauto))) : cat.
+Local Hint Extern 5 (Proper _ _ ) => progress(repeat(intro)) : cat.
+    
+#[local] Hint Rewrite @exl_fork : categories.
+#[local] Hint Rewrite @exr_fork : categories.
+
+Section CartesianProduct.
+  Context (C : Category).
+  Context (x y : C).
+  Proposition CartesianProductIsUniversalProperty :
+    IsUniversalProperty C^op (fun z => IsCartesianProduct x y z)
+                            (fun z => CartesianProductStructuresEquiv x y z).
+  Proof.
+    unshelve econstructor; [ exact ([Hom ─ , x ] × [Hom ─ , y ]) |].
+    intro z; unshelve econstructor.
+    - simpl. unshelve econstructor.
+      + intro H. unshelve econstructor.
+        * simpl. unshelve eapply Build_Transform'.
+          -- intro a. simpl. unshelve econstructor.
+             ++ auto with cat.
+             ++ abstract(auto with cat).
+          -- abstract(simpl; auto with cat).
+        * simpl. unshelve eapply Build_Transform'.
+          -- intro a. unshelve econstructor.
+             ++ simpl. intros [? ?]. now apply fork'.
+             ++ abstract(repeat(intro); destruct x0, y0, X; simpl in *;
+                now apply fork'_respects).
+          -- abstract(simpl; intros w s f [a b]; simpl; apply ump_product; split;
+                      [ now rewrite comp_assoc, exl'_fork |
+                        now rewrite comp_assoc, exr'_fork]).
+        * abstract(simpl; intros w [f g]; split;
+                   [ rewrite exl'_fork | rewrite exr'_fork];
+                    now autorewrite with categories ).
+        * abstract(simpl; intros; rewrite id_right; symmetry;
+                   apply ump_product; split; reflexivity).
+      + abstract(simpl; intros F G [eq1 eq2]; apply to_equiv_implies_iso_equiv;
+                 simpl; intros; split; apply compose_respects; auto with cat).
+    - simpl. unshelve econstructor.
+      + intro X. 
+        destruct X as [[X_to_transform X_to_naturality ?]
+                         [X_from_transform X_from_naturality ?]
+                         X_tofromid X_fromtoid ]. simpl in *.
+        simpl in X_to_transform, X_from_transform.
+        clear naturality_sym naturality_sym0.
+        unshelve econstructor.
+        * intros a f g. 
+          exact (X_from_transform a (f, g)).
+        * exact (fst (X_to_transform z id{C})).
+        * exact (snd (X_to_transform z id{C})).
+        * abstract(intros a ? ? ? ? ? ?;
+          apply (proper_morphism (X_from_transform a));
+                   split; auto).
+        * simpl in *. intros; split.
+          -- abstract(
+             intro heq; split; specialize X_to_naturality with _ _ h (id{C});
+               destruct X_to_naturality as [fst' snd'];
+               [ now rewrite fst', id_left, heq,
+                 (fst (X_tofromid _ _)), id_right |
+                 now rewrite snd', id_left, heq,
+                 (snd (X_tofromid _ _)), id_right ]).
+          -- abstract(intros [l r]; now rewrite <- l, <- r, <- X_from_naturality,
+               X_fromtoid, 2 id_left).
+      + abstract(
+          intros [Ftrans Fnat ?] [Gtrans Gnat ?] [eqto eqfrom]; simpl in *; apply (eqto _ _)).
+    - abstract(simpl; intros [[iso_to_transform iso_to_nat ?]
+                       [iso_from_transform iso_from_nat ?]
+                       tofrom_id fromto_id]; simpl in *;
+               apply to_equiv_implies_iso_equiv; simpl;
+               intros c f; assert (j:= (iso_to_nat z c f id{C})); 
+               set (m := f) at 2 4; split;
+               rewrite <- (id_left m); [ exact (fst j) | exact (snd j)]).
+    - abstract(simpl; intro a; split; now rewrite id_right).
+  Defined.
+End CartesianProduct.
diff --git a/Structure/UniversalProperty/Cartesian.v~ b/Structure/UniversalProperty/Cartesian.v~
new file mode 100644
index 00000000..a6abd398
--- /dev/null
+++ b/Structure/UniversalProperty/Cartesian.v~
@@ -0,0 +1,259 @@
+Require Import Category.Lib.
+Require Import Category.Lib.Tactics2.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Isomorphism.
+Require Import Category.Construction.Opposite.
+Require Import Category.Theory.Functor.
+Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Functor.Hom.
+Require Import Category.Instance.Sets.
+Require Import Category.Instance.Sets.Cartesian.
+Require Import Category.Instance.Fun.Cartesian.
+Require Import Category.Structure.Cartesian.
+Require Import Category.Structure.UniversalProperty.
+
+Local Hint Extern 5 (hom ?z ?x) => apply (@exl' _ x _ z (ltac:(typeclasses eauto))) : cat.
+Local Hint Extern 5 (hom ?z ?y) => apply (@exr' _ _ y z (ltac:(typeclasses eauto))) : cat.
+Local Hint Extern 5 (Proper _ _ ) => progress(repeat(intro)) : cat.
+    
+#[local] Hint Rewrite @exl_fork : categories.
+#[local] Hint Rewrite @exr_fork : categories.
+
+
+Section ACartesianProduct.
+  Lemma exl'_fork_comp {C : Category} {w x y z p} (f : x ~> y) (g : x ~> z) (h : w ~> x)
+    (H : IsCartesianProduct y z p) :
+    exl' ∘ (fork' f g ∘ h) ≈ f ∘ h.
+  Proof.
+    rewrite comp_assoc.
+    rewrite exl'_fork.
+    reflexivity.
+  Qed.
+  Lemma exr'_fork_comp {C : Category} {w x y z p} (f : x ~> y) (g : x ~> z) (h : w ~> x)
+    (H : IsCartesianProduct y z p) :
+    exr' ∘ (fork' f g ∘ h) ≈ g ∘ h.
+  Proof.
+    rewrite comp_assoc.
+    rewrite exr'_fork.
+    reflexivity.
+  Qed.
+End ACartesianProduct.
+
+Lemma preyoneda {C : Category} {c d: C} {P : C^op ⟶ Sets} (τ : [Hom ─ , c] ⟹ P) :
+  forall f : d ~> c,
+    transform τ d f ≈ fmap[P] f (transform τ c id{C}).
+Proof.
+  intro f. rewrite <- (id_left f) at 1.
+  exact (symmetry (naturality τ _ d f) id{C}).
+Qed.
+
+Section CartesianProductUniversalProperty.
+  Context (C : Category).
+  Context (x y : C).
+  
+  Set Warnings "-non-reversible-notation".
+  Notation next_field X
+    := ltac:(let c := type of X in match c with forall _ : ?A, _  => exact A end).
+  Set Warnings "non-reversible-notation".
+  
+  Let prod_is_univ_property :=
+      Build_IsUniversalProperty C^op
+       (fun z => IsCartesianProduct x y z)
+       (fun z => CartesianProductStructuresEquiv x y z)
+       ([Hom ─ , x ] × [Hom ─ , y ]).
+  Section allC.
+    Context (z : C).
+     (* IsCartesianProduct x y z
+       ≊ fobj[C^op] z ≅ fobj[Curried_CoHom C] x × fobj[Curried_CoHom C] y : Type] *)
+    Let master_iso := Eval hnf in ltac:(
+                      (let A := (eval hnf in (next_field prod_is_univ_property)) in
+                       match A with
+                       | forall a : _, @?B a => exact(B z)
+                       end)).
+    Let Build_Iso := Eval hnf in ltac:(let A := (eval hnf in master_iso) in
+                           match A with
+                           | @Isomorphism ?a ?b ?c => exact(@Build_Isomorphism a b c)
+                           end).
+    Let master_iso_to := next_field Build_Iso.
+
+    Let Build_to := Eval hnf in ltac:(let A := (eval hnf in master_iso_to) in
+                           match A with
+                           | @SetoidMorphism ?x ?sx ?y ?sy =>
+                               exact(@Build_SetoidMorphism x sx y sy)
+                           end).
+    Let master_iso_to_underlying := next_field Build_to.
+    Proposition cartesian_prod_struct_to_representable : master_iso_to_underlying.
+    Proof using Type.
+      clear prod_is_univ_property Build_Iso Build_to master_iso master_iso_to.
+      unfold master_iso_to_underlying; clear master_iso_to_underlying.
+      intro A; simpl in A.
+      cbn . 
+      unshelve econstructor.
+      - simpl. unshelve econstructor.
+        + intro a. simpl. unshelve econstructor.
+          * auto with cat. 
+          * abstract(auto with cat).
+        + abstract(simpl; intros; auto with cat).
+        + abstract(simpl; intros; auto with cat).
+      - simpl. unshelve econstructor.
+        + intro a. simpl. unshelve econstructor.
+          * intros [m n]. now apply fork'.
+          * abstract(eintros [? ?] [? ?] [eqm eqn]; now apply fork'_respects).
+        + abstract(simpl; intros ? ? ? [? ?]; simpl;
+          apply ump_product; split; 
+            [ exact (exl'_fork_comp _ _ _ _) | exact (exr'_fork_comp _ _ _ _) ]).
+        + abstract(simpl; intros ? ? ? [? ?]; simpl; symmetry; apply ump_product; split;
+                   [ exact (exl'_fork_comp _ _ _ _) | exact (exr'_fork_comp _ _ _ _) ]).
+      - abstract(simpl; intros t [p q]; split; 
+                 [ rewrite exl'_fork; now autorewrite with categories |
+                   rewrite exr'_fork; now autorewrite with categories ] ).
+      - abstract(simpl; intros a f; symmetry;
+                 apply ump_product; split; now autorewrite with categories).
+    Defined.
+
+    Let prod_to_representable_proper :=
+          next_field (Build_to cartesian_prod_struct_to_representable).
+    Proposition to_is_proper : prod_to_representable_proper.
+    Proof using Type.
+      unfold prod_to_representable_proper, cartesian_prod_struct_to_representable.
+      clear prod_to_representable_proper.
+      clear prod_is_univ_property Build_Iso Build_to master_iso master_iso_to
+        master_iso_to_underlying.
+      simpl. intros X Y [eq1 eq2]. unshelve econstructor.
+      + simpl; intros c f; split; auto with cat.
+      + simpl. intros c [f1 f2]. apply ump_product; split.
+        * rewrite <- eq1; apply exl'_fork.
+        * rewrite <- eq2; apply exr'_fork.
+    Qed.
+
+    Let to := Build_to cartesian_prod_struct_to_representable to_is_proper.
+    Let master_iso_from := Eval hnf in (next_field (Build_Iso to)).
+    Let Build_from := Eval hnf in ltac:(let A := (eval hnf in master_iso_from) in
+                           match A with
+                           | @SetoidMorphism ?x ?sx ?y ?sy =>
+                               exact(@Build_SetoidMorphism x sx y sy)
+                           end).
+    Let master_iso_from_underlying := next_field Build_from.
+    Proposition representable_to_cartesian_prod_struct : master_iso_from_underlying.
+    Proof using Type.
+      unfold master_iso_from_underlying; clear master_iso_from_underlying.
+      clear Build_from master_iso_from to prod_to_representable_proper
+        master_iso_to_underlying Build_to master_iso_to Build_Iso master_iso
+        prod_is_univ_property.
+      
+      intros [[to_trans to_nat ?] [from_trans from_nat ?] c d]. 
+              simpl in c, d.
+      simpl. (* set (j := trans z (@id _ z)). simpl in j; destruct j as [ll rr]. *)
+      unshelve econstructor.
+      - exact (fun a f g => from_trans a (f, g)).
+      - exact (fst (to_trans z (@id _ z))).
+      - exact (snd (to_trans z (@id _ z))).
+      - abstract(intro a; repeat(intro); now apply (proper_morphism (from_trans a))).
+      - intros a f g h; split; clear naturality_sym naturality_sym0; simpl in to_nat, from_nat. 
+        + abstract(
+            intro m; split; rewrite m; specialize c with a (f,g); destruct c as [feq geq];
+            simpl in feq, geq; rewrite id_right in feq; rewrite id_right in geq;
+            destruct (to_nat z a (from_trans a (f, g)) id{C}) as [fst_eq snd_eq];
+            symmetry; [ rewrite <- feq at 1 | rewrite <- geq at 1] ; symmetry;
+            rewrite id_left in fst_eq; rewrite id_left in snd_eq;
+            [ now apply fst_eq | now apply snd_eq ]).
+        + abstract(intros [t s];
+          rewrite <- id_right; symmetry; rewrite <- (d a h);
+          destruct (to_nat z a h id{C}) as [fst_eq snd_eq];
+          apply (proper_morphism (from_trans a)); split; simpl; symmetry;
+            rewrite <- (id_left h); [ now rewrite <- fst_eq | now rewrite <- snd_eq ]).
+    Defined.
+
+    Let representable_to_prod_proper :=
+          next_field (Build_from representable_to_cartesian_prod_struct).
+
+    (* Proper (equiv ==> equiv) representable_to_cartesian_prod_struct *)
+    Proposition from_is_proper : representable_to_prod_proper.
+    Proof using Type.
+      unfold representable_to_prod_proper; clear representable_to_prod_proper.
+      unfold representable_to_cartesian_prod_struct.
+      clear master_iso_from_underlying
+        Build_from
+        master_iso_from
+        to
+        prod_to_representable_proper
+        master_iso_to_underlying
+        Build_Iso
+        Build_to
+        master_iso_to
+        master_iso
+        prod_is_univ_property.
+      
+      intros a b eq; simpl; split; simpl in eq; unfold iso_equiv in eq;
+        destruct eq as [to_eq from_eq]; simpl in to_eq.
+      - exact (fst (to_eq z id{C})).
+      - exact (snd (to_eq z id{C})).
+    Qed.
+    Let from := Build_SetoidMorphism _ _ _ _ _ from_is_proper.
+
+    (* This proves that a Cartesian product structure is _logically_ equivalent
+       to the object representing a certain functor, but we need to construct the isomorphism. *)
+    (* Let tofrom_id := next_field (@Build_Isomorphism Sets _ _ to from). *)
+
+    Local Arguments transform {C D F G}.
+    
+    Proposition tofrom_id : @compose Sets _ _ _ to from ≈ id{Sets}.
+    Proof.
+      unfold to, from, representable_to_cartesian_prod_struct, Build_to,
+        cartesian_prod_struct_to_representable.
+      clear from.
+      intro T. simpl.
+      apply to_equiv_implies_iso_equiv; simpl.
+      intros c x1.
+      clear representable_to_prod_proper
+        master_iso_from_underlying
+        Build_from
+        master_iso_from
+        to
+        prod_to_representable_proper
+        master_iso_to_underlying
+        Build_to
+        master_iso_to
+        Build_Iso
+        master_iso
+        prod_is_univ_property.
+      split; destruct T as [Tto Tfrom T_tofromiso T_fromtoiso]; simpl;
+        rewrite (preyoneda _ x1);
+        set (X := fobj[Curried_CoHom C] x); set (Y := fobj[Curried_CoHom C] y).
+      - set (l := (@exl (@Fun.Fun C^op Sets) _ X Y)).
+        change (fst (fmap[X × Y] x1 (Tto z id{C}))) with
+          ((transform l _ ∘ (fmap[X × Y] x1)) (Tto z id{C})).
+        now rewrite <- (naturality l _ c x1 (Tto z id{C})).
+      - set (r := (@exr (@Fun.Fun C^op Sets) _ X Y)).
+        change (snd (fmap[X × Y] x1 (Tto z id{C}))) with
+          ((transform r _ ∘ (fmap[X × Y] x1)) (Tto z id{C})).
+        now rewrite <- (naturality r _ c x1 (Tto z id{C})).
+    Qed.
+
+    Proposition fromto_id : @compose Sets _ _ _ from to ≈ id{Sets}.
+    Proof using Type.
+      unfold to, from, representable_to_cartesian_prod_struct, Build_to,
+        cartesian_prod_struct_to_representable.
+      clear from.
+      intro T. simpl.
+      clear representable_to_prod_proper
+        master_iso_from_underlying
+        Build_from
+        master_iso_from
+        to
+        prod_to_representable_proper
+        master_iso_to_underlying
+        Build_to
+        master_iso_to
+        Build_Iso
+        master_iso
+        prod_is_univ_property.
+
+      split; rewrite id_right; reflexivity.
+      Qed.
+
+    Definition allC := Build_Iso to from tofrom_id fromto_id.
+  End allC.
+
+  Definition CartesianProductUniversalProperty := Eval hnf in prod_is_univ_property allC.
+End CartesianProductUniversalProperty.
diff --git a/Structure/UniversalProperty/Limit'.v~ b/Structure/UniversalProperty/Limit'.v~
new file mode 100644
index 00000000..fbd2dca0
--- /dev/null
+++ b/Structure/UniversalProperty/Limit'.v~
@@ -0,0 +1,156 @@
+Require Import Category.Lib.
+Require Import Category.Lib.Tactics2.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Isomorphism.
+Require Import Category.Construction.Opposite.
+Require Import Category.Theory.Functor.
+Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Functor.Hom.
+Require Import Category.Instance.Sets.
+Require Import Category.Structure.UniversalProperty.
+Require Import Category.Structure.Cone.
+Require Import Category.Structure.Limit.
+Require Import Category.Functor.Hom.Yoneda.
+
+Section LimitUniversalProperty.
+  Context (J C : Category).
+  Context (F : J ⟶ C).
+
+  Definition ump_limit_construct (a z : C) (H : IsALimit F z) :
+      ACone a F -> a ~> z.
+  Proof.
+    destruct H.
+    intro m; specialize ump_limit with {| vertex_obj := a ; coneFrom := m |}.
+    destruct ump_limit as [unique_obj ? ?].
+    exact unique_obj.
+  Defined.
+
+  Proposition ump_limit_construct_proper (a z : C) (H : IsALimit F z) :
+    Proper (equiv ==> equiv) (ump_limit_construct a z H).
+  Proof.
+    repeat(intro).
+    unfold ump_limit_construct.
+    apply uniqueness. simpl.
+    intro j.
+    set (k := (unique_property (ump_limit {| vertex_obj := a ; coneFrom := y |}))).
+    destruct x, y; simpl in X.
+    simpl in *; rewrite X; apply k.
+  Qed.
+
+  Local Arguments vertex_map {J C c F}.
+  Proposition ump_limit_construct_recover (w z : C) (H : IsALimit F z) (m : obj[J])
+     (a : ACone w F) : vertex_map limit_acone m ∘ (ump_limit_construct w z _ a) ≈ vertex_map a m.
+  Proof.
+    unfold ump_limit_construct. simpl. 
+    exact (unique_property (ump_limit {| vertex_obj := w; coneFrom :=a |} ) _).
+  Qed.
+
+  Proposition ump_limit_construct_recover' (q w z : C) (H : IsALimit F z) (m : obj[J])
+    (a : ACone w F) (f : q ~> w) :
+    vertex_map limit_acone m ∘ (ump_limit_construct w z _ a ∘ f) ≈ vertex_map a m ∘ f.
+  Proof.
+    now rewrite comp_assoc, ump_limit_construct_recover.
+  Qed.
+  
+  Create HintDb limit discriminated.
+  Hint Resolve ump_limit_construct : limit.
+  Hint Resolve ump_limit_construct_proper : limit.
+  Hint Resolve vertex_map : limit.
+  Hint Resolve limit_acone : limit.
+  Hint Rewrite -> @cone_coherence : limit.
+  Hint Rewrite -> ump_limit_construct_recover : limit.
+  Hint Rewrite -> ump_limit_construct_recover' : limit.
+
+  Proposition cone_equiv_to_morphism_equiv (c z : C) (H : IsALimit F z) (f g : c ~> z) :
+    (forall a : J, vertex_map limit_acone a ∘ f ≈ vertex_map limit_acone a ∘ g) ->
+    f ≈ g.
+  Proof.
+    intro e.
+    set (C' := fmap[ConePresheaf F] f limit_acone).
+    assert (A: (unique_obj (ump_limit {| vertex_obj := c ;  coneFrom := C'  |})) ≈ f) by
+      (apply uniqueness; reflexivity).
+    rewrite <- A.
+    set (C'' := fmap[ConePresheaf F] g limit_acone).
+    apply uniqueness.
+    intro. simpl. symmetry. trivial.
+  Qed.
+  Check @equiv _ (homset _ _) _ _.
+  Check @IsALimit.
+  Check @homset.
+  Ltac apply_cone_equiv_to_morphism_equiv :=
+    match goal with
+    | [ H : @IsALimit _ _ _ ?b |- @equiv _ (@homset _ _ ?b) _ _ ] =>
+        simple eapply cone_equiv_to_morphism_equiv
+    end.
+
+  Hint Extern 2 => apply_cone_equiv_to_morphism_equiv : limit.
+  Theorem cone_coherence_auto1 (x y : J) (f : x ~> y) (w z : C) (g : w ~> z)
+    (A : ACone z F) :
+    fmap[F] f ∘ (vertex_map A x ∘ g) ≈ vertex_map A y ∘ g.
+  Proof.
+    now rewrite comp_assoc, cone_coherence.
+  Qed.
+
+  Hint Rewrite -> cone_coherence_auto1 : limit.
+  Hint Extern 20 => easy : core.
+
+  Hint Extern 10 => (autorewrite with limit) : limit.
+  
+  Proposition LimitIsUniversalProperty :
+    IsUniversalProperty C^op (fun c => IsALimit F c)
+                            (fun c => @LimitSetoid J C F c).
+  Proof.
+    exists (@ConePresheaf J C F); intro c.
+    repeat(unshelve econstructor; try intros); simpl in *.
+    - auto with cat limit.
+    - abstract(auto with cat limit).
+    - abstract(auto with cat). 
+    - abstract(auto with cat).
+    - abstract(auto with cat).
+    - auto with limit.
+    - abstract(intros f g a; apply uniqueness; auto with limit).
+    - abstract(auto with cat limit).
+    - abstract(auto with cat limit).
+    - abstract(auto with cat limit).
+    - abstract(auto with cat limit).
+    - abstract(auto with cat limit).
+    - intros x1 x2. apply_cone_equiv_to_morphism_equiv. intro.
+      autorewrite with limit.  rewrite <- X. now autorewrite with limit.
+    - destruct X; apply to; exact id.
+    - abstract(auto with cat limit).
+    - destruct N; now apply X.
+    - abstract(destruct X as [[X_to_transform X_to_nat ?]
+                       [X_from_transform X_from_nat ?] iso_to_from ?]; simpl in *;
+        rewrite X_to_nat; revert x;
+      change _ with (X_to_transform vertex_obj[N]
+                       (id{C} ∘ X_from_transform vertex_obj[N] coneFrom) ≈ (@coneFrom _ _ _ N));
+      rewrite (proper_morphism (X_to_transform vertex_obj[N])
+                   _ _(id_left (X_from_transform vertex_obj[N] coneFrom)));
+      intro j;
+               now rewrite (iso_to_from N (@coneFrom _ _ _ N) j), id_right).
+    - simpl in *. 
+      destruct X as [[X_to_transform X_to_nat ?]
+                       [X_from_transform X_from_nat ?] ? ?].
+      simpl in *.
+      set (k:= X_from_nat _ _ v (X_to_transform c id{C})).
+      symmetry in k; rewrite iso_from_to, 2 id_left in k.
+      rewrite <- k.
+      apply (proper_morphism (X_from_transform vertex_obj[N])).
+      simpl. intro j.
+      symmetry.
+      apply X0.
+    - simpl. intros a b eq.
+      destruct a, b as [to1 from1 tofrom1 fromto1]; destruct eq as [eql eqr]. simpl in *.
+      apply eql.
+    - simpl. intros a f.
+      intro j.
+      destruct x.
+      simpl.
+      destruct to.
+      simpl in *.
+      rewrite naturality.
+      revert j.
+      change _ with (transform a (id{C} ∘ f) ≈ transform a f).
+      now rewrite id_left. 
+    - simpl. intros. simpl.
+      Abort.
diff --git a/Structure/UniversalProperty/Limit.v b/Structure/UniversalProperty/Limit.v
new file mode 100644
index 00000000..c4916666
--- /dev/null
+++ b/Structure/UniversalProperty/Limit.v
@@ -0,0 +1,153 @@
+Require Import Category.Lib.
+Require Import Category.Lib.Tactics2.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Isomorphism.
+Require Import Category.Construction.Opposite.
+Require Import Category.Theory.Functor.
+Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Functor.Hom.
+Require Import Category.Instance.Sets.
+Require Import Category.Structure.UniversalProperty.
+Require Import Category.Structure.Cone.
+Require Import Category.Structure.Limit.
+Require Import Category.Functor.Hom.Yoneda.
+
+Section LimitUniversalProperty.
+  Context (J C : Category).
+  Context (F : J ⟶ C).
+
+  Definition ump_limit_construct (a z : C) (H : IsALimit F z) :
+      ACone a F -> a ~> z.
+  Proof.
+    destruct H.
+    intro m; specialize ump_limit with {| vertex_obj := a ; coneFrom := m |}.
+    destruct ump_limit as [unique_obj ? ?].
+    exact unique_obj.
+  Defined.
+
+  Proposition ump_limit_construct_proper (a z : C) (H : IsALimit F z) :
+    Proper (equiv ==> equiv) (ump_limit_construct a z H).
+  Proof.
+    repeat(intro).
+    unfold ump_limit_construct.
+    apply uniqueness. simpl.
+    intro j.
+    set (k := (unique_property (ump_limit {| vertex_obj := a ; coneFrom := y |}))).
+    destruct x, y; simpl in X.
+    simpl in *; rewrite X; apply k.
+  Qed.
+
+  Local Arguments vertex_map {J C c F}.
+  Proposition ump_limit_construct_recover (w z : C) (H : IsALimit F z) (m : obj[J])
+     (a : ACone w F) : vertex_map limit_acone m ∘ (ump_limit_construct w z _ a) ≈ vertex_map a m.
+  Proof.
+    unfold ump_limit_construct. simpl. 
+    exact (unique_property (ump_limit {| vertex_obj := w; coneFrom :=a |} ) _).
+  Qed.
+
+  Proposition ump_limit_construct_recover' (q w z : C) (H : IsALimit F z) (m : obj[J])
+    (a : ACone w F) (f : q ~> w) :
+    vertex_map limit_acone m ∘ (ump_limit_construct w z _ a ∘ f) ≈ vertex_map a m ∘ f.
+  Proof.
+    now rewrite comp_assoc, ump_limit_construct_recover.
+  Qed.
+  
+  Create HintDb limit discriminated.
+  Hint Resolve ump_limit_construct : limit.
+  Hint Resolve ump_limit_construct_proper : limit.
+  Hint Resolve vertex_map : limit.
+  Hint Resolve limit_acone : limit.
+  Hint Rewrite -> @cone_coherence : limit.
+  Hint Rewrite -> ump_limit_construct_recover : limit.
+  Hint Rewrite -> ump_limit_construct_recover' : limit.
+
+  Proposition cone_equiv_to_morphism_equiv (c z : C) (H : IsALimit F z) (f g : c ~> z) :
+    (forall a : J, vertex_map limit_acone a ∘ f ≈ vertex_map limit_acone a ∘ g) ->
+    f ≈ g.
+  Proof.
+    intro e.
+    set (C' := fmap[ConePresheaf F] f limit_acone).
+    assert (A: (unique_obj (ump_limit {| vertex_obj := c ;  coneFrom := C'  |})) ≈ f) by
+      (apply uniqueness; reflexivity).
+    rewrite <- A.
+    set (C'' := fmap[ConePresheaf F] g limit_acone).
+    apply uniqueness.
+    intro. simpl. symmetry. trivial.
+  Qed.
+
+  Ltac apply_cone_equiv_to_morphism_equiv :=
+    match goal with
+    | [ H : @IsALimit _ _ _ ?b |- @equiv _ (@homset _ _ ?b) _ _ ] =>
+        simple eapply cone_equiv_to_morphism_equiv
+    end.
+
+  Hint Extern 2 => apply_cone_equiv_to_morphism_equiv : limit.
+  Theorem cone_coherence_auto1 (x y : J) (f : x ~> y) (w z : C) (g : w ~> z)
+    (A : ACone z F) :
+    fmap[F] f ∘ (vertex_map A x ∘ g) ≈ vertex_map A y ∘ g.
+  Proof.
+    now rewrite comp_assoc, cone_coherence.
+  Qed.
+
+  Hint Rewrite -> cone_coherence_auto1 : limit.
+  Hint Extern 20 => easy : core.
+
+  Hint Extern 10 => (autorewrite with limit) : limit.
+  
+  Proposition LimitIsUniversalProperty :
+    IsUniversalProperty C^op (fun c => IsALimit F c)
+                            (fun c => @LimitSetoid J C F c).
+  Proof.
+    exists (@ConePresheaf J C F); intro c.
+    repeat(unshelve econstructor; try intros); simpl in *.
+    - auto with cat limit.
+    - abstract(auto with cat limit).
+    - abstract(auto with cat). 
+    - abstract(auto with cat).
+    - abstract(auto with cat).
+    - auto with limit.
+    - abstract(intros f g a; apply uniqueness; auto with limit).
+    - abstract(auto with cat limit).
+    - abstract(auto with cat limit).
+    - abstract(auto with cat limit).
+    - abstract(auto with cat limit).
+    - abstract(auto with cat limit).
+    - intros x1 x2. apply_cone_equiv_to_morphism_equiv. intro.
+      autorewrite with limit.  rewrite <- X. now autorewrite with limit.
+    - destruct X; apply to; exact id.
+    - abstract(auto with cat limit).
+    - destruct N; now apply X.
+    - abstract(destruct X as [[X_to_transform X_to_nat ?]
+                       [X_from_transform X_from_nat ?] iso_to_from ?]; simpl in *;
+        rewrite X_to_nat; revert x;
+      change _ with (X_to_transform vertex_obj[N]
+                       (id{C} ∘ X_from_transform vertex_obj[N] coneFrom) ≈ (@coneFrom _ _ _ N));
+      rewrite (proper_morphism (X_to_transform vertex_obj[N])
+                   _ _(id_left (X_from_transform vertex_obj[N] coneFrom)));
+      intro j;
+               now rewrite (iso_to_from N (@coneFrom _ _ _ N) j), id_right).
+    - abstract(destruct X as [[X_to_transform X_to_nat ?]
+                       [X_from_transform X_from_nat ?] ? ?];
+                simpl in *;
+               set (k:= X_from_nat _ _ v (X_to_transform c id{C}));
+               symmetry in k; rewrite iso_from_to, 2 id_left in k;
+               rewrite <- k;
+               apply (proper_morphism (X_from_transform vertex_obj[N]));
+               simpl; intro j; symmetry; apply X0).
+    - abstract(simpl; intros a b eq;
+               destruct a, b as [to1 from1 tofrom1 fromto1];
+               destruct eq as [eql eqr]; simpl in *;
+               apply eql).
+    - abstract(intros a f j; destruct x, to; simpl in *;
+      rewrite naturality; revert j;
+      change _ with (transform a (id{C} ∘ f) ≈ transform a f);
+      now rewrite id_left). 
+    - abstract(now unfold  ump_limit_construct).
+    - abstract(auto with cat limit).
+  Defined.
+
+End LimitUniversalProperty.
+      
+      
+      
+      
diff --git a/Structure/UniversalProperty/Limit.v~ b/Structure/UniversalProperty/Limit.v~
new file mode 100644
index 00000000..9dd1fe55
--- /dev/null
+++ b/Structure/UniversalProperty/Limit.v~
@@ -0,0 +1,196 @@
+Require Import Category.Lib.
+Require Import Category.Lib.Tactics2.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Isomorphism.
+Require Import Category.Construction.Opposite.
+Require Import Category.Theory.Functor.
+Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Functor.Hom.
+Require Import Category.Instance.Sets.
+Require Import Category.Structure.UniversalProperty.
+Require Import Category.Structure.Cone.
+Require Import Category.Structure.Limit.
+Require Import Category.Functor.Hom.Yoneda.
+
+Section LimitUniversalProperty.
+  Context (J C : Category).
+  Context (F : J ⟶ C).
+
+  Definition ump_limit_construct (a z : C) (H : IsALimit F z) :
+      ACone a F -> a ~> z.
+  Proof.
+    destruct H.
+    intro m; specialize ump_limit with {| vertex_obj := a ; coneFrom := m |}.
+    destruct ump_limit as [unique_obj ? ?].
+    exact unique_obj.
+  Defined.
+
+  Proposition ump_limit_construct_proper (a z : C) (H : IsALimit F z) :
+    Proper (equiv ==> equiv) (ump_limit_construct a z H).
+  Proof.
+    repeat(intro).
+    unfold ump_limit_construct.
+    apply uniqueness. simpl.
+    intro j.
+    set (k := (unique_property (ump_limit {| vertex_obj := a ; coneFrom := y |}))).
+    destruct x, y; simpl in X.
+    simpl in *; rewrite X; apply k.
+  Qed.
+
+  Local Arguments vertex_map {J C c F}.
+  Proposition ump_limit_construct_recover (w z : C) (H : IsALimit F z) (m : obj[J])
+     (a : ACone w F) : vertex_map limit_acone m ∘ (ump_limit_construct w z _ a) ≈ vertex_map a m.
+  Proof.
+    unfold ump_limit_construct. simpl. 
+    exact (unique_property (ump_limit {| vertex_obj := w; coneFrom :=a |} ) _).
+  Qed.
+
+  Create HintDb limit discriminated.
+  Hint Resolve ump_limit_construct : limit.
+  Hint Resolve ump_limit_construct_proper : limit.
+
+  Set Warnings "-non-reversible-notation".
+  Notation next_field X
+    := ltac:(let c := type of X in match c with forall _ : ?A, _  => exact A end).
+  Set Warnings "non-reversible-notation".
+  
+  Let limit_is_univ_property :=
+        Build_IsUniversalProperty C^op
+         (fun c => IsALimit F c)
+         (fun c => @LimitSetoid J C F c)
+         (@ConePresheaf J C F).
+  Section allC.
+    Context (z : C).
+    Let master_iso := Eval hnf in ltac:(
+                      (let A := (eval hnf in (next_field limit_is_univ_property)) in
+                       match A with
+                       | forall a : _, @?B a => exact(B z)
+                       end)).
+    (* master_iso := IsALimit F z ≊ fobj[C^op] z ≅ ConePresheaf F *)
+
+    Let Build_Iso := Eval hnf in ltac:(let A := (eval hnf in master_iso) in
+                           match A with
+                           | @Isomorphism ?a ?b ?c => exact(@Build_Isomorphism a b c)
+                           end).
+    Let master_iso_to := next_field Build_Iso.
+
+    Let Build_to := Eval hnf in ltac:(let A := (eval hnf in master_iso_to) in
+                           match A with
+                           | @SetoidMorphism ?x ?sx ?y ?sy =>
+                               exact(@Build_SetoidMorphism x sx y sy)
+                           end).
+    Let master_iso_to_underlying := next_field Build_to.
+    
+    Local Arguments vertex_map {J C c F}.
+    Proposition limit_to_representable : master_iso_to_underlying.
+    Proof using Type.
+      unfold master_iso_to_underlying; clear master_iso_to_underlying.
+      clear Build_to master_iso_to master_iso Build_Iso limit_is_univ_property.
+      simpl. intro A.
+      unshelve econstructor.
+      - apply (from (Yoneda_Lemma C (ConePresheaf F) z)).
+        exact limit_acone. 
+      - simpl. unshelve eapply Build_Transform'.
+        + simpl; intro c; unshelve econstructor.
+          * auto with limit.
+          * abstract(auto with limit).
+        + abstract(simpl; intros c' c f L;
+          symmetry; apply uniqueness;
+          intro m; simpl;
+            now rewrite comp_assoc, ump_limit_construct_recover).
+      - abstract(simpl; intros a L j; rewrite id_right; apply ump_limit_construct_recover).
+      - abstract(intros a f; simpl; rewrite id_right; now apply uniqueness).
+    Defined.
+          
+    Proposition limit_to_representable_proper :
+      Proper (equiv ==> equiv) limit_to_representable.
+    Proof using Type.
+      unfold limit_to_representable.
+      unfold master_iso_to_underlying; clear master_iso_to_underlying.
+      clear Build_to master_iso_to master_iso Build_Iso limit_is_univ_property.
+      intros l1 l2 eq; apply to_equiv_implies_iso_equiv; simpl.
+      intros c f j.
+      apply compose_respects; auto.
+    Qed.
+
+    Let master_iso_from :=
+          next_field (Build_Iso (Build_to limit_to_representable limit_to_representable_proper)).
+    Let Build_from := Eval hnf in ltac:(let A := (eval hnf in master_iso_from) in
+                           match A with
+                           | @SetoidMorphism ?x ?sx ?y ?sy =>
+                               exact(@Build_SetoidMorphism x sx y sy)
+                           end).
+    Proposition from : next_field Build_from.
+    Proof using Type.
+      clear Build_from
+        master_iso_from
+        master_iso_to_underlying
+        Build_to
+        master_iso_to
+        Build_Iso
+        master_iso
+        limit_is_univ_property.
+      simpl; intro; simpl.
+      apply (from (representability_by_yoneda _ _ _)) in X.
+      destruct X as [x i]; exists x.
+      intros [Nvertex ConeOfN]; destruct i as [inv tofrom_id fromto_id].
+      exists (inv Nvertex ConeOfN).
+      + abstract(simpl; intro; simpl in tofrom_id; now rewrite tofrom_id, id_right).
+      + abstract(simpl; intros;
+        simpl in fromto_id; specialize fromto_id with Nvertex v; simpl in fromto_id;
+        rewrite id_right in fromto_id;
+        rewrite <- fromto_id;
+        apply (proper_morphism (inv Nvertex));
+        simpl; intro j; simpl in x; symmetry; exact (X j)).
+    Defined.
+
+    Proposition from_proper : Proper (equiv ==> equiv) from.
+    Proof using Type.
+      unfold from.
+      clear Build_from
+        master_iso_from
+        master_iso_to_underlying
+        Build_to
+        master_iso_to
+        Build_Iso
+        master_iso
+        limit_is_univ_property.
+      simpl. intros a b eq j.
+      simpl. destruct eq as [e _]. simpl in e. now rewrite e.
+    Qed.
+
+    Proposition tofrom_id : next_field (Build_Iso
+                               (Build_to limit_to_representable limit_to_representable_proper)
+                               (Build_from from from_proper)).
+    Proof using Type.
+      simpl; intro x; apply to_equiv_implies_iso_equiv. simpl.
+      clear Build_from
+        master_iso_from
+        master_iso_to_underlying
+        Build_to
+        master_iso_to
+        Build_Iso
+        master_iso
+        limit_is_univ_property.
+      intros a b j.
+      destruct x as [xto from ? ?]; simpl.
+      assert (k:= UniversalProperty.preyoneda xto b).
+      symmetry; simpl in k; apply k.
+    Qed.
+
+    Proposition fromto_id : next_field (Build_Iso
+                               (Build_to limit_to_representable limit_to_representable_proper)
+                               (Build_from from from_proper)
+                               tofrom_id).
+    Proof using Type.
+      simpl; intros a j; now rewrite id_right.
+    Qed.
+
+    Definition allC := Eval hnf in (Build_Iso
+                               (Build_to limit_to_representable limit_to_representable_proper)
+                               (Build_from from from_proper)
+                               tofrom_id fromto_id).
+  End allC.
+  Definition LimitIsUniversalProperty := Eval hnf in limit_is_univ_property allC.
+End LimitUniversalProperty.
+
diff --git a/Structure/UniversalProperty/Universal/Arrow.v b/Structure/UniversalProperty/Universal/Arrow.v
new file mode 100644
index 00000000..788d8c5b
--- /dev/null
+++ b/Structure/UniversalProperty/Universal/Arrow.v
@@ -0,0 +1,78 @@
+Require Import Category.Lib.
+Require Import Category.Lib.Tactics2.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Isomorphism.
+Require Import Category.Construction.Opposite.
+Require Import Category.Theory.Functor.
+Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Functor.Hom.
+Require Import Category.Instance.Sets.
+Require Import Category.Structure.UniversalProperty.
+Require Import Category.Theory.Universal.Arrow.
+
+Section UniversalArrowUniversalProperty.
+  Context (C D: Category).
+  Context (U : D ⟶ C).
+  Context (c : C).
+
+  Hint Resolve fmap : cat.
+
+  Proposition fmap_respects' (x y : D) (f g : x ~> y) :
+    f ≈ g -> fmap[U] f ≈ fmap[U] g.
+  Proof using Type.
+    apply fmap_respects.
+  Qed.
+                             
+  Hint Resolve fmap_respects' : cat.
+  Hint Rewrite @fmap_comp : categories.
+  Hint Resolve uniqueness : cat.
+  
+  Proposition UniversalArrowIsUniversalProperty :
+    IsUniversalProperty D (fun a : D => AUniversalArrow c U a) _.
+  Proof.
+    exists ((Curried_Hom C c) ◯ U).
+    intro a.
+    repeat(unshelve econstructor; try intro).
+    - simpl in *. destruct X. auto with cat.
+    - abstract(auto with cat).
+    - abstract(auto with cat).
+    - abstract(auto with cat).
+    - simpl in *. destruct X. now apply universal_arrow_universal. 
+    - abstract(simpl; intros; apply uniqueness;
+      rewrite (unique_property universal_arrow_universal); easy).
+    - abstract(simpl; intros; symmetry; apply uniqueness;
+      autorewrite with categories;
+               now rewrite (unique_property universal_arrow_universal)).
+    - abstract(simpl; intros; destruct X; simpl; apply uniqueness;
+      autorewrite with categories; apply compose_respects; [ reflexivity |];
+               apply (unique_property (universal_arrow_universal _ _))).
+    - abstract(simpl; intros; rewrite (unique_property universal_arrow_universal);
+               auto with cat).
+    - abstract(auto with cat).
+    - abstract(auto with cat).
+    - abstract(simpl; intros; apply uniqueness;
+      simpl in X;
+               now rewrite X, (unique_property (universal_arrow_universal ))).
+    - exact (((to X) a) id).
+    - now apply (from X d).
+    - abstract(simpl; set (M := @preyoneda D^op _ d _ (to X));
+      simpl in M; rewrite <- M; clear M;
+      assert (K := (@iso_to_from _ _ _ X)); simpl in K; rewrite K;
+               now autorewrite with categories).
+    - (* This proof is only valid for Coq versions >= 8.16 
+         because setoid rewriting supports polymorphism better *)
+      try(
+      simpl; assert (M := @preyoneda D^op _ d _ (to X));
+      simpl in M; intro A; rewrite <- M in A; clear M;
+      apply (proper_morphism (from X d)) in A;
+      set (B := (iso_from_to X)); simpl in B; now rewrite B , id_left in A); admit.
+    - abstract(simpl; intros; destruct X as [e ?]; simpl in e; apply e).
+    - abstract(simpl; intro; assert (M := @preyoneda D^op _ x0 _ (to x));
+               simpl in M; now rewrite <- M).
+    - abstract (auto with cat).
+    - abstract(auto with cat).
+  Defined.
+
+End UniversalArrowUniversalProperty.
+      
+      
diff --git a/Theory/Adjunction.v b/Theory/Adjunction.v
index b8616d65..fd5275da 100644
--- a/Theory/Adjunction.v
+++ b/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).
diff --git a/Theory/Functor.v b/Theory/Functor.v
index e5fb99a6..fa85500c 100644
--- a/Theory/Functor.v
+++ b/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.
+
diff --git a/Theory/Isomorphism.v b/Theory/Isomorphism.v
index 9ab1d502..5cb5fcf1 100644
--- a/Theory/Isomorphism.v
+++ b/Theory/Isomorphism.v
@@ -35,6 +35,21 @@ Arguments iso_from_to {x y} _.
 
 Infix "≅" := Isomorphism (at level 91) : category_scope.
 
+Class IsIsomorphism {x y : C} (f : x ~> y) := {
+    two_sided_inverse : y ~> x;
+    is_right_inverse : f ∘ two_sided_inverse ≈ id;
+    is_left_inverse : two_sided_inverse ∘ f ≈ id                        
+  }.
+
+#[export]
+Instance IsIsoToIso {x y : C} (f : x ~> y) ( _ : IsIsomorphism f) : Isomorphism x y :=
+  {|
+    to := f;
+    from := two_sided_inverse;
+    iso_to_from := is_right_inverse;
+    iso_from_to := is_left_inverse
+  |}.
+
 #[export] Program Instance iso_id {x : C} : x ≅ x := {
   to   := id;
   from := id
@@ -94,7 +109,7 @@ Qed.
 #[export] Instance iso_setoid {x y : C} : Setoid (x ≅ y) := {
   equiv := iso_equiv;
   setoid_equiv := iso_equiv_equivalence
-}.
+  }.
 
 #[local] Obligation Tactic := program_simpl.
 
@@ -114,8 +129,9 @@ Proof.
   intros.
   (* jww (2021-08-09): It should be possible to rewrite here with isomorphism
      acting similarly to an equivalence. *)
-(*   rewrite g. *)
-Abort.
+  rewrite g.
+  exact f.
+Qed.
 
 End Isomorphism.
 
@@ -175,6 +191,64 @@ Next Obligation.
   rewrites; reflexivity.
 Qed.
 
+Proposition to_equiv_implies_iso_equiv {C : Category} {x y} (f g : x ≅ y) :
+  to f ≈ to g -> f ≈ g.
+Proof.
+  intro eq. split; [ assumption | ].
+  assert (m := iso_to_epic f).
+  destruct f as [tof fromf tofrom_eqf fromto_eqf], 
+      g as [tog fromg tofrom_eqg fromto_eqg].
+  simpl in *.
+  destruct m as [epic]. apply epic.
+  rewrite fromto_eqf, eq, fromto_eqg; reflexivity.
+Qed.
+
+#[export]
+Instance iso_sym_proper {C: Category} {x y : C} : Proper (equiv ==> equiv) (@iso_sym C x y).
+Proof.
+  intros f g [fg_toeq fg_fromeq]; destruct f as [ffrom fto ? ?], g as [gfrom gto ? ?];
+    simpl in *.
+  unfold iso_equiv; split; assumption.
+Qed.
+
+#[export]
+Instance iso_compose_proper {C : Category} {x y z : C} :
+  Proper ((@iso_equiv C y z) ==> @iso_equiv C x y ==> (@iso_equiv C x z)) iso_compose.
+Proof.
+  intros f1 f2 eqf g1 g2 eqg.
+  apply to_equiv_implies_iso_equiv.
+  destruct f1 as [f1to ? ? ?], f2 as [f2to ? ? ?], eqf as [eqfto _], eqg as [eqgto _].
+  simpl in *.
+  rewrite eqfto, eqgto.
+  reflexivity.
+Qed.
+
+Proposition iso_sym_left_inverse {C : Category} {x y : C} (f : x ≅ y) :
+  iso_compose (iso_sym f) f ≈ iso_id.
+Proof.
+  apply to_equiv_implies_iso_equiv, iso_from_to.
+Qed.
+
+Proposition iso_sym_right_inverse {C : Category} {x y : C} (f : x ≅ y) :
+  iso_compose f (iso_sym f) ≈ iso_id.
+Proof.
+  apply to_equiv_implies_iso_equiv, iso_to_from.
+Qed.
+
+Proposition from_equiv_implies_iso_equiv {C : Category} {x y} (f g : x ≅ y) :
+  from f ≈ from g -> f ≈ g.
+Proof.
+  set (f1 := iso_sym f).
+  set (g1 := iso_sym g).
+  change f with (iso_sym (iso_sym f)).
+  change g with (iso_sym (iso_sym g)).
+  change (iso_sym f) with f1.
+  change (iso_sym g) with g1.
+  clearbody f1 g1. clear f g.
+  simpl. intro eq; apply to_equiv_implies_iso_equiv in eq.
+  now apply iso_sym_proper.
+Qed.
+
 #[export]
 Program Instance iso_from_epic {C : Category} {x y} (iso : @Isomorphism C x y) :
   Epic (iso⁻¹).
diff --git a/Theory/Metacategory/ArrowsOnly.v b/Theory/Metacategory/ArrowsOnly.v
index 727b2e3d..5abe3c3e 100644
--- a/Theory/Metacategory/ArrowsOnly.v
+++ b/Theory/Metacategory/ArrowsOnly.v
@@ -48,13 +48,13 @@ Section Category.
 
 Context (M : Metacategory).
 
-Record object := {
+Record object : Set := {
   obj_arr : arrow M;
   obj_def : composite M obj_arr obj_arr obj_arr;
   obj_id  : is_identity M obj_arr
 }.
 
-Record morphism (dom cod : object) := {
+Record morphism (dom cod : object) : Set := {
   mor_arr : arrow M;
   mor_dom : composite M mor_arr (obj_arr dom) mor_arr;
   mor_cod : composite M (obj_arr cod) mor_arr mor_arr
diff --git a/Theory/Natural/Transformation.v b/Theory/Natural/Transformation.v
index 01d0a92f..a0edb7ff 100644
--- a/Theory/Natural/Transformation.v
+++ b/Theory/Natural/Transformation.v
@@ -24,8 +24,17 @@ Class Transform := {
 
   naturality_sym {x y} (f : x ~> y) :
     transform ∘ fmap[F] f ≈ fmap[G] f ∘ transform
-}.
-
+  }.
+
+Definition Build_Transform'
+  (transform' : forall x, F x ~> G x)
+  (natural : forall x y (f : x ~> y), fmap[G] f ∘ transform' x ≈ transform' y ∘ fmap[F] f)
+  :  Transform.
+Proof.
+  apply (Build_Transform transform' natural).
+  intros x y f; symmetry; apply natural.
+Defined.
+  
 #[export]
 Program Instance Transform_Setoid : Setoid Transform :=
   {| equiv N0 N1 := ∀ x, (@transform N0 x) ≈ (@transform N1 x); |}.
diff --git a/Theory/Universal/Arrow.v b/Theory/Universal/Arrow.v
index 290984a0..f1444f55 100644
--- a/Theory/Universal/Arrow.v
+++ b/Theory/Universal/Arrow.v
@@ -1,9 +1,12 @@
 Require Import Category.Lib.
 Require Import Category.Theory.Category.
 Require Import Category.Theory.Functor.
+Require Import Category.Theory.Adjunction.
 Require Import Category.Structure.Initial.
+Require Import Category.Theory.Isomorphism.
 Require Import Category.Construction.Comma.
 Require Import Category.Functor.Diagonal.
+Require Import Category.Instance.Sets.
 
 Generalizable All Variables.
 
@@ -40,4 +43,85 @@ Proof.
                              ((ttt, h1); e) ((ttt, v); X))).
 Qed.
 
+Definition universal_arrow_from_UMP (c : C) (F : D ⟶ C) (d : D) (η : c ~> fobj[F] d)
+  (u : ∀ (d' : D) (f : c ~> fobj[F] d'), ∃! g : d ~> d', f ≈ fmap[F] g ∘ η)
+  : UniversalArrow c F.
+Proof.
+  unshelve eapply Build_UniversalArrow. simpl. unshelve esplit.
+  - simpl. unshelve esplit; [ split; [ exact ttt | exact d ] | exact η ].
+  - simpl. intros [ [unit d'] f]; simpl in *.
+    unshelve esplit; [ split ; [ exact ttt | exact (unique_obj (u d' f))] | ].
+    rewrite id_right; simpl. exact (unique_property (u d' f)).
+  - simpl. intros [[unit d']  f]; simpl in *.
+    intros [[unit2 g] g_eq]. simpl in g_eq.
+    intros [[unit3 h] h_eq]. split.
+    + simpl. destruct unit2, unit3; reflexivity.
+    + simpl. rewrite id_right in g_eq, h_eq. simpl in h_eq.
+      rewrite <- (uniqueness (u d' f) _ g_eq).
+      exact (uniqueness (u d' f) _ h_eq).
+Defined.
+
+Context (U : @Functor D C).
+
+Arguments arrow : clear implicits.
+Arguments arrow_obj : clear implicits.
+Definition LeftAdjointFunctorFromUniversalArrows (H : forall c : C, UniversalArrow c U) 
+  : @Functor C D.
+Proof.
+  refine
+    ({|
+        fobj := (fun c => arrow_obj _ _ (H c));
+        fmap := (fun x y f => unique_obj (ump_universal_arrows (H x)
+                                            ((arrow _ _ (H y) ∘ f))))
+                  
+      |}).
+  - abstract(intros x y f g f_eq_g;
+             apply uniqueness;
+             rewrite <- (unique_property
+                  (ump_universal_arrows (H x) (arrow y U (H y) ∘ g)));
+             now rewrite f_eq_g).
+  - abstract(intros ?; apply uniqueness; cat_simpl).
+  - abstract(intros c1 c2 c3 g f; apply uniqueness;
+      rewrite fmap_comp,
+      <- comp_assoc,
+      <- (unique_property (ump_universal_arrows (H c1) _)),
+      2! comp_assoc;
+      exact (compose_respects _ _
+             (unique_property (ump_universal_arrows (H c2) _))
+             f f (Equivalence_Reflexive _))).
+Defined.
+
+Definition AdjunctionFromUniversalArrows (H: forall c : C, UniversalArrow c U) :
+  @Adjunction _ _ (LeftAdjointFunctorFromUniversalArrows H) U.
+Proof.
+  unshelve eapply Build_Adjunction'.
+  + intros c d; unshelve eapply Isomorphism.Build_Isomorphism.
+  - unshelve eapply Sets.Build_SetoidMorphism.
+    * exact (fun g => (fmap[U] g) ∘ (arrow _ _ (H c))).
+    * abstract(intros ? ? g1_eq_g2; rewrite g1_eq_g2; reflexivity).
+  - unshelve eapply Sets.Build_SetoidMorphism.
+    * exact(fun f => unique_obj (ump_universal_arrows (H c) f)).
+    * abstract(intros f1 f2 f1_eq_f2; apply uniqueness; rewrite f1_eq_f2;
+               apply (unique_property (ump_universal_arrows (H c) f2))).
+  - abstract(intro f; symmetry; exact (unique_property (ump_universal_arrows (H c) f))).
+  - abstract(simpl; intro g; apply uniqueness; reflexivity).
+  + abstract(intros c1 c2 d f g;
+             simpl; rewrite fmap_comp, <- 2! comp_assoc;
+             apply (compose_respects (fmap[U] f) _ (Equivalence_Reflexive _) _ _);
+             symmetry;
+             apply (unique_property (ump_universal_arrows (H c1) _))).
+  + abstract(intros ? ? ? ? ?; simpl; rewrite fmap_comp, <- comp_assoc; reflexivity).
+Defined.
+
+
+Class AUniversalArrow (c : C) (F : D ⟶ C) (a : D) := {
+    universal_arrow : c ~> fobj[F] a ;
+    universal_arrow_universal {d} {f : c ~> (fobj[F] d)} :
+    Unique (fun g : hom a d => fmap[F] g ∘ universal_arrow ≈ f)
+  }.
+
+#[export] Program Instance AUniversalArrowEquiv (c : C) (F : D ⟶ C) (a : D) :
+  Setoid (AUniversalArrow c F a) :=
+  {| equiv := fun X Y => (@universal_arrow _ _ _ X) ≈ (@universal_arrow _ _ _ Y) |}.
+
 End UniversalArrow.
diff --git a/_CoqProject b/_CoqProject
index 0b38dda8..28c7ca75 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -21,6 +21,7 @@ Construction/Product/Comma.v
 Construction/Slice.v
 Construction/Slice/Pullback.v
 Construction/Subcategory.v
+Construction/Free/Quiver.v
 Functor/Applicative.v
 Functor/Bifunctor.v
 Functor/Construction/Product.v
@@ -54,6 +55,7 @@ Instance/Cat.v
 Instance/Cat/Cartesian.v
 Instance/Cat/Cartesian/Closed.v
 Instance/Cat/Cocartesian.v
+Instance/StrictCat.v
 Instance/Comp.v
 Instance/Cones.v
 Instance/Cones/Comma.v
@@ -66,6 +68,7 @@ Instance/Coq/ParE.v
 Instance/Ens.v
 Instance/Fact.v
 Instance/Fun.v
+Instance/Fun/Cartesian.v
 Instance/Lambda.v
 Instance/Lambda/Eval.v
 Instance/Lambda/Example.v
@@ -109,6 +112,7 @@ Lib/NETList.v
 Lib/Setoid.v
 Lib/TList.v
 Lib/Tactics.v
+Lib/Tactics2.v
 Monad/Adjunction.v
 Monad/Algebra.v
 Monad/Compose.v
@@ -177,6 +181,10 @@ Structure/Pullback.v
 Structure/Pullback/Limit.v
 Structure/Span.v
 Structure/Terminal.v
+Structure/UniversalProperty.v
+Structure/UniversalProperty/Cartesian.v
+Structure/UniversalProperty/Limit.v
+Structure/UniversalProperty/Universal/Arrow.v
 Structure/Wedge.v
 Theory.v
 Theory/Adjunction.v