Andrew Marmaduke amarmaduke

## IRExample.v
(**
Dybjer and Setzer provide a logical framework in which Induction-Recursion —
mutual definition of an (A : Type) and a (B : A -> V), in which constructors for A can talk about values of B, and B is defined by case analysis on members of A —
becomes equivalent to supposing initial algebras for certain functors on { X : Set & X -> V }.  However, this latter family is, up to equivalences over V, the same as ordinary maps V -> Set.  The universal case, in which V = Set, becomes somewhat trickier, for universe level reasons.

In any case, here is one way to define a "large" universe ("large" in the sense: we allow all externally definable functions) with naturals, dependent sums, and dependent products.  A more careful presentation might work on a fibration over functions,
 { AB : Type * Type & fst AB -> snd AB } -> Type
instead, but good luck with that.
*)
	(**
	Dybjer and Setzer provide a logical framework in which Induction-Recursion —
	mutual definition of an (A : Type) and a (B : A -> V), in which constructors for A can talk about values of B, and B is defined by case analysis on members of A —
	becomes equivalent to supposing initial algebras for certain functors on { X : Set & X -> V }. However, this latter family is, up to equivalences over V, the same as ordinary maps V -> Set. The universal case, in which V = Set, becomes somewhat trickier, for universe level reasons.

	In any case, here is one way to define a "large" universe ("large" in the sense: we allow all externally definable functions) with naturals, dependent sums, and dependent products. A more careful presentation might work on a fibration over functions,
	{ AB : Type * Type & fst AB -> snd AB } -> Type
	instead, but good luck with that.
	*)