mikeshulman/ohtt

This is stars and forks stats for /mikeshulman/ohtt repository. As of 20 Apr, 2024 this repository has 34 stars and 2 forks.

Higher Observational Type Theory Overview This is an implementation in Agda of Higher Observational Type Theory (a.k.a. Observational Homotopy Type Theory, especially in case-insensitive contexts such as github repository names). It is a "very shallow" embedding using Agda's experimental --two-level type theory: the fibrant fragment contains HOTT with its homotopical identity type, while the strict equality of the exo-fragment represents the definitional equality of HOTT. In addition, we declare...