I thought a bit about infinitary type theory.
In categorical terms, the "meta-theory" is the base of a Grothendieck fibration
whose fibers are categories of "external" families.
It might be worth describing the axioms.
André
________________________________________
From: HomotopyT...@googlegroups.com [HomotopyT...@googlegroups.com] on behalf of Michael Shulman [shu...@sandiego.edu]
Sent: Sunday, June 22, 2014 2:05 AM
To: HomotopyT...@googlegroups.com
Subject: [HoTT] Infinitary type theory
Mike
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com.