The Coq mailing list

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

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