-- ignore module 1FundamentalGroup.Quest2 where open import 1FundamentalGroup.Preambles.P2 isSet→LoopSpace≡⊤ : {A : Type} (x : A) → isSet A → (x ≡ x) ≡ ⊤ isSet→LoopSpace≡⊤ = {!!} data _⊔_ (A B : Type) : Type where inl : A → A ⊔ B inr : B → A ⊔ B {- Your definition of ℤ≡ℕ⊔ℕ goes here. Your definition of ⊔NoConfusion goes here. Your definition of Path≡⊔NoConfusion goes here. Your definition of isSet⊔NoConfusion goes here. Your definition of isSet⊔ goes here. Your definition of isSetℤ goes here. -}