The Coq mailing list

[Polina Vinogradova <polina.vino AT gmail.com>]

Thank you so much! This helps a lot. I was hoping to avoid building additional structures but i think you are right, this is the way to go.

Polina

On Thu, Nov 17, 2016 at 1:07 AM, Amin Timany <amintimany AT gmail.com> wrote:

Hi Polina,

Instead of the nthProd, you can use the following alternative definition:

Require Import Categories.Essentials.Notations.
Require Import Categories.Category.Category.
Require Import Categories.Basic_Cons.CCC.

Section nth_Prod.
 Context {C : Category} {HT: Terminal C} {HP: Has_Products C}.

 Record nth_ProdT :=
  { npT : Type; npel:> npT; npobj : npT → C}.

 Fixpoint nth_Prod (A : C) (n : nat) : nth_ProdT :=
  match n with
  | O => {| npT := (Terminal C); npel := HT; npobj := terminal |}
  | S m =>
     {| npT := Product A (npobj (nth_Prod A m) (nth_Prod A m));
        npel := HP A (npobj (nth_Prod A m) (nth_Prod A m));
        npobj := product _ _ |}
  end.

 Definition nth_Prod_obj (np : nth_ProdT) : C := npobj np np.
 Coercion nth_Prod_obj : nth_ProdT >-> Obj.

 Fixpoint arrow_to_nthProd (A B : C) (f : (A –≻ B)%morphism) (n : nat) :
  (A –≻ (nth_Prod B n))%morphism :=
  match n with
  | O => t_morph _ _
  | S m => Prod_morph_ex _ _ f (arrow_to_nthProd A B f m)
  end.

End nth_Prod.

Notice that here I have defined a type nth_ProdT which doesn’t directly include the object that you want (the n-fold product of an object). Instead it comes with a type which depending on n in nth_Prod can be a Terminal (the complete record) or a Product (the complete record) of A and the object computed from the lower level (m in case n = S m). It also includes an element of this type and a way to get an object out of this element. This way, you can keep the information you want around, e.g., the unique morphism to the terminal object (t_morph above) the projections of product, etc. You can use this to for example define something lie arrow_to_nthProd above.

Regards,
Amin

> On 17 Nov 2016, at 04:36, Polina Vinogradova <polina.vino AT gmail.com> wrote:
>
> Hello !
>
> I am trying to build a coercion that would allow me to apply the projection function found in the Product Type Class (category-theoretic notion thereof) to an n-fold product of an object A (in a category).
>
> I need to to build a function akin to
>
> Fixpoint func (A B:Obj) ( m:nat) ( f: B Hom (nthProd A m) )
>     (  ... other parameters) : Prop :=
> match m with
> | 0 => ..
> | S m' => ..
> | S (S m') => func A (S m') (compose f Pi_2) ...
> end.
>
> for this , I need
>  (nthProd  A (S (S m))) : (Product A (nthProd A (S m)))
> (but it is merely of type Obj)
>
> or something like that, so that
> f : Hom B (Product A (nthProd A (S m)))
> (compose f Pi_2) : Hom B  (nthProd A (S m))
>
>  Alternatively, I need to build a function Pi_2' that would take the available arguments and produce a map of the right type to recursively call func with. Here, nthProd is
>
> Fixpoint nthProd (A : RC) (n : nat) : Obj :=
> match n with
>
>   | 0 => termial_obj
>   | S 0 => A
>   | S m => (Has_Products A (nthProd  A m))
>
> end.
>
> I have been trying to work this out for a while now and I would really appreciate any ideas on defining the appropriate coercions or avoiding this problem in some other way!
>
> Thank you!
>
> Polina
>