%PDF-1.4 % 4 0 obj > endobj 7 0 obj (Quotients of Bounded Natural Functors) endobj 8 0 obj > endobj 11 0 obj (1 Introduction) endobj 12 0 obj > endobj 15 0 obj (2 Background) endobj 16 0 obj > endobj 19 0 obj (2.1 Bounded Natural Functors) endobj 20 0 obj > endobj 23 0 obj (2.2 Quotient types) endobj 24 0 obj > endobj 27 0 obj (3 Quotients of Bounded Natural Functors) endobj 28 0 obj > endobj 31 0 obj (3.1 Characterization of the BNF setter) endobj 32 0 obj > endobj 35 0 obj (3.2 The quotient's setter) endobj 36 0 obj > endobj 39 0 obj (3.3 The quotient's relator) endobj 40 0 obj > endobj 43 0 obj (3.4 Subdistributivity via confluent relations) endobj 44 0 obj > endobj 47 0 obj (3.5 Non-emptiness witnesses) endobj 48 0 obj > endobj 51 0 obj (3.6 Partial quotients) endobj 52 0 obj > endobj 55 0 obj (4 Implementation) endobj 56 0 obj > endobj 59 0 obj (4.1 The lift\137bnf command) endobj 60 0 obj > endobj 63 0 obj (4.2 Transfer rule generation) endobj 64 0 obj > endobj 67 0 obj (5 Related work) endobj 68 0 obj > endobj 71 0 obj (5.1 Quotients in the category of Sets) endobj 72 0 obj > endobj 75 0 obj (5.2 Comparison with Lean's quotients of polynomial functors) endobj 76 0 obj > endobj 79 0 obj (6 Conclusion) endobj 80 0 obj > endobj 130 0 obj > stream xڭ]oFݿBtmK=$Iu@KūD*$U7K.)n ~/|꛷Li#ۅHclaafq|v1-}_էjSlcޝ|OjM!Xİ$+2͗ 8M線E2# \ Ԥ̘vҟ0^pcZ ̊TISS4Q ST֊ahCH3*XyYm"wPwwn?R OUxeWo\_LpO-Lgb}|ŸVM;ou}3 :)i,[4#)**2㿔B %1L>]S>RzbBz\P6z%*b &LS`іQ԰}vewꊱx_mwe]9i(֧&|];g}8Ƌu~G_I8E3*5\eG>{J,`PA{ٶ#yp,tM|w{ {+Ms@aSaƜ|k&_wlc;gY 8" r{U:ڒ.-U5Xw;GRD[jvGg]W)ݷRb A9Rd0 !qlN%a)>q.))4MmJHhպ\SO] ٭,%?