The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

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
>