diff --git a/1FundamentalGroup/Quest0.agda b/1FundamentalGroup/Quest0.agda index b804318..5936e14 100644 --- a/1FundamentalGroup/Quest0.agda +++ b/1FundamentalGroup/Quest0.agda @@ -1,8 +1,8 @@ --- ignore this +-- ignore module 1FundamentalGroup.Quest0 where --- ignore this open import 1FundamentalGroup.Preambles.P0 + Refl : base ≡ base Refl = {!!} diff --git a/1FundamentalGroup/Quest1.agda b/1FundamentalGroup/Quest1.agda index 08001fe..4ab21d0 100644 --- a/1FundamentalGroup/Quest1.agda +++ b/1FundamentalGroup/Quest1.agda @@ -1,8 +1,8 @@ -- ignore module 1FundamentalGroup.Quest1 where --- ignore open import 1FundamentalGroup.Preambles.P1 + Ω : (A : Type) (a : A) → Type Ω A a = a ≡ a diff --git a/1FundamentalGroup/Quest2.agda b/1FundamentalGroup/Quest2.agda index 73d4b85..b6adab1 100644 --- a/1FundamentalGroup/Quest2.agda +++ b/1FundamentalGroup/Quest2.agda @@ -1,5 +1,5 @@ +-- ignore module 1FundamentalGroup.Quest2 where - open import 1FundamentalGroup.Preambles.P2 sucℤ : ℤ → ℤ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai index 4f81153..51c632e 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai index 0fb5cc8..a6fac66 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest2.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest2.agdai index f8aaca9..7aefc71 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest2.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest2.agdai differ