In the w-types section of the induction chapter, there is an erroneously notated type 'C' that should be a type family eliminated with argument 'a' i.e. C(a). This happened when deriving 'e' during the derivation of 'double' using the recursor for w-types.
In the w-types section of the induction chapter, there is an erroneously notated type 'C' that should be a type family eliminated with argument 'a' i.e. C(a). This happened when deriving 'e' during the derivation of 'double' using the recursor for w-types.