Cone redefinition - Githubissues

The current definition of a cone is

Class Cone `(F : J ⟶ C) := {
  vertex_obj : C;
  vertex_map {x : J} : vertex_obj ~{C}~> F x;
  ump_cones {x y : J} (f : x ~{J}~> y) :
    fmap[F] f ∘ @vertex_map x ≈ @vertex_map y
}.

and, if N is an object in C, a cone from N to F is defined as

Notation "Cone[ N ] F" := { ψ : Cone F | vertex_obj[ψ] = N }

There are well-known headaches in dependent type theory that arise from using equations to constrain the values of fields of a record. We can eliminate this by reversing the order in which Cone[N] F and Cone F are defined, i.e.,

Class ConeFrom `(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
  }.
Class Cone `(F : J ⟶ C) := {
  vertex_obj : C;
  coneFrom : ConeFrom vertex_obj F
}.

The field ump_cones has been renamed cone_coherence. The given equation is not generally considered a universal mapping property, and the name ump_cones may lead to confusion. (ump_limit, on the other hand, is well named. )

We also define an equivalence relation on cones from c to F, saying that two cones are equivalent if all their morphisms are pairwise equivalent.

For fixed F : J -> C we define the presheaf ConePresheaf : C^op -> Sets of cones over F. If f : c -> c' is a morphism in C, then a cone from c' to F can be precomposed with f to yield a new cone c -> F, so ConeFrom c F is a contravariant functor of the argument c.

All other changes are repairing things that break as a result of redefining Cone in terms of ConeFrom.

jwiegley / category-theory

Cone redefinition #116