diff --git a/1FundamentalGroup/Preambles/PEmpty.agda b/1FundamentalGroup/Preambles/PEmpty.agda new file mode 100644 index 0000000..1323bf0 --- /dev/null +++ b/1FundamentalGroup/Preambles/PEmpty.agda @@ -0,0 +1,6 @@ +module 1FundamentalGroup.Preambles.PEmpty where + +open import Cubical.Foundations.Prelude public +open import Cubical.Data.Empty renaming (rec to ⊥Rec) public +open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public + diff --git a/1FundamentalGroup/Preambles/PTrueNotFalse.agda b/1FundamentalGroup/Preambles/PTrueNotFalse.agda new file mode 100644 index 0000000..c2e38b9 --- /dev/null +++ b/1FundamentalGroup/Preambles/PTrueNotFalse.agda @@ -0,0 +1,6 @@ +module 1FundamentalGroup.Preambles.PTrueNotFalse where + +open import Cubical.Data.Empty public +open import Cubical.Data.Unit renaming ( Unit to ⊤ ) public +open import Cubical.Data.Bool using (Bool ; true ; false) public +open import Cubical.Foundations.Prelude public diff --git a/1FundamentalGroup/Quest0.agda b/1FundamentalGroup/Quest0.agda index dbdf318..b804318 100644 --- a/1FundamentalGroup/Quest0.agda +++ b/1FundamentalGroup/Quest0.agda @@ -1,5 +1,6 @@ +-- ignore this module 1FundamentalGroup.Quest0 where - +-- ignore this open import 1FundamentalGroup.Preambles.P0 Refl : base ≡ base diff --git a/1FundamentalGroup/Quest0SideQuests/Empty.agda b/1FundamentalGroup/Quest0SideQuests/Empty.agda index 0d70498..2bcb98c 100644 --- a/1FundamentalGroup/Quest0SideQuests/Empty.agda +++ b/1FundamentalGroup/Quest0SideQuests/Empty.agda @@ -1,13 +1,10 @@ module 1FundamentalGroup.Quest0SideQuests.Empty where -open import Cubical.Foundations.Prelude -open import Cubical.Data.Empty renaming (rec to ⊥Rec) -open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) +open import 1FundamentalGroup.Preambles.PEmpty toEmpty : (A : Type) → Type toEmpty A = {!!} --- why Type₁ pathEmpty : (A : Type) → Type₁ pathEmpty A = {!!} @@ -15,10 +12,10 @@ isoEmpty : (A : Type) → Type isoEmpty A = {!!} toEmpty→isoEmpty : (A : Type) → toEmpty A → isoEmpty A -toEmpty→isoEmpty A f = {!!} +toEmpty→isoEmpty A = {!!} isoEmpty→pathEmpty : (A : Type) → isoEmpty A → pathEmpty A isoEmpty→pathEmpty A = {!!} pathEmpty→toEmpty : (A : Type) → pathEmpty A → toEmpty A -pathEmpty→toEmpty A p = {!!} +pathEmpty→toEmpty A = {!!} diff --git a/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agda b/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agda index 0b3df63..901dce0 100644 --- a/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agda +++ b/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agda @@ -1,13 +1,10 @@ module 1FundamentalGroup.Quest0SideQuests.EmptySolutions where -open import Cubical.Foundations.Prelude -open import Cubical.Data.Empty renaming (rec to ⊥Rec) -open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) +open import 1FundamentalGroup.Preambles.PEmpty toEmpty : (A : Type) → Type toEmpty A = A → ⊥ --- why Type₁ pathEmpty : (A : Type) → Type₁ pathEmpty A = A ≡ ⊥ @@ -27,4 +24,4 @@ isoEmpty→pathEmpty : (A : Type) → isoEmpty A → pathEmpty A isoEmpty→pathEmpty A = isoToPath pathEmpty→toEmpty : (A : Type) → pathEmpty A → toEmpty A -pathEmpty→toEmpty A p = J (λ B q → toEmpty B) (λ x → x) (sym p) +pathEmpty→toEmpty A p x = transport p x diff --git a/1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agda b/1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agda index 7e8ede4..41aa677 100644 --- a/1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agda +++ b/1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agda @@ -1,9 +1,6 @@ module 1FundamentalGroup.Quest0SideQuests.TrueNotFalse where -open import Cubical.Data.Empty -open import Cubical.Data.Unit renaming ( Unit to ⊤ ) -open import Cubical.Data.Bool using (Bool ; true ; false) -open import Cubical.Foundations.Prelude +open import 1FundamentalGroup.Preambles.PTrueNotFalse true≢false : true ≡ false → ⊥ true≢false = {!!} diff --git a/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agda b/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agda index 16149ff..f6bc6f7 100644 --- a/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agda +++ b/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agda @@ -1,9 +1,6 @@ module 1FundamentalGroup.Quest0SideQuests.TrueNotFalseSolutions where -open import Cubical.Data.Empty -open import Cubical.Data.Unit renaming ( Unit to ⊤ ) -open import Cubical.Data.Bool using (Bool ; true ; false) -open import Cubical.Foundations.Prelude +open import 1FundamentalGroup.Preambles.PTrueNotFalse true≢false : true ≡ false → ⊥ true≢false h = transport ⊤≡⊥ tt where diff --git a/1FundamentalGroup/Quest1.agda b/1FundamentalGroup/Quest1.agda index 830a598..08001fe 100644 --- a/1FundamentalGroup/Quest1.agda +++ b/1FundamentalGroup/Quest1.agda @@ -1,5 +1,6 @@ +-- ignore module 1FundamentalGroup.Quest1 where - +-- ignore open import 1FundamentalGroup.Preambles.P1 Ω : (A : Type) (a : A) → Type diff --git a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.agdai b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.agdai index 6cd0f16..5af2140 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Preambles/PEmpty.agdai b/_build/2.6.2/agda/1FundamentalGroup/Preambles/PEmpty.agdai new file mode 100644 index 0000000..bb8c0ba Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Preambles/PEmpty.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Preambles/PTrueNotFalse.agdai b/_build/2.6.2/agda/1FundamentalGroup/Preambles/PTrueNotFalse.agdai new file mode 100644 index 0000000..d38ed4c Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Preambles/PTrueNotFalse.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agdai index 16b8695..6983ed0 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agdai index f91a74e..89b5938 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai index cc09bdd..0fb5cc8 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai differ