Open omasanori opened 1 year ago
Originally pointed out by @zick in https://twitter.com/zick_minoh/status/1525789599997448192 (in Japanese).
While the type of applicate is E → E* → P → K → C, the definition of cwv contains an expression applicate ε₂ε*ω which implies E → E* → P → C. The corresponding part should be applicate ε₂ε*ωκ.
applicate
E → E* → P → K → C
cwv
applicate ε₂ε*ω
E → E* → P → C
applicate ε₂ε*ωκ
Originally pointed out by @zick in https://twitter.com/zick_minoh/status/1525789599997448192 (in Japanese).
While the type of
applicateisE → E* → P → K → C, the definition ofcwvcontains an expressionapplicate ε₂ε*ωwhich impliesE → E* → P → C. The corresponding part should beapplicate ε₂ε*ωκ.