The following pages link to (Q4247303):
Displaying 50 items.
- Category theory, logic and formal linguistics: some connections, old and new (Q280832) (← links)
- Modeling Martin-Löf type theory in categories (Q280835) (← links)
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory (Q280837) (← links)
- The intrinsic topology of Martin-Löf universes (Q290640) (← links)
- Martin-Löf complexes (Q385803) (← links)
- Combinatorial realizability models of type theory (Q385804) (← links)
- The category of equilogical spaces and the effective topos as homotopical quotients (Q504545) (← links)
- Constructions of categories of setoids from proof-irrelevant families (Q512135) (← links)
- Univalence in locally Cartesian closed categories (Q524707) (← links)
- Proof-relevance of families of setoids and identity in type theory (Q661282) (← links)
- Isomorphism is equality (Q740487) (← links)
- The identity type weak factorisation system (Q959823) (← links)
- On the strength of dependent products in the type theory of Martin-Löf (Q1024547) (← links)
- Game semantics for dependent types (Q1641014) (← links)
- Univalent completion (Q1659918) (← links)
- Homotopy type theory in Lean (Q1687770) (← links)
- Meaning explanations at higher dimension (Q1688954) (← links)
- Univalent foundations as structuralist foundations (Q1708879) (← links)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 (Q1731963) (← links)
- Univalence as a principle of logic (Q1788330) (← links)
- The simplicial model of univalent foundations (after Voevodsky) (Q2031691) (← links)
- A characterisation of elementary fibrations (Q2131276) (← links)
- Towards a directed homotopy type theory (Q2133175) (← links)
- Constructing a universe for the setoid model (Q2233391) (← links)
- The justification of identity elimination in Martin-Löf's type theory (Q2288279) (← links)
- Preface: Special issue on homotopy type theory and univalent foundations (Q2319980) (← links)
- On a possible application of the homotopy concept to model theory (Q2448535) (← links)
- Observability in the univalent universe (Q2675950) (← links)
- Homotopy type theory and Voevodsky’s univalent foundations (Q2933829) (← links)
- The Local Universes Model (Q2957763) (← links)
- Notions of anonymous existence in Martin-Löf type theory (Q2980980) (← links)
- Homotopy-Theoretic Models of Type Theory (Q3007656) (← links)
- (Q3105096) (← links)
- A homotopy-theoretic model of function extensionality in the effective topos (Q3119466) (← links)
- Data Types with Symmetries and Polynomial Functors over Groupoids (Q3178294) (← links)
- (Q3204678) (← links)
- Homotopies in Grothendieck fibrations (Q3305548) (← links)
- Mathesis Universalis and Homotopy Type Theory (Q3305624) (← links)
- From Mathesis Universalis to Provability, Computability, and Constructivity (Q3305633) (← links)
- Weak ω-Categories from Intensional Type Theory (Q3637194) (← links)
- (Q4470942) (← links)
- Heterogeneous Substitution Systems Revisited (Q4580223) (← links)
- (Q4944848) (← links)
- (Q4944852) (← links)
- Semantics of higher inductive types (Q4958656) (← links)
- (Q4989403) (← links)
- HOMOTOPY MODEL THEORY (Q5021916) (← links)
- (Q5028425) (← links)
- Bicategories in univalent foundations (Q5055496) (← links)
- Hom weak ω-categories of a weak ω-category (Q5058363) (← links)
