Yuta TAKAHASHI
Codes
A formalisation of Aczel's constructive set theory CZF in Agda with a Mahlo universe
An Agda formalisation of large universe types of Martin-Löf type theory
DTS With Coq Library
Coq tactics for Dependent Type Semantics (forked from
HinaKosa/DTSWithCoq
)