%PDF-1.5
%
1 0 obj
<<
/Metadata 2 0 R
/Names 3 0 R
/OpenAction 4 0 R
/Outlines 5 0 R
/PageMode /UseNone
/Pages 6 0 R
/Type /Catalog
>>
endobj
7 0 obj
<<
/Author (Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg)
/CreationDate (D:20180221182841Z)
/Creator (LaTeX with hyperref package)
/Keywords ()
/ModDate (D:20191128102850Z)
/PTEX.Fullbanner (This is pdfTeX, Version 3.14159265-2.6-1.40.16 \(TeX Live 2015/Debian\) kpathsea version 6.2.1)
/Producer (pdfTeX-1.40.16)
/Subject ()
/Title (Quotient Inductive-Inductive Types)
/Trapped /False
>>
endobj
2 0 obj
<<
/Length 3958
/Subtype /XML
/Type /Metadata
>>
stream
application/pdf
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg
Quotient Inductive-Inductive Types
2018-02-21T18:28:41Z
LaTeX with hyperref package
2019-11-28T10:28:50Z
2019-11-28T10:28:50Z
pdfTeX-1.40.16
False
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) kpathsea version 6.2.1
uuid:817510f7-a871-4f2f-ac4d-c3ce2c333703
uuid:aaa68241-12d7-4569-bb5f-6ec8e8263f14
endstream
endobj
3 0 obj
<<
/Dests 8 0 R
>>
endobj
4 0 obj
<<
/D [9 0 R /Fit]
/S /GoTo
>>
endobj
5 0 obj
<<
/Count 13
/First 10 0 R
/Last 10 0 R
/Type /Outlines
>>
endobj
6 0 obj
<<
/Count 19
/Kids [11 0 R 12 0 R 13 0 R]
/Type /Pages
>>
endobj
8 0 obj
<<
/Kids [14 0 R 15 0 R 16 0 R]
/Limits [(Doc-Start) (theorem.1.4.31)]
>>
endobj
9 0 obj
<<
/Annots [17 0 R 18 0 R 19 0 R 20 0 R 21 0 R 22 0 R 23 0 R 24 0 R 25 0 R 26 0 R]
/Contents [27 0 R 28 0 R 29 0 R 30 0 R 31 0 R 32 0 R 33 0 R 34 0 R]
/CropBox [0 0 612 792]
/MediaBox [0 0 612 792]
/Parent 11 0 R
/Resources 35 0 R
/Rotate 0
/Type /Page
>>
endobj
10 0 obj
<<
/A 36 0 R
/Count 12
/First 37 0 R
/Last 38 0 R
/Parent 5 0 R
/Title
>>
endobj
11 0 obj
<<
/Count 7
/Kids [39 0 R 9 0 R 40 0 R 41 0 R 42 0 R 43 0 R 44 0 R]
/Parent 6 0 R
/Type /Pages
>>
endobj
12 0 obj
<<
/Count 6
/Kids [45 0 R 46 0 R 47 0 R 48 0 R 49 0 R 50 0 R]
/Parent 6 0 R
/Type /Pages
>>
endobj
13 0 obj
<<
/Count 6
/Kids [51 0 R 52 0 R 53 0 R 54 0 R 55 0 R 56 0 R]
/Parent 6 0 R
/Type /Pages
>>
endobj
14 0 obj
<<
/Kids [57 0 R 58 0 R 59 0 R 60 0 R 61 0 R 62 0 R]
/Limits [(Doc-Start) (cite.sojakova2015hits)]
>>
endobj
15 0 obj
<<
/Kids [63 0 R 64 0 R 65 0 R 66 0 R 67 0 R 68 0 R]
/Limits [(cite.typicalAmbiguity) (page.14)]
>>
endobj
16 0 obj
<<
/Kids [69 0 R 70 0 R 71 0 R 72 0 R 73 0 R 74 0 R]
/Limits [(page.15) (theorem.1.4.31)]
>>
endobj
17 0 obj
<<
/A <<
/D (cite.martinlof1972ITT)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /I
/Rect [395.978 319.364 407.931 327.748]
/Subtype /Link
/Type /Annot
>>
endobj
18 0 obj
<<
/A <<
/D (cite.coq)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /I
/Rect [260.97 307.409 267.942 315.793]
/Subtype /Link
/Type /Annot
>>
endobj
19 0 obj
<<
/A <<
/D (cite.moura:lean)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /I
/Rect [317.876 307.409 329.828 315.793]
/Subtype /Link
/Type /Annot
>>
endobj
20 0 obj
<<
/A <<
/D (cite.agda)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /I
/Rect [198.995 295.454 210.948 303.837]
/Subtype /Link
/Type /Annot
>>
endobj
21 0 obj
<<
/A <<
/D (cite.idris)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /I
/Rect [261.449 295.454 268.422 303.837]
/Subtype /Link
/Type /Annot
>>
endobj
22 0 obj
<<
/A <<
/D (cite.Univalent2013)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /I
/Rect [172.747 283.499 184.699 291.882]
/Subtype /Link
/Type /Annot
>>
endobj
23 0 obj
<<
/A <<
/D (cite.awodeyWarren2009id)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /I
/Rect [307.602 271.543 314.574 279.927]
/Subtype /Link
/Type /Annot
>>
endobj
24 0 obj
<<
/A <<
/D (cite.kapulkinLumsdaine2016SSet)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /I
/Rect [390.659 271.543 402.611 279.927]
/Subtype /Link
/Type /Annot
>>
endobj
25 0 obj
<<
/A <<
/D (cite.voevodsky2010Uni)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /I
/Rect [406.706 271.543 418.658 279.927]
/Subtype /Link
/Type /Annot
>>
endobj
26 0 obj
<<
/A <<
/D (cite.shulmanSynth)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /I
/Rect [449.009 128.081 460.962 136.465]
/Subtype /Link
/Type /Annot
>>
endobj
27 0 obj
<<
/Length 456
/Filter /FlateDecode
>>
stream
HSMo0Wh0{lVmU)]H.H;ƛfEJ=MrZ(hHF(o CD:V%}?5uS"9:}2Y "w\pkL˕"4T!֊
b*0N"|vD;N}r@jAȀqeٷ}(|[
M?MC0@,/$)kձ|܍P^Dݫfӷ3!7jLi(+Mu)yspHE?SFq>@,xoqt?xLzas|ˮ#^%ȡf\CuX+˶oj=wЃx:「ak!w3 _pv6gԷ!L!vgo|s>mkIY
OWݴN F
endstream
endobj
28 0 obj
<<
/Length 553
/Filter /FlateDecode
>>
stream
HtSM0+\cU*[wnBRNIƤI.7TYϊ楑Yּ~C6
$e&Y)%7ri-V2k?v3n̋JH6ݴ%/k֡d)/(Mhur)OsaoH JJ2Ӫz]C{