Error: Illegal application (Non-functional construction)

Question

I'm trying to work some proofs of the various deMorgans laws using the type constructors/eliminators from the HoTT book. I had hopped to pick through https://mdnahas.github.io/doc/Reading_HoTT_in_Coq.pdf for relevant stuff and dump it all into a .v text file. I need Elimination/Introduction rules for product, co-product and a way to set up negation. So far I have,

Definition idmap {A:Type} (x:A) : A := x.

Inductive prod {A B:Type} : Type := pair : A -> B -> @prod A B.

Notation "x * y" := (prod x y) : type_scope.

Section projections.
  Context {A : Type} {B : Type}.
  Definition fst (p: A * B ) :=
    match p with
      | (x , y) => x
    end.

  Definition snd (p:A * B ) :=
    match p with
      | (x , y) => y
    end.
End projections.

The Error on "Definition fst (p: A * B ) :=" is

Error: Illegal application (Non-functional construction): 
The expression "prod" of type "Type"
cannot be applied to the term
 "A" : "Type"

I tried searching through the error list on the Coq site but didn't find anything.

Answer 1

There are two issues with your code:

• prod's two Type arguments are declared implicit

As a consequence, the notation "x * y" corresponds to prod {_} {_} x y which will always lead to ill-typed terms: prod {_} {_} is a Type and as such it does not make sense to apply something to it.

The fix is to turn these two implicit arguments into explicit ones:

Inductive prod (A B:Type) : Type := pair : A -> B -> @prod A B.

• The notation (x , y) has not been declared

Once you've fixed the definition of prod, the definition still don't typecheck because Coq does not know what you mean by the pattern (x, y). You can declare it as a new notation before your Section projections like so:

Notation "x , y" := (pair _ _ x y) (at level 10).