From d89ed0c7a01900fdfeecc830837761e35e2e4ff8 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 30 May 2024 14:10:28 -0500 Subject: [PATCH] 2.11.2 - 2.11.4 --- src/HottBook/Chapter2.lagda.md | 128 +++++++++++++++++------- src/HottBook/Chapter2.pdf | Bin 0 -> 12270 bytes src/HottBook/Chapter2.typ | 59 +++++++++++ src/HottBook/Chapter2Exercises.lagda.md | 1 - src/HottBook/Chapter3.lagda.md | 1 - src/HottBook/Chapter6.lagda.md | 1 - src/MayConcise/Chapter1.lagda.md | 1 - 7 files changed, 151 insertions(+), 40 deletions(-) create mode 100644 src/HottBook/Chapter2.pdf create mode 100644 src/HottBook/Chapter2.typ diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 5e76081..9209779 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -6,7 +6,7 @@ module HottBook.Chapter2 where open import Agda.Primitive open import HottBook.Chapter1 -open import HottBook.Chapter2Lemma221 +open import HottBook.Chapter2Lemma221 public open import HottBook.Util ``` @@ -738,45 +738,67 @@ open axiom2∙10∙3 ### Theorem 2.11.1 ``` -theorem2∙11∙1 : {A B : Set} - → (eqv @ (f , f-eqv) : A ≃ B) - → (a a' : A) - → (a ≡ a') ≃ (f a ≡ f a') -theorem2∙11∙1 (f , f-eqv) a a' = - let - open ≡-Reasoning - mkQinv g α β = isequiv-to-qinv f-eqv - inv : (f a ≡ f a') → a ≡ a' - inv p = (sym (β a)) ∙ (ap g p) ∙ (β a') - backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p - backward q = begin - ap f ((sym (β a)) ∙ (ap g q) ∙ (β a')) ≡⟨ lemma2∙2∙2.i (sym (β a)) (ap g q ∙ β a') ⟩ - ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {! !} ⟩ - ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {! !} ⟩ - id q ∎ - forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p - forward p = begin - (sym (β a)) ∙ (ap g (ap f p)) ∙ (β a') ≡⟨ ap (λ p → (sym (β a)) ∙ p ∙ (β a')) (lemma2∙2∙2.iii f g p) ⟩ - (sym (β a)) ∙ (ap (g ∘ f) p) ∙ (β a') ≡⟨ {! !} ⟩ - -- (sym (β a)) ∙ (ap id p) ∙ (β a') ≡⟨ {! !} ⟩ - id p ∎ - eqv = mkQinv inv backward forward - in - ap f , qinv-to-isequiv eqv +-- theorem2∙11∙1 : {A B : Set} +-- → (eqv @ (f , f-eqv) : A ≃ B) +-- → (a a' : A) +-- → (a ≡ a') ≃ (f a ≡ f a') +-- theorem2∙11∙1 (f , f-eqv) a a' = +-- let +-- open ≡-Reasoning +-- mkQinv g α β = isequiv-to-qinv f-eqv +-- inv : (f a ≡ f a') → a ≡ a' +-- inv p = (sym (β a)) ∙ (ap g p) ∙ (β a') +-- backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p +-- backward q = begin +-- ap f ((sym (β a)) ∙ (ap g q) ∙ (β a')) ≡⟨ lemma2∙2∙2.i (sym (β a)) (ap g q ∙ β a') ⟩ +-- ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {! !} ⟩ +-- ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {! !} ⟩ +-- id q ∎ +-- forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p +-- forward p = begin +-- (sym (β a)) ∙ (ap g (ap f p)) ∙ (β a') ≡⟨ ap (λ p → (sym (β a)) ∙ p ∙ (β a')) (lemma2∙2∙2.iii f g p) ⟩ +-- (sym (β a)) ∙ (ap (g ∘ f) p) ∙ (β a') ≡⟨ {! !} ⟩ +-- -- (sym (β a)) ∙ (ap id p) ∙ (β a') ≡⟨ {! !} ⟩ +-- id p ∎ +-- eqv = mkQinv inv backward forward +-- in +-- ap f , qinv-to-isequiv eqv ``` ### Theorem 2.11.2 ``` --- module theorem2∙11∙2 where --- i : {A : Set} {a x1 x2 : A} --- → (p : x1 ≡ x2) --- → (q : a ≡ x1) --- → transport (λ y → a ≡ y) p q ≡ q ∙ p --- i {A} {a} {x1} {x2} p q = --- J (λ x3 x4 p1 → (q1 : a ≡ x3) → transport (λ y → a ≡ y) p1 q1 ≡ q1 ∙ p1) --- (λ x3 q1 → J (λ x5 x6 q2 → transport (λ y → a ≡ y) refl q1 ≡ q1 ∙ refl) (λ x4 → {! refl !}) a x3 q1) --- x1 x2 p q +module theorem2∙11∙2 where + open ≡-Reasoning + + i : {A : Set} {a x1 x2 : A} + → (p : x1 ≡ x2) + → (q : a ≡ x1) + → transport (λ y → a ≡ y) p q ≡ q ∙ p + i {A} {a} {x1} {x2} p q = + J (λ x3 x4 p1 → (q1 : a ≡ x3) → transport (λ y → a ≡ y) p1 q1 ≡ q1 ∙ p1) + (λ x3 q1 → J (λ x5 x6 q2 → transport (λ y → a ≡ y) refl q1 ≡ q1 ∙ refl) (λ x4 → lemma2∙1∙4.i1 q1) a x3 q1) + x1 x2 p q + + ii : {A : Set} {a x1 x2 : A} + → (p : x1 ≡ x2) + → (q : x1 ≡ a) + → transport (λ y → y ≡ a) p q ≡ sym p ∙ q + ii {A} {a} {x1} {x2} p q = + J (λ x y p → (q1 : x ≡ a) → transport (λ y → y ≡ a) p q1 ≡ sym p ∙ q1) + (λ x q1 → J (λ x y p → transport (λ y → y ≡ a) refl q1 ≡ sym refl ∙ q1) (λ x → lemma2∙1∙4.i2 q1) x a q1) + x1 x2 p q + + iii : {A : Set} {a x1 x2 : A} + → (p : x1 ≡ x2) + → (q : x1 ≡ x1) + → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p + iii {A} {a} {x1} {x2} p q = + J (λ x y p → (q1 : x ≡ x) → transport (λ y → y ≡ y) p q1 ≡ sym p ∙ q1 ∙ p) + (λ x q1 → J (λ x y p → transport (λ y → y ≡ y) refl q1 ≡ sym refl ∙ q1 ∙ refl) + (λ x → let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q1) in lemma2∙1∙4.i2 q1 ∙ helper) + x x q1) + x1 x2 p q ``` ### Theorem 2.11.3 @@ -786,7 +808,41 @@ theorem2∙11∙3 : {A B : Set} → {f g : A → B} → {a a' : A} → (p : a ≡ a') → (q : f a ≡ g a) → transport (λ x → f x ≡ g x) p q ≡ sym (ap f p) ∙ q ∙ (ap g p) -theorem2∙11∙3 p q = {! !} +theorem2∙11∙3 {A} {B} {f} {g} {a} {a'} p q = + J (λ x y p → (q1 : f x ≡ g x) → transport (λ x → f x ≡ g x) p q1 ≡ sym (ap f p) ∙ q1 ∙ (ap g p)) + (λ x q1 → + J (λ x y p → transport (λ z → f z ≡ g z) refl q1 ≡ sym (ap f refl) ∙ q1 ∙ ap g refl) + (λ x → let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q1) in lemma2∙1∙4.i2 q1 ∙ helper) + (f a) (g a) q) + a a' p q +``` + +### Theorem 2.11.4 + +``` +theorem2∙11∙4 : {A : Set} {B : A → Set} {f g : (x : A) → B x} {a a' : A} + → (p : a ≡ a') + → (q : f a ≡ g a) + → transport (λ x → f x ≡ g x) p q ≡ sym (apd f p) ∙ ap (transport B p) q ∙ apd g p +theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} p q = + let open ≡-Reasoning in + J (λ x y p → (q1 : f x ≡ g x) → transport (λ x → f x ≡ g x) p q1 ≡ sym (apd f p) ∙ ap (transport B p) q1 ∙ apd g p) + (λ x q1 → + J (λ x y p → transport (λ z → f z ≡ g z) refl q1 ≡ sym (apd f refl) ∙ ap (transport B refl) q1 ∙ apd g refl) + (λ y → + let + q2 = ap id q1 + q1≡q2 : q1 ≡ q2 + q1≡q2 = J (λ a b p → p ≡ ap id p) (λ x → refl) (f x) (g x) q1 + in + begin + transport (λ z → f z ≡ g z) refl q1 ≡⟨⟩ + q1 ≡⟨ q1≡q2 ⟩ + q2 ≡⟨ (let helper = ap (λ p → refl ∙ p) (lemma2∙1∙4.i1 q2) in lemma2∙1∙4.i2 q2 ∙ helper) ⟩ + refl ∙ ap (transport B refl) q1 ∙ refl ∎ + ) + (f a) (g a) q) + a a' p q ``` ## 2.12 Coproducts diff --git a/src/HottBook/Chapter2.pdf b/src/HottBook/Chapter2.pdf new file mode 100644 index 0000000000000000000000000000000000000000..e1a1a37ac79be05030c94c2b68aebb1a80ac4f44 GIT binary patch literal 12270 zcmb7q2Rzm7`@a!F$S6A}vJ&SQ$8qdEva+`v9P>CwXV{VuA|*1ivRXz)nPo&MvPa1( zva&)*#{YAur=I8ge1E^+|MNP|`P|oiUDtiBd({2rzo4!uDlP`2;lBbrG&E8m2ngfo zK_f3u0|J3f{k@SOuqFnLC$>xoj`#xtkqjYHR1r8Nu@?l^vo^BQ)ezBhN9(yeBC&XP zG?K`mfp)?;yQ5t}U>#>98t;zx7u6=x)sZ+SB-$B)#uLSHAR8z!uCX1l%M@dVb_b-8 zAQ+KGqo_y&a1w2zAu|21#;NJ36Lk`8l=wf{2nd+?r0Y0TO8rfvs(FkZ4!D8%X-lk;A%I z1M)(Q8c+sEgcl9}=?f;J2gM*NDF##~5{DsRosgmjZ2bJ{7$*WT{{~2;Gt&82FHRQZ zjm0?Oka!S~Z5^~bo`#=a2knF+I3s`Y{2PlZP=4s&48$=&Y6Kh}1K7cD>W)VtWkEuR z1kiy^pkDhaNXRH2wA2n;@Pn3=)Im#H{ICT*Y)Krp;D;^g z!Z2Y&~N{Z%8xG#hFX z=|9UAcsp1$iG}~4bq-iF3F@gY0IaTqR?* zSJlN*QtF7Xd;?pHNm<{f`)w5+u&P&8^o*Z*7Ur!!BnA2QYUV^}sLzEA_g56btPHI5 z`=#l=-&v~A|JeQt))Ok7m<*muk{}~z=o5O3{fui6`wgzi9-3P8lAEp8v%KcX+ZdK_I*Lnc z$1l}8Zib%zIkKZ$asRwikvYNmAD$WKhW^@e>;m3LI&rRK;T?Znyh+nFVnvy2r- z$CW!^1$d#pwBC6?VHX2uhqF!8b(zHw@9zcAe!GGsJ19vfC> zQEgFe=&$@eU*aCkksEJORWRyW%{l5?YcsmIRPsZ0Q)9_jVQ0k=nYAAgss_lc-b z3%nqgSn%0CjdOEk(Z6jiWrn?LEpt4;{_FF(X#Yj~NZ-e>4|1bl)=mZ_2da%d8>7eE z^iB4y^sV1auEUSBT#UoKz|<}e)hSWdkST-~sRVYjr`|x>7OFUzXl_HBlM`#ZGu!t`81 z3w%C>tY5`7QRNMP40CRxVxKo9SihvQ-@3=8Xjwd#xYF1+kDC`kV;{u+a5xoo9Qy=^ z!TZ)e!7pRSCoi)oZb=3;G*Mlj9$2O0Sr898{wBB|mppT2#;B_=b4DKQzxR4=7#0NS zTTyxU!F_Au)H3;`VilWW6oqQ&lJc20s?QFCb$3=m$#}XQ97>KT&T>BwUSZ#w;BKN~ zd8Y9|eeD=eM_eYi9g6~t*Ow*>|EPo(7MQ@Aho?Z8>4mE$N58i%*}po_*#_U$s57P z1Hl^x3q|kho5x~bFa|342yH~ZTXx##3KZS&Sh(}9y)@ae{<;EZ;Moo5g|F}UO6^K* z9AT|KEtlD96@9!Gs7fDOA`9isIYgpQv|e{?v{dQfNn>ok`T5mIsk^wa3+H#osmXYy zn>&}LM&m2BE-S6B#sAQ{EQ_6K-TX<6| zLkM9jp{b{7nfvnQ3IoH%kgA!Ls~?|S%i^r_pY6-e&Th>1jT}1_;57R!TTKm2zsOVL z>o(L~qy}U7#$X4<&t2HOFw`BPmZ3(cMo^QCe3M&$v+iUte0z6x+U*klQ*G_|i``M1 zu}jbSUIZ8JzOMieD|!aX?8ojr`fjpXzACvYIAhrMp^u zJGf^9otH#>RS+S0KC>U8Q6k`cOoG9?Oo za&r=@P@xj?ts^otBgca1gGft8S1ri`uS}{}6msUG3%%+TRP5it zyYQYv3biE5D$i3h5PmeR);#UF?!7L_(=YeL*4qgbe(X}H`2e;c_{F-2OstSZgMESQ>_4p|60N0;4o1}=h7gfjnDR<DALZ(T(m3j=jA%2h>yw~FseaptqA97hA~A+=@6(~DQ@y2A0C z>qJ)TU=BaZAlN#NWJmaP=YYkP$_B(meEbM=140*unsC|mC#!iGzMk}bp#$`SE;xyr zT6_vEb@~PE4K|-9N+!oQqaLc;4MCkgPMz8*v`YkKwjef+t`W3+r7mChC`n8xU$+HW zN-k4o=_p$oXK?cITy*o5v>TgGx}&@{ohB?LN5FS))rD)GtBJRGIUM@PSy`3K!>?`7 z@)(HznJKeGEyG3kqsQ56Z&TL0t;ECzaZG1UQ)xYSvq-sRr2GM)syX7e5=JT4?l(9{ zpL$FDJr2rTM$6&U_2MMg;#5vobyP6B&#FVlii1~T>5@M^2}9^O%?Jr2+GX%|qE<0~^hE*>#atJp0W`>YW=zceFD}0g(YczTy=%RYf@P!Yv#B}r!LUoT~ z9k8lp;;r;)r#-(1X}3!41A+ydJNPl#)a<+8cnw}e>9X%`T+?fF8?PM<-|6aJDX%2w z`chEI+@Q$2Pa2R+&3@_gsF$jyt^dc1;OUCks@1Z(9I(Wo-o+ZA>r(7G7uh0@hmDvp12>`jI3dn z54bH8s2J{gJ9Ke|FH)9L%3Y?~ji9F5sAzN&;7T!p2x~Ad(?1WTCSxtXP35Uly1rzVOT1nGa2H( zY9iL$IAuPg_D89)jE0bt`6rt(n;vf%I8gJ>^!2fZ%X65A5UfD^)`UB+XBm z!6Q$)C`$xOTnC0cNeg#7>1PEMJ6J-{=J>i(E@eVVlg+f843KsC#{t{ZR*&v7qumN6jZRDSE6c);Dv9M@SZ zan0bTaWDIYFKd68MbGEcmipT3ahBq2wS2YrwbSwubC9A3MZMs>2YG_wF?mCeV#HX@ zdxF=`1ZNEzSFV#)ss#LA-v#I2)CKxv@As;p@wO`8}EUp zt~@!*#l*5(?J_!Tm;ZsoqVnP0yQAYdvv1#uKDPgGw`kTZ*6dlu*_!fFuZ+xAv5Xtn z?VGh3+rQf4VtTXJH!Dx;;&hJ+UyqM2rD-{<`aXMba1fQTQ&bdP(Idmt&0l1|O6vG< z=+$<Qizw8vTXFNE6Y^v@_HOZp>=30GC0;B~s3!NaVmn37z_WP+pJ&G`3~W!# z8Y}ycXf7^1Jy|rX^X+uLQr@hNb%y!9_E6IE#Yzv5Ab9nuJA-q#>+jHA+wA9W5uYI8 z@&1&DOTBwF?jEKMvDW`>Q>0My(zVCg3v68miBz#)%-1nu0Z>@pvYQfu3Uxc-8D&Pn zkb5U-++?>Ya0v8WxFKS#Z8$iec-$k{`Q;J%gxca_B`MI_<=_`eA8r`I<9j}WyA#OB zx%ys*l4j0PhmwZQMTe4d_6b8+`yPdo#?L)%xYE3y*Knm{eX8L~*xdRR^kztFg=Dvn z>>KACulwcQ(tRexzaHs6*Ly%4`0WGQaJRI%Ikz--3z8!Jqr%@x9HUa{Ly{`o&O^nZ z!Nz{p6_0bQ`0v&3)Oc!!7E`hWc@SPETHD;Yzn;~H^>CCHnLY&*PJUD%i5JUlV~g-v zjjF#a0=t)(yGS<546=iKQ7eoydn<%gMCpxOgIfxZ={W>1T2emMip8sX_@$*cgszDs-c0+02Bxr*%y!cqV1I#Evf=KH*5&$8{#$y+mb6lP}%Ov9?j z9@3hnn7OyGv}#1X?}+>E;EFV&f95on>qF|Qw~f;GQZV8RI_}V9bjxv5;99PkQzC_C znHZnyiF}>3_IX!xdX8LH%h{BQ>=U9Y`5d%4?1oO1aD;qMSV8#>oj1_pfnjE&gpvm> zst+JNmb)n`YN*{;BrPa=mhMClr$6&x+Wg?e6-T|OPhY2|6B2amGJibvcgcBuOp?B2 zuVFbMtcJBN>l-GoOB0WqOCa$05tO?k&(h6G?mSo=8X?JS(N&oa^^Q&FmT6!YUQ>xp zEW5I_x#<*i&d(tdGf3`BNuaPwE}ws+Y+f?Y29GprZ98wy&G&iI2tKWObiZuQI|7{e$YRUCtRr zB#)38$fy;Y@N5nJnTeRkpx#n z43ljk{Vc^~^-u{d-=;sMQ*{@Ntvx_RnIX=Vu9TL~Gp*5b&?l_4(33piqu(H5;bj|# zG+X;H0+K{fkmZdeoUZiew7EmuF=J0Zem#$E+^sZn{KHBfs{4^gMt{AEpaNWyA@zqS%vwH%r1-J<)%J7R&)%x;;i5*kvx@^F8fGAGN#uUZnV0pa(UoESM_bJ zkk&i01G=Ydjn1t~qnS2)6zw@jeRnb@d1A*>`Ox>a+QYtBX6*GG2Y*=B%AkLKx5vZ$ zbn+WrKX=WD6LmYC|-*@N;l=6W{Aurl=msrab5bF zbU$?@aL@4t_S<~nTw3CtWx~R@?_P81eal@s=QHn`$%K6F>uq z7edg>>hGxP1t+` zf=3^{Okc33YYeLt%--!U6#VQ_M3~acO#IUM_D=6kddeNjFw?|je`uwtk@fA=c!Rqi zW=`-MVSk)`)A#1;^DY}JBdgn|UGnmAU!>5NCOd7OR6E$|wr*rB-;5inFOn4%foc%+ z6JK3@bjPYwORgNb7gc~wRBgIBx=K?o5a8e}Wi1h(mU!Rbn-_~>p zx~vboyX>$w*E6k(?=j8W-+SQj^!u6f(mJ*gH^>7d@AcU5GOw1y*Sspx_{S?r-X!J0 zvSVj&4!MZ7sBdDW@3vp6ATyYnzwNJ5Civ1p`hCXKQ|2F(I*BrjS&&;eM#X6DM>;Lu z2`7z=jnCic(79c5G=V%JbcQ>o?V~oXgmv)<*e@wJKaqdEFFq#)H4Bwr1fuL!i4#}vZ*8s^z&I%*QeFHNHdJ6&9{l!(u^Uc z7yCP(c5c*?X|h!s}xalr;&3TD{}RvBPINZD3|%Vdpcs zyVrZ|eL2cc-=_T1e(zE{nwoXP6n)8ep=z%&_0^rr11F@ECQHCUP$m1aiK~h8`>nOk zlkPtTIz+~GXE&8R;d_;z*53E(t-j8>krKj_lQ&VG)TQ=nCTklWBk7pCEEXhJM7Fc8 zWEs9Ib#aUKhn$39czq&`!voo}W+vTprT;%)-@D>(_nq>bo!|d7DYCTM{FQ(I5y3L@ zzkgbNmD;v87dxX;^jjEmjvFHJC%s4ltrRo2&aEFqcfPClpSj=j?g<4p@v4ZJ(fLn1 zll8nZVIn%-oU4U8-g4E|w9K}7&S=-G?QLre)Jr7w;Kl@@$iQ=r361-PR}JrBm%!AD z@$>%R9~Y@m^!S|X%X;2%_dhHdcxMU>U%oRzR#dVp*61ZQS}ahN!Li^fP^E3MV8LG% zD<8--Lb|7ZRj}vWk2LB`z4GR#N3xVTUr_++E`t=yO3DMdv5b#u+d!@ z-iNTUadz$Md7PnzMMHHSY@|r)8(u3>bo9&1;5XO3$M3&AZy4Dd`a!`)u69U7Klo!w z+4Bc{WzUMhvGar1YGIMEE^Mcl{llrZbiR>4hHDb1MHlTdJX@EhMQr5wI4@}V=7FAj zc~!xB-}e%iu|nG~!|K+k=lq-vkNK*!I`4~e8d@te?sNQA z)qL-`AqZYoPC5Se6zkA*8y##Y#NAuNH#k`OhrM(r%rh8K? zx8o6VE&kP4TgV0(cRYT)TSfcT15Y;3}+Nul9$@|qgWK=yv8xGZLGYCB}l2~CG5-IM)k^~ zZ~f9_Q46CKHqB{nThp^K{O#T(|692675g0poO+{AT?$7FU;Tt!^X}Y_ckxj+<*#!VJ>nE8# z4~1ygqjgzlKdqXH23S>O4spyo><9Nm@5gA)Ji8W|u0ysQA_TvYA&C4q63~z&2o>{G zzI$U+sq@v79xpkn6@t)iNCCLq_Frz|;D5V`JG^7o@WX4F;DO6G;%&7P0=TXv-fXJ? zzkgg+ixa^BzwhwWFenVxgm|O*7h1tt8tRHg_=9Y~I%;Y}RE9H15|BASRQ$#w{Kc*b z0TF>7#=u~Qy_SZK9!TKAS6=?GeF1?7?gi0*wf{2nFBMui2#Dy=PaS_)OC0#Ou|F@? zC8Q4!0tSZ;8WV3~i5Lg*0}#Ofb_*GNQ$?4|h$W&+>dr~?7+a2Gj72m#mzBeBc?~~Q zF)0}0^vX*`1YlI>E!6k#oviR;ow}d2c%<;}VH?OI(Jn3Ecs`@65^sP^o zNHSf+H?sKiS*b(QHyGVjwYWUrHPcV_)_0`4s_V82rK?*Lr_&6WE*|GBUTYTI z52tg4FP~LAwR8p)f3;yPy<=V|A)hATM``H$R-Lm-D>jQ{1bxhTaD!wEb7YI%o6UYbf$az|+>4{by) zdfc+|Or&F2p3ptA8w@IS!7lvql3$SLTB457#$?I#_NBGHx67rtJO-+Fh!Sfxjj@ZH z4hehU+wF+AylRMTz|`;D>U+=?67sA)j5N86;YZ1itNq>{$wpro^(-VQ>a`}89V_(e zlzvBX|J|~y(YATYDP9|5ppXdFe3|og=CvuL>1s8JS9MuJL)0y<-pUZ98My9@h+*%s zs$kO-Q`tym`BqGJyyfxKQIi@fZ~D33rN`QgYg%^J*IuL{W4^ZrapjTVH&wnx+pZo- zNpL)sVQ8v5B4s#xu5X}Gj#udP`7gP?)Q`^Ws&Ncgtu)sl9+lOoxJMmjyw87=$m3Yp zMp__OhT2|xF^SVcf(oD96jbjZr7hAr!K7-(+Ted`r$x8>)EVX{^vQ4f`h`2!D36K{ zH}yQ<{mf0Wv;FCX!bs|eF#o2m_SUDNYulNxcfZtcN!G3OaPRMWj@8W=Zad`cmWR+X z={_Qi#s#qipXX9$cs_pbB-r~~r>nDE<16E{<`H6b(*r{aKp^_%qO?z2GQK>Q9CNRH zO!H*9tK^g^l_INw-$gS!OEs1AVUFh)qB_g;36&=O_&%z)R+`*tYM#m$6;5>D;@0RW zMUijEx{aZ8-oNonXuXR_d&ZXDb;8fYr!5K;&Xy>5U6@A;pXBv8uu{XIJ^W$P)WZ8? zA7$|rWI7XU%EeYQ`nQs5B5~Tu*HiVcS=M3RO3V*&)!dcJtfnSk<=4B^i2E*y+i2Zh zrH4E(na!ZuGjr=|`nulPil9eg3I%r;np~!!gRMsPhU)w$G_Hz7tOne0r6gu;*0{xX z;CcJ&)5u=VYCZ+>OzX`Tz3nOSgkTQBX&T{1KG}BZfwxBd)1S8MVD0xVN=|K8saXhr zW#1RPzcOuf43ia=jpB;Vj?HRu)+P+G7;nVQp8H^0c}z%DRQP<^84r?~TX!SN3iUaaE&cxhW%`;UYO{wF-hf`PcPeebRA~mgD|qQQg;0N?yT5 z>H1FubS0>P7;ak|v#`@h70KbbALcA&2KnRsh9Z&OY3$hG?ReVPhgGXXQs`+6Pt*6ZdFI6Y8mAo2BgN>6Mss7mYFAEuQ zvH87n{9ed#2OA=WKwQX(ue$Eez^X%B_JGapk6j0VEd8lK4S;MBF?T|MCLDmt6B8E~ z1AtM)&6U^#K%>-wO&27jE-L|%kb*!ZA>uL+DJh8c0gpb$`M-AmIp)7^b#R%3t?tkT zeIy>?jKCv^Bmae;wA9!817#zx;I)A2L-f7XkZ$hU z0a&C-fPtw~fTt7OnO8|s-cQ!g%i9ak4)XItp>eW)3cLs+P*E0mCz8RupaT}Xrvfj) zDe8-L2X=H`MR}~Vi>$G_=1(!8rNHZk$9v0y!M?t}V!o1M7_2K;91e$rArfE-2~mJU z6z7k|Bm6|sIKH0>egOr6ID&`@5snxFUV#@F^S~Hqr@xeX6R@ZQmCjCJ^ySnI8}KcKt2k{YNzZ zW(v>&m?8;q0+ILfmi<{?rWg!L@y`mA2miD8H#?G8Qi{ZK6NNxUB_XEbGO`dUS)k_r zkUC^K5CV$O-NpZZ5&DCPC!ifwJ~d@pn~qwRY9AkS4e)C>$90cUGbg07VCl!z0j6$p3@zAFMxxjREAFJ8_1q zp%6HnA^^X{03IGH{zsoY;Jhq=fc}XiR0M#~^2C7rNjvoOkAnZ{IWUKSx4)*L;_qn; zjIY3p1t#ggEpz_{uvP;W2o%PZxJDf0?)Q<++#TtQ#9qK6T>uCm5D?s7=Wlg)EO1~a z&Ofl8#P5Uruk{8v)crcC5uuZR$RTmSvF#_y85r=e7dXZd5t;{w|AQ~E9#8`yAtYM( z&qdY`FoXs;wL@u$Aj-oBK;J?op&%E!Lz*~55(YqPi4O?4&(uwB#SQ;IRk*f(&3u4>0v6?g2<*1cBHaV=%z3_Um6_-~;^m!9I3y k!q!m-*$Dl&xg!kv?_CG`A~1ol_=9|ji_1tz9Ku8YAJ%r);{X5v literal 0 HcmV?d00001 diff --git a/src/HottBook/Chapter2.typ b/src/HottBook/Chapter2.typ new file mode 100644 index 0000000..cf92f13 --- /dev/null +++ b/src/HottBook/Chapter2.typ @@ -0,0 +1,59 @@ +#import "@preview/cetz:0.2.2" +#set page(width: auto, height: auto, margin: .5cm) + +#let data = ( + ([Belgium], 24), + ([Germany], 31), + ([Greece], 18), + ([Spain], 21), + ([France], 23), + ([Hungary], 18), + ([Netherlands], 27), + ([Romania], 17), + ([Finland], 26), + ([Turkey], 13), +) + +#cetz.canvas({ + import cetz.chart + import cetz.draw: * + + // let colors = gradient.linear(red, blue, green, yellow) + + // chart.piechart( + // data, + // value-key: 1, + // label-key: 0, + // radius: 4, + // slice-style: colors, + // inner-radius: 1, + // outset: 3, + // inner-label: (content: (value, label) => [#text(white, str(value))], radius: 110%), + // outer-label: (content: "%", radius: 110%)) + + let point(p, name) = { + content((p.at(0)-0.1, p.at(1)+0.1), name) + circle(p, radius: 0.05, fill: black) + } + + circle((2, 1), radius: (1, 1), fill: gray, stroke: none) + circle((2, 3), radius: (1, 0.75), fill: gray, stroke: none) + + let a = (1.6, 3) + let b = (2.4, 3) + + let fa = (1.6, 1.5) + let fb = (2.4, 1.5) + let ga = (1.3, 0.5) + let gb = (2.7, 0.5) + + point(a, "a") + point(b, "b") + point(fa, "f(a)") + point(fb, "f(b)") + point(ga, "g(a)") + point(gb, "g(b)") + + line(a, fa) + +}) \ No newline at end of file diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md index 341d88e..9b31abe 100644 --- a/src/HottBook/Chapter2Exercises.lagda.md +++ b/src/HottBook/Chapter2Exercises.lagda.md @@ -4,7 +4,6 @@ module HottBook.Chapter2Exercises where open import Agda.Primitive open import HottBook.Chapter1 open import HottBook.Chapter2 -open import HottBook.Chapter2Lemma221 open import HottBook.Util ``` diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index 7292f4b..88deb69 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/src/HottBook/Chapter3.lagda.md @@ -5,7 +5,6 @@ open import Agda.Primitive open import HottBook.Chapter1 open import HottBook.Chapter1Util open import HottBook.Chapter2 -open import HottBook.Chapter2Lemma221 open import HottBook.Chapter3Definition331 open import HottBook.Chapter3Lemma333 open import HottBook.Util diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md index 280eb94..06a3e7d 100644 --- a/src/HottBook/Chapter6.lagda.md +++ b/src/HottBook/Chapter6.lagda.md @@ -3,7 +3,6 @@ module HottBook.Chapter6 where open import HottBook.Chapter1 open import HottBook.Chapter2 -open import HottBook.Chapter2Lemma221 ``` # 6 Higher inductive types diff --git a/src/MayConcise/Chapter1.lagda.md b/src/MayConcise/Chapter1.lagda.md index 085e298..a4661fd 100644 --- a/src/MayConcise/Chapter1.lagda.md +++ b/src/MayConcise/Chapter1.lagda.md @@ -29,5 +29,4 @@ https://en.wikipedia.org/wiki/Homomorphism ## 4 Homotopy invariance ``` -_⋆ ``` \ No newline at end of file