私は次のようにします:
π1 : A × B → A
π1 ∘ π1 : A × B × C → A
π1 ∘ π1 ∘ π1 : A × B × C × D → A
map (π1 ∘ π1 ∘ π1) : (A × B × C × D) * → A *
map (map (π1 ∘ π1 ∘ π1)) : ((A × B × C × D) *) * → (A *) *
これが必要かもしれません:
Definition comp {s1 s2 s3 : Set} (f2 : s2 -> s3) (f1 : s1 -> s2) (o1 : s1) : s3 :=
f2 (f1 o1).
Notation "f2 ∘ f1" := (comp f2 f1) (at level 30, right associativity).
Inductive Prod (s1 s2 : Set) : Set :=
| Pair : s1 -> s2 -> Prod s1 s2.
Arguments Pair {_ _} _ _.
Notation "s1 × s2" := (Prod s1 s2) (at level 40, left associativity).
Notation "( o1 , o2 , .. , o3 )" := (Pair .. (Pair o1 o2) .. o3) (at level 0).
Definition proj_1 {s1 s2 : Set} (p1 : s1 × s2) : s1 :=
match p1 with
| (o1, _) => o1
end.
Notation "'π1'" := proj_1 (at level 0).
Inductive List (s1 : Set) : Set :=
| Nil : List s1
| Cons : s1 -> List s1 -> List s1.
Arguments Nil {_}.
Arguments Cons {_} _ _.
Notation "s1 *" := (List s1) (at level 30, no associativity).
Notation "'ε'" := Nil (at level 0).
Notation "o1 ◁ l1" := (Cons o1 l1) (at level 60, right associativity).
Fixpoint map {s1 s2 : Set} (f1 : s1 -> s2) (l1 : s1 *) : s2 * :=
match l1 with
| ε => ε
| o1 ◁ l2 => (f1 o1) ◁ (map f1 l2)
end.