DHOL error in typing - proof obligation?
I get an error typing the following. error.mmt
The error is the following:
error.mmt 18:invalid unit: patrick-nicodemus:/category-theory?Bicat?error?definition: Judgment |-- [x:tm obj]hzcomp_twocells@x :: tm Πͭ [x:tm obj]Πͭ [y:tm obj]Πͭ [z:tm obj]Πͭ [fa:tm (mor x y)]Πͭ [fb:tm (mor x y)]Πͭ [ga:tm (mor y z)]Πͭ [gb:tm (mor y z)]Πͭ [alpha:tm (twocells x y fa fb)]Πͭ [beta:tm (twocells y z ga gb)]twocells x z hzcomp@x@y@z@fa@ga hzcomp@x@y@z@fb@gb: [x:tm obj]hzcomp_twocells@x