FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

This page contains an index consisting of author-provided keywords.

A
AB axioms	The internal AB axioms
Agda	An Experiment with 2LTT Features in Agda
Applied topology	Elementary Simplicial Collapses in Cubical Agda
Artin gluing	Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability
Assemblies	Groupoidal Realizability: Formalizing the Topological BHK Interpretation
C
categories with families	Towards Directed Higher Observational Type Theory
computer-checked proofs	Semantics for two-dimensional type theory
constructive algebra	The internal AB axioms
Coq	A Library of Monoidal Categories for Display and Univalence
cubical sets	A type-theoretic model structure over cubes with one connection presenting spaces
D
directed type theory	Towards Directed Higher Observational Type Theory
Discrete Morse theory	Elementary Simplicial Collapses in Cubical Agda
F
formal mathematics	Elementary Simplicial Collapses in Cubical Agda
formalization	An Experiment with 2LTT Features in Agda
formalization of category theory	A Library of Monoidal Categories for Display and Univalence
G
group cohomology	Towards computing cohomology of dependent abelian groups
Groupoids	Groupoidal Realizability: Formalizing the Topological BHK Interpretation
H
higher observational type theory	Towards Directed Higher Observational Type Theory
homological algebra	Towards computing cohomology of dependent abelian groups The internal AB axioms
homotopy type theory	Towards Directed Higher Observational Type Theory Towards computing cohomology of dependent abelian groups A type-theoretic model structure over cubes with one connection presenting spaces The Compatibility of MF with HoTT Models of homotopy type theory from the Yoneda embedding The internal AB axioms TBA TBA Internal languages of diagrams of ∞-toposes
I
Impredicative universe	Groupoidal Realizability: Formalizing the Topological BHK Interpretation
infinity-topos	Internal languages of diagrams of ∞-toposes
internal language	Internal languages of diagrams of ∞-toposes
K
Kan-Quillen model structure	A type-theoretic model structure over cubes with one connection presenting spaces
L
lex modality	Internal languages of diagrams of ∞-toposes
M
Minimalist Type Theory	The Compatibility of MF with HoTT
monoidal category	A Library of Monoidal Categories for Display and Univalence
N
normalization by evaluation	Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability
Q
Quasicategories	Models of homotopy type theory from the Yoneda embedding
Quillen equivalence	A type-theoretic model structure over cubes with one connection presenting spaces
Quotient model	The Compatibility of MF with HoTT
R
Realizability	Groupoidal Realizability: Formalizing the Topological BHK Interpretation
Reedy category	A type-theoretic model structure over cubes with one connection presenting spaces
S
Semantic	Models of homotopy type theory from the Yoneda embedding
semantics	Semantics for two-dimensional type theory
sheaf cohomology	Towards computing cohomology of dependent abelian groups
simplicial type theory	Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability
synthetic Tait computability	Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability
T
two level type theory	An Experiment with 2LTT Features in Agda
type theory	Semantics for two-dimensional type theory TBA TBA
U
UniMath	A Library of Monoidal Categories for Display and Univalence
univalence	Groupoidal Realizability: Formalizing the Topological BHK Interpretation A Library of Monoidal Categories for Display and Univalence
Univalent Foundations	TBA TBA
Y
Yoneda lemma	Models of homotopy type theory from the Yoneda embedding

Disclaimer | Powered by EasyChair Smart Program