universe elimination rules

• To: types@dcs.gla.ac.uk, l-logic@math.uio.no
• Subject: universe elimination rules
• From: Daniel Mahler <mahler@socs.uts.edu.au>
• Date: Tue, 22 Aug 1995 18:31:27 +1000
• Approved: types@dcs.gla.ac.uk

Could someone tell me what are universe elimination rules in type theories.

Do they have something to do with quantifying or abstracting over universes?
Are there type systems which actually do this?

	thanks
	Daniel Mahler

[All, Please send your replies to Daniel Mahler.
 Daniel Mahler, Please summarise your replies to the Types Forum.
  -- Philip Wadler, moderator, Types Forum.]

• Prev: announcement of a congress
• Next: CADE-13 Call for Papers
• Index(es):
  • Main
  • Thread