28 lines
576 B
Agda
28 lines
576 B
Agda
-- 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.
|
||
|
||
-}
|