The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Did you mean to write the equation the other way?  You always have x = y -> (X, x) = (X, y) (by f_equal), but the reverse isn't always true.

-Jason

On Jan 20, 2014 10:37 AM, "Arnaud Spiwack" <aspiwack AT lix.polytechnique.fr> wrote:

Dear Daniel,

A small technical note considering your first proposal. Unless I'm mistaken the statement

forall x y:X, x=y -> (X,x) = (X,y)

Is true if and only if X is a set (in the hott sense). You would lose equalities between objects in the case X is a category and x, y objects in X.


Best regards,

Arnaud

On 19 January 2014 21:08, Daniel R. Grayson <drg AT illinois.edu> wrote:

Thanks!  The following code is perhaps simpler and does the same thing (recall

C and C' are two categories sharing the same objects.)

Record Obj (C:precategory) := enclose { release : ob C }.

Arguments release {C} o.

Definition iso' {C:precategory} (c c':Obj C) := @iso C (release c) (release c').

Definition funny'   (c:ob  C) (c':ob  C') := iso c c'. (* succeeds, but confusing *)

Definition funny''  (c:Obj C) (c':Obj C ) := iso' c c.

(*

Definition funny''' (c:Obj C) (c':Obj C') := iso' c c'. (* doesn't succeed, good *)

*)

And then since it's a primitive record definition, once we have eta for primitive

records, things will be even better.

On Sun, Jan 19, 2014 at 1:20 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

On Sunday, January 19, 2014 12:27:06 PM Daniel R. Grayson wrote:
> Good points, all.
>
> Actually, Bas, I'm not sure 1*2 is a good example of what I wanted to
> disallow.  A good example
> would be a category C and its opposite C^op, which have the same objects.
>  But after the
> discussion it seems it's better to write Hom_C(c,c') or Hom_(C^op)(c,c'),
> rather than to
> write Hom(c,c'), in which C is filled in automatically.  As Vladimir says,
> implicit parameters should
> be uniquely determined.
>
> On the other hand, obeying that would mean jettisoning the standard
> mathematical notation
> f : c --> c' for declaring f to be a morphism from c to c', because there C
> is filled in automatically.
> Hmm.

Another way to do this would be something like:

Inductive OpCat (C:Type) : Type :=
| OpObj : C -> OpCat C.

(* Define Hom on OpCat. *)
Inductive OpHom (Homs:Type) : Type :=
| RevHom : Homs -> OpHom Homs.

Instance OpArrows (C:Type) `{!Arrows C} : Arrows (OpCat C) :=
fun Xop => let '(OpObj X) := Xop in
fun Yop => let '(OpObj Y) := Yop in
OpHom (Hom Y X).

Instance OpComp (C:Type) `{!Arrows C} `{!Composition C} :
  Composition (OpCat C).
(* I wanted to do :=
fun Xop => let '(OpObj X) := Xop in
fun Yop => let '(OpObj Y) := Yop in
fun Zop => let '(OpObj Z) := Zop in
fun fop => let '(RevHom f) := fop in
fun gop => let '(RevHom g) := gop in
RevHom (Hom X Y)
but ran into issues with specifying the return types; so this was the easiest
way I found to do the definition... *)
intros [X] [Y] [Z] [f] [g].
exact (RevHom _ (comp g f)).
Defined.

etc.

So then OpCat C is canonically isomorphic as a type to C, and likewise Hom
(OpObj X) (OpObj Y) is canonically isomorphic as a type to Hom Y X; but Coq
can't automatically determine that.  It does have the issue that it requires a
bit more notation than is conventional.  But on further reflection, I'm not
convinced that would actually be a disadvantage: in fact, I've often found the
additional annotation to be useful in making things clearer.  (The primary
example I'm thinking of here is the Kleisli category of a monad: it makes
things easier to keep track of, at least for me, if I write
Ob(C^T) := a copy of Ob(C) by a map ^*
Hom(X^*, Y^*) := a copy of Hom(X, TY) by a map ^*
comp(f^*, g^*) := (comp(mu, Tf, g))^*
id(X^*) := (eta_X)^*
rather than
Hom_{C^T}(X, Y) := Hom_C(X, TY)
comp_{C^T}(f, g) := comp_C(mu, Tf, g)
id_{C^T}(X) := eta_X.)
--
Daniel Schepler