This is a repository for formalization in objective type theory, shallowly embedded into Agda.
See Theory.agda for formalized content. See Rules.agda for details on the embedding into Agda.
This is a repository for formalization in objective type theory, shallowly embedded into Agda.
See Theory.agda for formalized content. See Rules.agda for details on the embedding into Agda.