Dr NICOLAI KRAUS's Outputs (2)

Extending Homotopy Type Theory with Strict Equality (2016)
Presentation / Conference Contribution
Altenkirch, T., Capriotti, P., & Kraus, N. (2016, August). Extending Homotopy Type Theory with Strict Equality. Presented at 25th EACSL Annual Conference on Computer Science Logic, CSL 2016., Marseille, France

In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult a... Read More about Extending Homotopy Type Theory with Strict Equality.

Constructions with Non-Recursive Higher Inductive Types (2016)
Presentation / Conference Contribution
Kraus, N. (2016, July). Constructions with Non-Recursive Higher Inductive Types. Presented at LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science, New York NY USA

© 2016 ACM. Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say tha... Read More about Constructions with Non-Recursive Higher Inductive Types.