[Agda] Defining Coq(w/o Prop) in Agda using Induction Recursion

Nils Anders Danielsson nad at cse.gu.se
Tue Nov 26 10:55:30 CET 2013

On 2013-11-26 00:38, Abhishek Anand wrote:
> Has someone tried to define(using IR) a universe closed under both PI
> and strictly-positive-Inductive type-constructors? (Coq's first
> universe seems to match that description precisely.)


   Hier Soir, an OTT Hierarchy
   Conor McBride

> If so, does the definition fit in Set 0 of Agda?

Yes: "We’ve built something like Coq’s hierarchy inside Agda’s lowest


More information about the Agda mailing list