module 1FundamentalGroup.Quest3 where open import 1FundamentalGroup.Preambles.P3