diff --git a/Cubical/Algebra/Group/MorphismProperties.agda b/Cubical/Algebra/Group/MorphismProperties.agda index bc5f285f7d..3bf92551e9 100644 --- a/Cubical/Algebra/Group/MorphismProperties.agda +++ b/Cubical/Algebra/Group/MorphismProperties.agda @@ -310,3 +310,18 @@ BijectionIso→GroupIso {G = G} {H = H} i = grIso BijectionIsoToGroupEquiv : BijectionIso G H → GroupEquiv G H BijectionIsoToGroupEquiv i = GroupIso→GroupEquiv (BijectionIso→GroupIso i) + +Aut[_] : Group ℓ → Group ℓ +Aut[ Ĝ@(G , Gstr) ] = + makeGroup {G = GroupIso Ĝ Ĝ} + idGroupIso compGroupIso + invGroupIso (isSetΣ (isSet-SetsIso (is-set Gstr) (is-set Gstr)) (λ _ → isProp→isSet (isPropIsGroupHom _ _))) + (λ _ _ _ → GroupIso≡ (i≡ refl)) + (λ _ → GroupIso≡ (i≡ refl)) + (λ _ → GroupIso≡ (i≡ refl)) + (λ (x , _) → GroupIso≡ (i≡ (funExt (Iso.leftInv x)))) + (λ (x , _) → GroupIso≡ (i≡ (funExt (Iso.rightInv x)))) + where + open GroupStr Gstr + + i≡ = SetsIso≡fun (is-set Gstr) (is-set Gstr) diff --git a/Cubical/Algebra/Ring/Properties.agda b/Cubical/Algebra/Ring/Properties.agda index afe940f880..f3bb310188 100644 --- a/Cubical/Algebra/Ring/Properties.agda +++ b/Cubical/Algebra/Ring/Properties.agda @@ -90,6 +90,13 @@ module RingTheory (R' : Ring ℓ) where (0r · x) + (0r · x) ∎ in +Idempotency→0 _ 0·x-is-idempotent + + 0RightAnnihilates' : (x y : R) → y ≡ 0r → x · y ≡ 0r + 0RightAnnihilates' x y p = cong (x ·_) p ∙ 0RightAnnihilates x + + 0LeftAnnihilates' : (x y : R) → x ≡ 0r → x · y ≡ 0r + 0LeftAnnihilates' x y p = cong (_· y) p ∙ 0LeftAnnihilates y + -DistR· : (x y : R) → x · (- y) ≡ - (x · y) -DistR· x y = implicitInverse (x · y) (x · (- y)) @@ -152,6 +159,42 @@ module RingTheory (R' : Ring ℓ) where ·-assoc2 : (x y z w : R) → (x · y) · (z · w) ≡ x · (y · z) · w ·-assoc2 x y z w = ·Assoc (x · y) z w ∙ congL _·_ (sym (·Assoc x y z)) + +IdR' : ∀ x y → y ≡ 0r → x + y ≡ x + +IdR' x y y=0 = cong (x +_) y=0 ∙ +IdR x + + +IdL' : ∀ x y → x ≡ 0r → x + y ≡ y + +IdL' x y x=0 = cong (_+ y) x=0 ∙ +IdL y + + +InvL' : ∀ x y → x ≡ y → - x + y ≡ 0r + +InvL' x y x=y = cong (- x +_) (sym x=y) ∙ (+InvL x) + + +InvR' : ∀ x y → x ≡ y → x + - y ≡ 0r + +InvR' x y x=y = cong (_+ - y) x=y ∙ (+InvR y) + + plusMinus : ∀ x y → (x + y) - y ≡ x + plusMinus x y = sym (+Assoc _ _ _) ∙ +IdR' _ _ (+InvR y) + + plusMinus' : ∀ x y y' → y ≡ y' → (x + y) - y' ≡ x + plusMinus' x y y' p = sym (+Assoc _ _ _) ∙ +IdR' _ _ (+InvR' y y' p) + + minusPlus : ∀ x y → (x - y) + y ≡ x + minusPlus x y = sym (+Assoc _ _ _) ∙ +IdR' _ _ (+InvL y) + + minusPlus' : ∀ x y y' → y ≡ y' → (x - y) + y' ≡ x + minusPlus' x y y' p = sym (+Assoc _ _ _) ∙ +IdR' _ _ (+InvL' y y' p) + + ·IdR' : ∀ x y → y ≡ 1r → x · y ≡ x + ·IdR' x y y=0 = cong (x ·_) y=0 ∙ ·IdR x + + ·IdL' : ∀ x y → x ≡ 1r → x · y ≡ y + ·IdL' x y x=0 = cong (_· y) x=0 ∙ ·IdL y + + ·DistR- : (x y z : R) → x · (y - z) ≡ (x · y) - (x · z) + ·DistR- _ _ _ = ·DistR+ _ _ _ ∙ cong (_ +_) (-DistR· _ _) + + ·DistL- : (x y z : R) → (x - y) · z ≡ (x · z) - (y · z) + ·DistL- _ _ _ = ·DistL+ _ _ _ ∙ cong (_ +_) (-DistL· _ _) + Ring→Semiring : Ring ℓ → Semiring ℓ Ring→Semiring R = let open RingStr (snd R) diff --git a/Cubical/Data/Fin/Properties.agda b/Cubical/Data/Fin/Properties.agda index dda477bf43..87ea9a5cd5 100644 --- a/Cubical/Data/Fin/Properties.agda +++ b/Cubical/Data/Fin/Properties.agda @@ -16,7 +16,7 @@ open import Cubical.HITs.PropositionalTruncation renaming (rec to ∥∥rec) open import Cubical.Data.Fin.Base as Fin open import Cubical.Data.Nat -open import Cubical.Data.Nat.Order +open import Cubical.Data.Nat.Order hiding (<-·sk-cancel) open import Cubical.Data.Empty as Empty open import Cubical.Data.Unit open import Cubical.Data.Sum diff --git a/Cubical/Data/Int/Base.agda b/Cubical/Data/Int/Base.agda index 0576b0f241..22fdd45573 100644 --- a/Cubical/Data/Int/Base.agda +++ b/Cubical/Data/Int/Base.agda @@ -6,7 +6,7 @@ module Cubical.Data.Int.Base where open import Cubical.Foundations.Prelude open import Cubical.Data.Bool -open import Cubical.Data.Nat hiding (_+_ ; _·_) renaming (isEven to isEvenℕ ; isOdd to isOddℕ) +open import Cubical.Data.Nat as ℕ hiding (_+_ ; _·_) renaming (isEven to isEvenℕ ; isOdd to isOddℕ) open import Cubical.Data.Fin.Inductive.Base infix 8 -_ @@ -60,6 +60,13 @@ _+_ : ℤ → ℤ → ℤ m + pos n = m +pos n m + negsuc n = m +negsuc n +_+f_ : ℤ → ℤ → ℤ +pos n +f pos n₁ = pos (n ℕ.+ n₁) +negsuc n +f negsuc n₁ = negsuc (suc (n ℕ.+ n₁)) +n +f m = n + m +-- pos n +f negsuc n₁ = {!!} +-- negsuc n +f pos n₁ = {!!} + -_ : ℤ → ℤ - pos zero = pos zero - pos (suc n) = negsuc n @@ -74,6 +81,16 @@ pos (suc n) · m = m + pos n · m negsuc zero · m = - m negsuc (suc n) · m = - m + negsuc n · m +_·f_ : ℤ → ℤ → ℤ +pos n ·f pos n₁ = pos (n ℕ.· n₁) +pos zero ·f negsuc n₁ = pos zero +pos (suc n) ·f negsuc n₁ = negsuc (suc n ℕ.· suc n₁) +negsuc n ·f pos zero = pos zero +negsuc n ·f pos (suc n₁) = negsuc (suc n ℕ.· suc n₁) +negsuc n ·f negsuc n₁ = pos (suc n ℕ.· suc n₁) + + + -- Natural number and negative integer literals for ℤ open import Cubical.Data.Nat.Literals public diff --git a/Cubical/Data/Int/Order.agda b/Cubical/Data/Int/Order.agda index fac79698da..0422ce48bb 100644 --- a/Cubical/Data/Int/Order.agda +++ b/Cubical/Data/Int/Order.agda @@ -4,11 +4,12 @@ module Cubical.Data.Int.Order where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Function - +open import Cubical.Foundations.Equiv open import Cubical.Data.Empty as ⊥ using (⊥) open import Cubical.Data.Int.Base as ℤ open import Cubical.Data.Int.Properties as ℤ open import Cubical.Data.Nat as ℕ +import Cubical.Data.Nat.Order as ℕ open import Cubical.Data.NatPlusOne.Base as ℕ₊₁ open import Cubical.Data.Sigma @@ -498,3 +499,59 @@ negsuc zero ≟ negsuc zero = eq refl negsuc zero ≟ negsuc (suc n) = gt (negsuc-≤-negsuc zero-≤pos) negsuc (suc m) ≟ negsuc zero = lt (negsuc-≤-negsuc zero-≤pos) negsuc (suc m) ≟ negsuc (suc n) = Trichotomy-pred (negsuc m ≟ negsuc n) + +0<_ : ℤ → Type +0< pos zero = ⊥ +0< pos (suc n) = Unit +0< negsuc n = ⊥ + +isProp0< : ∀ n → isProp (0< n) +isProp0< (pos (suc _)) _ _ = refl + +·0< : ∀ m n → 0< m → 0< n → 0< (m ℤ.· n) +·0< (pos (suc m)) (pos (suc n)) _ _ = + subst (0<_) (pos+ (suc n) (m ℕ.· (suc n)) ∙ cong (pos (suc n) ℤ.+_) (pos·pos m (suc n))) _ + +0<·ℕ₊₁ : ∀ m n → 0< (m ℤ.· pos (ℕ₊₁→ℕ n)) → 0< m +0<·ℕ₊₁ (pos (suc m)) n x = _ +0<·ℕ₊₁ (negsuc n₁) (1+ n) x = + ⊥.rec (subst 0<_ (negsuc·pos n₁ (suc n) + ∙ congS -_ (cong (pos (suc n) ℤ.+_) + (sym (pos·pos n₁ (suc n))) ∙ + sym (pos+ (suc n) (n₁ ℕ.· suc n)))) x) + ++0< : ∀ m n → 0< m → 0< n → 0< (m ℤ.+ n) ++0< (pos (suc m)) (pos (suc n)) _ _ = + subst (0<_) (cong sucℤ (pos+ (suc m) n)) _ + +0<→ℕ₊₁ : ∀ n → 0< n → Σ ℕ₊₁ λ m → n ≡ pos (ℕ₊₁→ℕ m) +0<→ℕ₊₁ (pos (suc n)) x = (1+ n) , refl + +min-0< : ∀ m n → 0< m → 0< n → 0< (ℤ.min m n) +min-0< (pos (suc zero)) (pos (suc n)) x x₁ = tt +min-0< (pos (suc (suc n₁))) (pos (suc zero)) x x₁ = tt +min-0< (pos (suc (suc n₁))) (pos (suc (suc n))) x x₁ = + +0< (sucℤ (ℤ.min (pos n₁) (pos n))) 1 (min-0< (pos (suc n₁)) (pos (suc n)) _ _) _ + +ℕ≤→pos-≤-pos : ∀ m n → m ℕ.≤ n → pos m ≤ pos n +ℕ≤→pos-≤-pos m n (k , p) = k , sym (pos+ m k) ∙∙ cong pos (ℕ.+-comm m k) ∙∙ cong pos p + +ℕ≥→negsuc-≤-negsuc : ∀ m n → m ℕ.≤ n → negsuc n ≤ negsuc m +ℕ≥→negsuc-≤-negsuc m n = negsuc-≤-negsuc ∘ ℕ≤→pos-≤-pos m n + +pos-≤-pos→ℕ≤ : ∀ m n → pos m ≤ pos n → m ℕ.≤ n +pos-≤-pos→ℕ≤ m n (k , p) = k , injPos ((pos+ k m ∙ ℤ.+Comm (pos k) (pos m)) ∙ p) + +pos-≤-pos≃ℕ≤ : ∀ m n → (pos m ≤ pos n) ≃ (m ℕ.≤ n) +pos-≤-pos≃ℕ≤ m n = propBiimpl→Equiv isProp≤ ℕ.isProp≤ + (pos-≤-pos→ℕ≤ _ _) (ℕ≤→pos-≤-pos _ _) + +pos-<-pos≃ℕ< : ∀ m n → (pos m < pos n) ≃ (m ℕ.< n) +pos-<-pos≃ℕ< m n = propBiimpl→Equiv (isProp< {pos m} {pos n}) ℕ.isProp≤ + (pos-≤-pos→ℕ≤ _ _) (ℕ≤→pos-≤-pos (suc m) n) + + +0≤x² : ∀ n → 0 ≤ n ℤ.· n +0≤x² (pos n) = subst (0 ≤_) (pos·pos n n) zero-≤pos +0≤x² (negsuc n) = subst (0 ≤_) (pos·pos (suc n) (suc n) + ∙ sym (negsuc·negsuc n n)) zero-≤pos diff --git a/Cubical/Data/Int/Properties.agda b/Cubical/Data/Int/Properties.agda index 1fc854cafa..81582a24ab 100644 --- a/Cubical/Data/Int/Properties.agda +++ b/Cubical/Data/Int/Properties.agda @@ -1,6 +1,7 @@ -{-# OPTIONS --safe #-} +{-# OPTIONS --safe --v=tc.conv:20 #-} module Cubical.Data.Int.Properties where + open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function open import Cubical.Foundations.Isomorphism @@ -11,7 +12,7 @@ open import Cubical.Relation.Nullary open import Cubical.Data.Empty as ⊥ open import Cubical.Data.Bool -open import Cubical.Data.Nat +open import Cubical.Data.Nat as ℕ hiding (+-assoc ; +-comm ; min ; max ; minComm ; maxComm) renaming (_·_ to _·ℕ_; _+_ to _+ℕ_ ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm ; isEven to isEvenℕ ; isOdd to isOddℕ) @@ -1505,3 +1506,42 @@ sumFinℤ0 n = sumFinGen0 _+_ 0 (λ _ → refl) n (λ _ → 0) λ _ → refl sumFinℤHom : {n : ℕ} (f g : Fin n → ℤ) → sumFinℤ {n = n} (λ x → f x + g x) ≡ sumFinℤ {n = n} f + sumFinℤ {n = n} g sumFinℤHom {n = n} = sumFinGenHom _+_ 0 (λ _ → refl) +Comm +Assoc n + +abs-max : ∀ n → pos (abs n) ≡ max n (- n) +abs-max (pos zero) = refl +abs-max (pos (suc n)) = refl +abs-max (negsuc n) = refl + +min-pos-pos : ∀ m n → min (pos m) (pos n) ≡ pos (ℕ.min m n) +min-pos-pos zero n = refl +min-pos-pos (suc m) zero = refl +min-pos-pos (suc m) (suc n) = cong sucℤ (min-pos-pos m n) + +max-pos-pos : ∀ m n → max (pos m) (pos n) ≡ pos (ℕ.max m n) +max-pos-pos zero n = refl +max-pos-pos (suc m) zero = refl +max-pos-pos (suc m) (suc n) = cong sucℤ (max-pos-pos m n) + + +sign : ℤ → ℤ +sign (pos zero) = 0 +sign (pos (suc n)) = 1 +sign (negsuc n) = -1 + +sign·abs : ∀ m → sign m · pos (abs m) ≡ m +sign·abs (pos zero) = refl +sign·abs (pos (suc n)) = refl +sign·abs (negsuc n) = refl + +-- abs[sign[m]·pos[n]]≡n : ∀ m n → abs (sign m · pos n) ≡ n +-- abs[sign[m]·pos[n]]≡n m n = {!!} + + +-- ·'≡· : ∀ n m → n · m ≡ n ·' m +-- ·'≡· (pos n) (pos n₁) = sym (pos·pos n n₁) +-- ·'≡· (pos zero) (negsuc n₁) = refl +-- ·'≡· (pos (suc n)) (negsuc n₁) = {!!} +-- ·'≡· (negsuc n) (pos zero) = ·AnnihilR (negsuc n) +-- ·'≡· (negsuc n) (pos (suc n₁)) = negsuc·pos n (suc n₁) ∙ +-- {!!} +-- ·'≡· (negsuc n) (negsuc n₁) = negsuc·negsuc n n₁ ∙ sym (pos·pos (suc n) (suc n₁)) diff --git a/Cubical/Data/Nat/Mod.agda b/Cubical/Data/Nat/Mod.agda index 8911504e25..1d53e66990 100644 --- a/Cubical/Data/Nat/Mod.agda +++ b/Cubical/Data/Nat/Mod.agda @@ -4,7 +4,8 @@ module Cubical.Data.Nat.Mod where open import Cubical.Foundations.Prelude open import Cubical.Data.Nat open import Cubical.Data.Nat.Order -open import Cubical.Data.Empty +open import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Sum as ⊎ -- Defining x mod 0 to be 0. This way all the theorems below are true -- for n : ℕ instead of n : ℕ₊₁. @@ -36,6 +37,9 @@ mod< n = , cong (λ x → fst ind + suc x) (modIndStep n x) ∙ snd ind +<→mod : (n x : ℕ) → x < (suc n) → x mod (suc n) ≡ x +<→mod = modIndBase + mod-rUnit : (n x : ℕ) → x mod n ≡ ((x + n) mod n) mod-rUnit zero x = refl mod-rUnit (suc n) x = @@ -153,6 +157,7 @@ mod-lCancel n x y = ∙∙ mod-rCancel n y x ∙∙ cong (_mod n) (+-comm y (x mod n)) + -- remainder and quotient after division by n -- Again, allowing for 0-division to get nicer syntax remainder_/_ : (x n : ℕ) → ℕ @@ -192,3 +197,117 @@ private test₁ : ((11 + (10 mod 3)) mod 3) ≡ 0 test₁ = refl + + + +·mod : ∀ k n m → (k · n) mod (k · m) + ≡ k · (n mod m) +·mod zero n m = refl +·mod (suc k) n zero = cong ((n + k · n) mod_) (sym (0≡m·0 (suc k))) + ∙ 0≡m·0 (suc k) +·mod (suc k) n (suc m) = ·mod' n n ≤-refl (splitℕ-≤ (suc m) n) + + where + ·mod' : ∀ N n → n ≤ N → ((suc m) ≤ n) ⊎ (n < suc m) → + ((suc k · n) mod (suc k · suc m)) ≡ suc k · (n mod suc m) + ·mod' _ zero x _ = cong (modInd (m + k · suc m)) (sym (0≡m·0 (suc k))) + ∙ 0≡m·0 (suc k) + ·mod' zero (suc n) x _ = ⊥.rec (¬-<-zero x) + ·mod' (suc N) n@(suc n') x (inl (m' , p)) = + let z = ·mod' N m' (≤-trans (m + , +-comm m m' ∙ injSuc (sym (+-suc m' m) ∙ p)) + (pred-≤-pred x)) (splitℕ-≤ _ _) ∙ cong ((suc k) ·_) + (sym (modIndStep m m') ∙ + cong (_mod (suc m)) (+-comm (suc m) m' ∙ p)) + in (cong (λ y → ((suc k · y) mod (suc k · suc m))) (sym p) + ∙ cong {x = (m' + suc m + k · (m' + suc m))} + {suc (m + k · suc m + (m' + k · m'))} + (modInd (m + k · suc m)) + (cong (_+ k · (m' + suc m)) (+-suc m' m ∙ cong suc (+-comm m' m)) + ∙ cong suc + (sym (+-assoc m m' _) + ∙∙ cong (m +_) + (((cong (m' +_) (sym (·-distribˡ k _ _) + ∙ +-comm (k · m') _) ∙ +-assoc m' (k · suc m) (k · m')) + ∙ cong (_+ k · m') (+-comm m' _)) + ∙ sym (+-assoc (k · suc m) m' (k · m')) ) + ∙∙ +-assoc m _ _)) + ∙ modIndStep (m + k · suc m) (m' + k · m')) ∙ z + ·mod' (suc N) n x (inr x₁) = + modIndBase _ _ ( + subst2 _<_ (·-comm n (suc k)) (·-comm _ (suc k)) + (<-·sk {n} {suc m} {k = k} x₁) ) + ∙ cong ((suc k) ·_) (sym (modIndBase _ _ x₁)) + +2≤x→10 zero (suc l) r = ⊥.rec (¬-<-zero r) n∸l>0 (suc n) zero r = suc-≤-suc zero-≤ n∸l>0 (suc n) (suc l) r = n∸l>0 n l (pred-≤-pred r) +[n-m]+m : ∀ m n → m ≤ n → (n ∸ m) + m ≡ n +[n-m]+m zero n _ = +-zero n +[n-m]+m (suc m) zero p = ⊥.rec (¬-<-zero p) +[n-m]+m (suc m) (suc n) p = + +-suc _ _ ∙ cong suc ([n-m]+m m n (pred-≤-pred p)) + -- automation ≤-solver-type : (m n : ℕ) → Trichotomy m n → Type @@ -545,3 +577,126 @@ pattern s_ + + private ·CommR : (a b c : ℤ) → a ℤ.· b ℤ.· c ≡ a ℤ.· c ℤ.· b ·CommR a b c = sym (ℤ.·Assoc a b c) ∙ cong (a ℤ.·_) (ℤ.·Comm b c) ∙ ℤ.·Assoc a c b @@ -164,6 +168,19 @@ data Trichotomy (m n : ℚ) : Type₀ where eq : m ≡ n → Trichotomy m n gt : m > n → Trichotomy m n +record TrichotomyRec {ℓ : Level} (n : ℚ) (P : ℚ → Type ℓ) : Type ℓ where + no-eta-equality + field + lt-case : ∀ m → (p : m < n) → P m + eq-case : P n + gt-case : ∀ m → (p : m > n) → P m + + go : ∀ m → (t : Trichotomy m n) → P m + go m (lt p) = lt-case m p + go m (eq p) = subst P (sym p) eq-case + go m (gt p) = gt-case m p + + module _ where open BinaryRelation @@ -401,6 +418,7 @@ module _ where b) + + +isIncrasingℙ : (P : ℙ ℚ) → (∀ x → x ∈ P → ℚ) → Type₀ +isIncrasingℙ P f = ∀ x x∈ y y∈ → x ℚ.< y → f x x∈ ℚ.< f y y∈ + +isNondecrasingℙ : (P : ℙ ℚ) → (∀ x → x ∈ P → ℚ) → Type₀ +isNondecrasingℙ P f = ∀ x x∈ y y∈ → x ℚ.≤ y → f x x∈ ℚ.≤ f y y∈ + +isIncrasingℙ→injective : (P : ℙ ℚ) → (f : ∀ x → x ∈ P → ℚ) → + isIncrasingℙ P f → + ∀ x x∈ x' x'∈ + → f x x∈ ≡ f x' x'∈ → x ≡ x' +isIncrasingℙ→injective P f incrF x x∈ x' x'∈ = + ⊎.rec const (⊎.rec (w x x∈ x' x'∈) ((sym ∘_) ∘ (_∘ sym) ∘ w x' x'∈ x x∈)) + (ℚ.≡⊎# x x') + + where + w : ∀ x x∈ x' x'∈ → x ℚ.< x' → f x x∈ ≡ f x' x'∈ → x ≡ x' + w x x∈ x' x'∈ x : ∀ x → ⟨ openPred (λ y → (y <ᵣ x) , isProp<ᵣ _ _) ⟩ +openPred> x y = + PT.map (map-snd (λ {q} q 0 x) + + + +·invℝ' : ∀ r 0 : ℝ → ℙ ℝ +pred> x y = (x <ᵣ y) , isProp<ᵣ _ _ + +pred≤< : ℝ → ℝ → ℙ ℝ +pred≤< a b x = ((a ≤ᵣ x) × (x <ᵣ b)) , isProp× (isProp≤ᵣ _ _) (isProp<ᵣ _ _) + +pred<≤ : ℝ → ℝ → ℙ ℝ +pred<≤ a b x = ((a <ᵣ x) × (x ≤ᵣ b)) , isProp× (isProp<ᵣ _ _) (isProp≤ᵣ _ _) diff --git a/Cubical/HITs/CauchyReals/Sequence.agda b/Cubical/HITs/CauchyReals/Sequence.agda new file mode 100644 index 0000000000..73840e0540 --- /dev/null +++ b/Cubical/HITs/CauchyReals/Sequence.agda @@ -0,0 +1,1471 @@ +{-# OPTIONS --safe --lossy-unification #-} + +module Cubical.HITs.CauchyReals.Sequence where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Function +open import Cubical.Foundations.Transport +open import Cubical.Foundations.Structure +open import Cubical.Foundations.Powerset + +import Cubical.Functions.Logic as L + + +open import Cubical.Data.Bool as 𝟚 hiding (_≤_) +open import Cubical.Data.Nat as ℕ hiding (_·_;_+_) +import Cubical.Data.Nat.Mod as ℕ +import Cubical.Data.Nat.Order as ℕ +open import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Sum as ⊎ +open import Cubical.Data.Int as ℤ using (pos) +import Cubical.Data.Int.Order as ℤ +open import Cubical.Data.Sigma + +open import Cubical.HITs.PropositionalTruncation as PT + +open import Cubical.Data.NatPlusOne + +open import Cubical.Data.Rationals as ℚ using (ℚ ; [_/_]) +open import Cubical.Data.Rationals.Order as ℚ using + ( _ℚ₊+_ ; 0<_ ; ℚ₊ ; _ℚ₊·_ ; ℚ₊≡) +open import Cubical.Data.Rationals.Order.Properties as ℚ + using (invℚ₊;/2₊;/3₊;/4₊;x/2