feat(colimits): arbitrary colimits in Mon and CommRing (#910)

* feat(category_theory): working in Sort rather than Type, as far as possible

* missed one

* adding a comment about working in Type

* remove imax

* removing `props`, it's covered by `types`.

* fixing comment on `rel`

* tweak comment

* add matching extend_π lemma

* remove unnecessary universe annotation

* another missing s/Type/Sort/

* feat(category_theory/shapes): basic shapes of cones and conversions

minor tweaks

* Moving into src. Everything is borked.

* investigating sparse

* blech

* maybe working again?

* removing terrible square/cosquare names

* returning to filtered colimits

* colimits in Mon

* rename

* actually jump through the final hoop

* experiments

* fixing use of ext

* feat(colimits): colimits in Mon and CommRing

* fixes

* removing stuff I didn't mean to have in here

* minor

* fixes

* merge

* update after merge

* fix import

src/category_theory/concrete_category.lean

@@ -66,8 +66,11 @@ instance : has_coe_to_fun (X ⟶ Y) :=
 { F   := λ f, X → Y,
   coe := λ f, f.1 }
 
+@[extensionality] lemma bundled_hom.ext  {f g : X ⟶ Y} : (∀ x : X, f x = g x) → f = g :=
+λ w, subtype.ext.2 $ funext w
+
 @[simp] lemma coe_id {X : bundled c} : ((𝟙 X) : X → X) = id := rfl
-@[simp] lemma bundled_hom_coe {X Y : bundled c} (val : X → Y) (prop) (x : X) :
+@[simp] lemma bundled_hom_coe (val : X → Y) (prop) (x : X) :
   (⟨val, prop⟩ : X ⟶ Y) x = val x := rfl
 
 end concrete_category

src/category_theory/instances/CommRing/adjunctions.lean

@@ -35,6 +35,10 @@ noncomputable def polynomial_ring : Type u ⥤ CommRing.{u} :=
 @[simp] lemma polynomial_ring_map_val {α β : Type u} {f : α → β} :
   (polynomial_ring.map f).val = eval₂ C (X ∘ f) := rfl
 
+lemma hom_coe_app' {R S : CommRing} (f : R ⟶ S) (r : R) : f r = f.val r := rfl
+-- this is usually a bad idea, as it forgets that `f` is ring homomorphism
+local attribute [simp] hom_coe_app'
+
 noncomputable def adj : adjunction polynomial_ring (forget : CommRing ⥤ Type u) :=
 adjunction.mk_of_hom_equiv _ _
 { hom_equiv := λ α R,
@@ -47,7 +51,7 @@ adjunction.mk_of_hom_equiv _ _
       have H2 := λ p₁ p₂, (@is_ring_hom.map_mul _ _ _ _ f.val f.2 p₁ p₂).symm,
       apply mv_polynomial.induction_on p; intros;
       simp only [*, eval₂_add, eval₂_mul, eval₂_C, eval₂_X,
-        eq_self_iff_true, function.comp_app, hom_coe_app] at *
+        eq_self_iff_true, function.comp_app, hom_coe_app'] at *
     end,
     right_inv := by tidy },
   hom_equiv_naturality_left_symm' := λ X' X Y f g, subtype.ext.mpr $ funext $ λ p,

src/category_theory/instances/CommRing/basic.lean

@@ -5,7 +5,8 @@ Authors: Scott Morrison, Johannes Hölzl
 Introduce CommRing -- the category of commutative rings.
 -/
 
-import category_theory.instances.monoids
+import category_theory.instances.Mon.basic
+import category_theory.fully_faithful
 import algebra.ring
 import data.int.basic
 
@@ -49,7 +50,10 @@ instance hom_coe : has_coe_to_fun (R ⟶ S) :=
 { F := λ f, R → S,
   coe := λ f, f.1 }
 
-@[simp] lemma hom_coe_app (f : R ⟶ S) (r : R) : f r = f.val r := rfl
+@[extensionality] lemma hom.ext  {f g : R ⟶ S} : (∀ x : R, f x = g x) → f = g :=
+λ w, subtype.ext.2 $ funext w
+
+@[simp] lemma hom_coe_app (val : R → S) (prop) (r : R) : (⟨val, prop⟩ : R ⟶ S) r = val r := rfl
 
 instance hom_is_ring_hom (f : R ⟶ S) : is_ring_hom (f : R → S) := f.2