search

nmvdw / Three-HITs

All higher inductive types can be obtained from three simple HITs.
17 stars 2 forks source link

Definition of a constructor term over a given `c` #2

Closed andrejbauer closed 7 years ago

andrejbauer commented 7 years ago

The definition of a constructor term (labeled def:constructor-term) seems fishy. They way it's written, I can come up with any term e whatsoever, and then claim that π₁(e, e) is a constructor term. What was actually meant here?

Also, the premise that c : A T → T is a function is not clear. What is A? What is T?

nmvdw commented 7 years ago

The term e should be a constructor term if you want (e, e) and thus \pi_1(e, e) to be a constructor term. So, there is an extra condition on e.

I will change the premise so that A is polynomial and T is a type.