Categorical structures for type theory in univalent foundations MG51GG0QZN

URI	`m2://res/MG51GG0QZN`
Kind	preprint
Creators	Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky
Date	2017-05-11
MSC	03-XX, 18-XX
Subjects	arxiv math.LO, arxiv cs.LO, arxiv math.CT
Scope	in

Expressions

e1: version, preprint

Language	en
Date	2017-05-11
Ids	arXiv 1705.04310, DOI 10.23638/lmcs-14(3:18)2018, zbl 1496.03053, zbl_id 6943957

Items in this resource

The mentions of the inventory that name this resource. Each name links to the card of its inventory row.

Item	Kind	Where	Source
1SSQAN1YSZ	problem	problem 3.16	arxiv
1XRGPRNPQB	problem	problem 4.11	arxiv
2EKHM9WRFN	problem	problem 4.7	arxiv
\coqident{obj_ext_structure	definition	definition 3.4	arxiv
762SA82XDR	problem	problem 4.5	arxiv
88WQERRR2Q	definition	definition 3.2	arxiv
\coqident{is_universe_transfer	statement	lemma 4.9	arxiv
8ZD76N6HJD	problem	problem 3.6	arxiv
AA9ZEFGK66	problem	problem 5.3	arxiv
ATC9SD7HCT	definition	definition 5.12	arxiv
\coqident{isaprop_rel_universe_structure	statement	lemma 4.3	arxiv
BF66SWW6JP	definition	definition 3.13	arxiv
\coqident{fpullback	definition	definition 4.1	arxiv
C6HWA8CR4F	example	example 3.20	arxiv
CSTVKR006M	problem	problem 5.5	arxiv
CTRCN3ST3G	definition	definition 5.4	arxiv
CX4D18D5P0	problem	problem 5.7	arxiv
D9SSEXB8HQ	problem	problem 3.12	arxiv
DNSJXZR87B	problem	problem 5.11	arxiv
E03SAWT8R7	definition	definition 4.8	arxiv
E0EXQ1F9A0	definition	definition 3.7	arxiv
\coqident{weq_relative_universe_weak_relative_universe	statement	corollary 4.4	arxiv
F6ZMF8P2BY	definition	definition 5.8	arxiv
GDFW7XCG4X	problem	problem 5.9	arxiv
\coqident{isweq_from_cwf_to_rep	statement	lemma 5.2	arxiv
cf.\ },; \coqident{typecat_structure}, \coqident{is_split_}\allowbreak\coqident{typecat}, \coqident{split_typecat_structure	definition	definition 3.3	arxiv
\coqident{term_fun_structure	definition	definition 3.5	arxiv
HQW47M43V5	definition	definition 4.6	arxiv
HTKXCG9HFP	definition	definition 5.10	arxiv
K28BGA367Q	problem	problem 3.14	arxiv
KPR4MAS86M	definition	definition 4.12	arxiv
\coqident{isweq_is_universe_transfer	statement	lemma 4.10	arxiv
M5QZ807EB2	definition	definition 3.10	arxiv
MWYSCNW70R	definition	definition 5.6	arxiv
\coqident{rep_map	definition	definition 5.1	arxiv
PTHN7WDAJE	definition	definition 3.17	arxiv
\coqident{cwf_structure}}, {\coqident{cwf	definition	definition 3.1	arxiv
\coqident{qq_morphism_structure	definition	definition 3.8	arxiv
TEAYPWH05N	definition	definition 3.15	arxiv
TMT22XE08K	problem	problem 3.18	arxiv
\coqident{relative_universe}, \coqident{weak_relative_universe	definition	definition 4.2	arxiv
WEQFSVPV7Q	problem	problem 3.9	arxiv
YXJNBKEW27	definition	definition 3.19	arxiv
ZZ46KW0RDZ	definition	definition 3.11	arxiv

Catalogue records

arxiv: 1705.04310 (work)
zbmath_search: 6943957 (work)