From 5ff2b6837eda19539fa8ac3e4f213424c410788d Mon Sep 17 00:00:00 2001 From: Jlh18 Date: Sat, 30 Oct 2021 20:56:10 +0100 Subject: [PATCH] added quest 3 --- 1FundamentalGroup/Quest3Solutions.agda | 9 +++++++++ .../agda/1FundamentalGroup/Quest3Solutions.agdai | Bin 0 -> 6233 bytes 2 files changed, 9 insertions(+) create mode 100644 1FundamentalGroup/Quest3Solutions.agda create mode 100644 _build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai diff --git a/1FundamentalGroup/Quest3Solutions.agda b/1FundamentalGroup/Quest3Solutions.agda new file mode 100644 index 0000000..37c92cf --- /dev/null +++ b/1FundamentalGroup/Quest3Solutions.agda @@ -0,0 +1,9 @@ +module 1FundamentalGroup.Quest3Solutions where + +open import Cubical.Foundations.Prelude +open import Cubical.HITs.S1 +open import 1FundamentalGroup.Quest1Solutions + +outOfS¹ : (B : S¹ → Type) → (b : B base) → b ≡ b → (x : S¹) → B x +outOfS¹ B b p base = b +outOfS¹ B b p (loop i) = {!p i!} diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai new file mode 100644 index 0000000000000000000000000000000000000000..6578bbb59d2efbecd73e525840760ff2869764f0 GIT binary patch literal 6233 zcmYjTX;@RqwykrLkRVeC${^EGv9V={q5?8VY~`A6McYnl3=aC_~~8 z7uu+7+!TQe5jdG+MR-t6gnIyqB>@;RKzw7MhdT7I0Srk1j$k1xFeC?I<5@sC#MB2= zD(gW*gw*-F`vi=*lftgltAOA^tf!3}D`={si`4~k7GcO3NtNGg{Sv|;LZBB^x08iB zXslsf?3mcgLInVhHbMXajlZnUfT0c{>Ty-Q0e*-*hIpY6#9$1V2)848Rxf+i4ag?K zWvq*;VU?r`m@-26F1F?3 z#?iXXEYyHX_=pjPWVZrRor)+ID?KCTdWUebEoEUC$wIFy`8`{ca8v?8YiLBk1~4Qu zMM!|aT!;=3JKaS{epl+&A_Sp^yQi8OVSl>;_9{Wq_5aK-a&&8dQ=xIAX$PX1iS-82qp+NV!~|g0c52?1yP>Z z2{kYvTMjp(5*x|6aAc~8Y%PpTAG%Uy3^>Pxa~e_=pga)=GjQN#LYikGw;Vc?WFm}J zj1u7L7Gm{01#YVW1KYBnV03O3tZ_myUWb$Ap^yrVLkK~|yu#EOt}j-s^Pq0zdWv;T zVx2^+Ye4cRCgEtbfj~lG7_%j0Htr1t)=RqtqsW9j8$8)fNRbI^Y( z4f&u}2^RTCQ8^U}t`{H3fx_rwTSBel6@?RGU1*}Vtl37QfS;o z{0YrDiVyXxYOcssmRb3GAnR$avc$o`Fa7Hp(+lu{^{K>ot}Iuq3Oo-W76H2#Tckh0bYN9@ghiD9<@! z6Mig-H=>7vZ%WU=B<&@Mu_@&=mHd@N1Yrv8DY^AWW!{P)ocd~!Ge8vpK5Z*t&=I!W zRuf15;30n?{(z?kSg0=*o1kGlPh1sYjY9G*S<9y-3@k(gBXLQQ%YdH5y;x-(zSU#< zD2W_uh-tZoN+1p~##q1#i!+Gw(dP38=~1M!l~g|Ou_z3& z=RM*@`{q>YWR|G0D}U;wUU{M&>g11r%?^Mqa*##i!cZ3dHPw#>q!j$Ty#nq4#|nk0 zh=ZOOFl3)a$;f608e8NgT?une=IJn)CN*FIP_TH-ISc8LD-=KurSajC27=zjF?Es^ z8I;i2xI2<)dv-gn$}XxiATU#|)NR1GnrktsWTXRb1#mXHhb--N2=JhwyIfG)ZV<8kKdVIe481UnUA7jbeW!snr|3F)~{ zENBq zksyaRDJH_l_|{LA1u;!N}&i{+YW9Xyg zE*c?HmcBp|-}Am9wCiNDES<=iy97h_fkgRn57bZi(uG5ZNnbtMyV*m7EfO<=p;-i> zo*JX#bMmE9HIY8grguR;HiRAplv03WH84XPdJm0u9VN>e6|gE$KMR@FHf6S`f-w%rvOog1Te)qsAe&<*+b8V^)$72|n~9D4R0|b9oA^zc#$AT-zEPghfrtq& zogs*8Mc_^x?@T1ZH6Ihf{*S*PcZEK%YrUl3Anvy;IbF6)D*jHxHwx5%d=1e_b55+~ zo3_p=VH3_c7O%x$26#QFiSQi6wT8IZBQ*^S=34A(fIeCcLETWV?eO`mCom-GES3e+_f0b2_ZVP58f{f)^f`}21bhPJX;6VI?7q9 z-nW#s{Oe^o8JdxZ4j}tbOI%KBx{GqZqwYds&A5vcs3@OjA!Q=7ysX5djMpo)d0Ja{ z?%)++HHq>dX#>yOWYbS`Yh`YDoT!DT&vVl}EIlF$mBvf!M6*1x*7$NG)9#&6h$?UEoCQ2fLns}h9t6O%@U#Yv%ivGg%2IKJo~uOkpZ=Qd9uyWm7cue8 zked=Sw-04hE`oVd_&oQ-(*&QD#-$=xsJ#QMS2lNLmVKu`fhe9evc zRxU4Gh1k7s0SLZbWxJcx6!N=pK)M>7{j`|1yqvv@GP>gHRk@ASiTCXX%8x5Pm^A)5 z{b%6{&t27tpG=wq^EL|ca5}G6$pjsWghT3D%nIr&#SF(B4cDA|eJJbG`sQ_jKe4fS z9YXRom1*SJBkSY_Lk9q0%MHqr%`w(KtZEfNCks`Fg5awXwrzG^EZ7`li7jK#py)ar z>(bEmx%de{<1Y@Zi?Nz*f7haCKXIW$H177N7r@U)H>*G-P3(})&?KV#dSw@h)_e{> ze>BYtWpj*%j97fHMeNGdPgbm_=M>;H{sgxf#p)bsC;OCHd~IZ1-XP-j^FfsL^e%fF z*lf3m%~1}}D?S%)JXD{@#0-}k{_xm-#L^VG z9oMn@yiK2lT#37)M!Dzr;3w`fYk^@;Qk0})Vkg(WhBW>(O8RJ`OK!wvcBhQj#ZJu2 z5rK{q&-kfEUz}WXZdJUh)1_SDtSn9b7AK9K-(DSE9y2%1hMp`r7`s zE-y(56gGfjwKgT8wU2%W@c};i#VLU&4`<0uPm;zOtjo`QT2+oLEGg{Oa7SfUF@hvGP%NwctGnnDP?VY`g6&?s?R@x25LfuzK-$Q$W*{ z#=Q-1%a~c!BtI1wci^vMlN4F%5?1Zmwr7qTYev3?-M>SRkm<~PSOtaK4Lih)aa*GeBxo%uVtQ1q{zZ@=MA1raPDEht8naLO}6@MfIEoH zJvmvOwLVbeilb|$ezfbGI$G$!y=3xT+Q5h z?ZFrln~^^yt&dk^amBOH=GyW0Oc%9hmn?HfflX0)W8Tnn$g{xi-OiCiFn_fxjv1-X zd;e2zkVDOTI16H1zmywHC#Sl+P!kqvIj7GY*#jfoad&mF4HB!aQ+LYIY0r}6RK#EW zCDLy6c3=|{X;8i2x=)>N;o48;XRms-5ATA~c&im0v+M18En&`-e@y;r?Q1DFDWg9Q zPrdyrf0y>542(Lsr>FH7BBOTj`&QsYZF7xmlyaJbQT5B7rM5YrvUUk%foTG#3Sx{K zHkLWXPbb>c>J-QRIWwr;kQT31eER!nGSQ~ye(=Iv>B2X}v&a0B>HL6JFxUOvhUC7V zYn9ttDq5t8Hjf8SdPUS{1H3D$$MJg3j|tI~w$n3R5n)jqbJho*juMx}Q7il9|7zOz z+3&a3TWO7-Z;tI84D^KJQ@cGJWOsFap!YrF;n{MBbstoOXAZX%Fil-U{~GW3__B;? z2i5$1-RfalEB8iZ8<(jplA$_MF|KZmE<)?0q z*Zr;!+XrAD+ZKBS|KnO!^FMDqdv+$owV**>g*G1xJiLz$7Y5(1s|heJxYipjy#HeA zUtZ}WDvkeY8o1@#>#^3MR^iSWUV!|iv^^X)|K<6Cr&Ye3_=k<#`V2xkzORK9SlT3& zn`ysVQa5=waMRL3JS$@)MX*}DYjIt^r;|r{eKC>7p6`>|A1d!nLeX9btDl%tvXEmtNSxZu7ErQ+-Ve+US~Fl%+ED%O=a}{+K(0{nJ?q$%iPM=XbtvyFC7K`xx3} zA-?O9UU8(hir}Ujna&w;5ZHsLo9~T|Dtzy?d%!fw&Ny?5RvdNX-Kuu( zUh}A~GGJiqv7_Dh3T*h?R~^;xY&oH^%hYw_%US7O;^cMN-e3Qq$D?r9;)qR_BTXg# zaR-;+`j_Ay8FlITUe9L*2Tyk7Q#@j!h~Z&EBnoNV1`oX#y+eZgFJj1TwH~fVvm!lU z_h=Vz+n3<(nIna-M-GMlWteR_8e@_`mId8%tF+R=Px=6qFsa$12w#{7*) za^;b#u`dE6ZL>yMfYa4!QybHI$ULyI6ze;8q`SmbUimb*bMfa1j}mp;kb4Jm_tp32 zzaNg5N%I0=?b8RItq&F_PgTFK{`YEQ#NX{&e3h5Jbs8En|4U2JRN%(ZyNz%2&1O&C z0xykb`3i{BIqb++7k3f|91Ya zejqOFKbj0#x?leJ*mY8&_lwus+g&%=9VqL2@M`vf5t37~;2&N+`g%jl*ItEbKc}Se zkuSVn!1ob z_QjexQbX!IRWNq#_^tikg|jysi95C-Y125c$tif0-@d9fbxGXUB!R``I!NNQLR;0h z`eP2Hg4kUV&aUBIr##amkjlQjZhM`@_Xpy<%cgpL_xA_F`|a_YGSj3(Erq1-Zf}RK z78sz@*N2m)!@FDIgTPUXIDhP$f?>)Z8MkJH#wW({q{Gy%3&_pAle92P z$K6u0rUG0I1i=9Ziw65{j!h1;J9e1PIM`WKe?9Xs|JwACJyBHVb+dNgNcaw#dU6Uz s@l_JHy(PxcSSKRaZCks)UDY7*s+uWWcvWRl0FZxkh+HA-bOhjk0ZnD