Pages that link to "Item:Q2031691"
From MaRDI portal
The following pages link to The simplicial model of univalent foundations (after Voevodsky) (Q2031691):
Displaying 43 items.
- Univalence in locally Cartesian closed categories (Q524707) (← links)
- Homotopy type theory in Lean (Q1687770) (← links)
- The Frobenius condition, right properness, and uniform fibrations (Q2013548) (← links)
- Filter quotients and non-presentable \((\infty,1)\)-toposes (Q2040521) (← links)
- A characterisation of elementary fibrations (Q2131276) (← links)
- Towards a directed homotopy type theory (Q2133175) (← links)
- The construction of set-truncated higher inductive types (Q2133178) (← links)
- Guarded cubical type theory (Q2319985) (← links)
- From signatures to monads in \textsf{UniMath} (Q2319990) (← links)
- Observability in the univalent universe (Q2675950) (← links)
- C-system of a module over a \(Jf\)-relative monad (Q2689172) (← links)
- A type theory for synthetic $\infty$-categories (Q3121017) (← links)
- (Q3121020) (← links)
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types (Q5016211) (← links)
- Model structure on the universe of all types in interval type theory (Q5022925) (← links)
- Syntax and models of Cartesian cubical type theory (Q5022926) (← links)
- The Interpretation Lifting Theorem for C-Systems (Q5025082) (← links)
- (Q5028425) (← links)
- Canonicity and homotopy canonicity for cubical type theory (Q5028486) (← links)
- (Q5031679) (← links)
- Cubical methods in homotopy type theory and univalent foundations (Q5055493) (← links)
- Bicategories in univalent foundations (Q5055496) (← links)
- (Q5094128) (← links)
- Models of Type Theory Based on Moore Paths (Q5111326) (← links)
- Modalities in homotopy type theory (Q5208873) (← links)
- Univalence for inverse diagrams and homotopy canonicity (Q5740656) (← links)
- Simplicial sets inside cubical sets (Q5858940) (← links)
- The effective model structure and -groupoid objects (Q5866297) (← links)
- The Hurewicz theorem in homotopy type theory (Q6112530) (← links)
- Strange new universes: Proof assistants and synthetic foundations (Q6130525) (← links)
- On Small Types in Univalent Foundations (Q6135756) (← links)
- Univalent categories of modules (Q6149909) (← links)
- Bicategorical type theory: semantics and syntax (Q6149956) (← links)
- On the ∞$\infty$‐topos semantics of homotopy type theory (Q6150054) (← links)
- What should a generic object be? (Q6174093) (← links)
- Towards a constructive simplicial model of Univalent Foundations (Q6176777) (← links)
- Non-accessible localizations (Q6564515) (← links)
- Topological quantum gates in homotopy type theory (Q6584358) (← links)
- Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories (Q6612003) (← links)
- Modal fracture of higher groups (Q6614927) (← links)
- Semantics for two-dimensional type theory (Q6649441) (← links)
- Syllepsis in homotopy type theory (Q6649459) (← links)
- Examples and cofibrant generation of effective Kan fibrations (Q6671729) (← links)
