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 0000000..6578bbb Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai differ