feat(hott/init): add notation for sigma types
test(tests/lean/hott): add test for no_confusion construction for HoTT
test(tests/lean/hott): add test for no_confusion construction for HoTT