whitespace fix

Author: marcinjangrzybowski

Cubical/HITs/CauchyReals.agda

@@ -0,0 +1,12 @@
+{-# OPTIONS --safe #-}
+module Cubical.HITs.CauchyReals where
+
+open import Cubical.HITs.CauchyReals.Base public
+open import Cubical.HITs.CauchyReals.Closeness public
+open import Cubical.HITs.CauchyReals.Lipschitz public
+open import Cubical.HITs.CauchyReals.Order public
+open import Cubical.HITs.CauchyReals.Continuous public
+open import Cubical.HITs.CauchyReals.Multiplication public
+open import Cubical.HITs.CauchyReals.Inverse public
+open import Cubical.HITs.CauchyReals.Sequence public
+open import Cubical.HITs.CauchyReals.Derivative public

Cubical/HITs/CauchyReals/Continuous.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --lossy-unification #-}
+{-# OPTIONS --safe --lossy-unification #-}
 
 module Cubical.HITs.CauchyReals.Continuous where
 

Cubical/HITs/CauchyReals/Derivative.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --lossy-unification #-}
+{-# OPTIONS --safe --lossy-unification #-}
 
 module Cubical.HITs.CauchyReals.Derivative where
 

Cubical/HITs/CauchyReals/Inverse.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --lossy-unification #-}
+{-# OPTIONS --lossy-unification --safe #-}
 
 module Cubical.HITs.CauchyReals.Inverse where
 
@@ -43,7 +43,7 @@ open import Cubical.HITs.CauchyReals.Multiplication
 
 Rℝ = (CR.CommRing→Ring
                (_ , CR.commringstr 0 1 _+ᵣ_ _·ᵣ_ -ᵣ_ IsCommRingℝ))
-
+-- module CRℝ = ?
 
 module 𝐑 = CR.CommRingTheory (_ , CR.commringstr 0 1 _+ᵣ_ _·ᵣ_ -ᵣ_ IsCommRingℝ)
 module 𝐑' = RP.RingTheory Rℝ
@@ -1020,6 +1020,7 @@ sign·absᵣ r = ∘diag $
           ∙ cong rat (cong (ℚ._· ℚ.sign r) (sym (ℚ.abs'≡abs r))
            ∙ ℚ.sign·abs r) ) r
 
+-- HoTT Theorem (11.3.47)
 
 abstract
  invℝ : ∀ r → 0 ＃ r → ℝ

Cubical/HITs/CauchyReals/Lipschitz.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --lossy-unification #-}
+{-# OPTIONS --safe --lossy-unification #-}
 
 module Cubical.HITs.CauchyReals.Lipschitz where
 
@@ -98,6 +98,13 @@ lim-surj = PT.map (map-snd (eqℝ _ _)) ∘ (Elimℝ-Prop.go w)
 
 -- TODO : (Lemma 11.3.11)
 
+-- HoTT-11-3-11 : ∀ {ℓ} (A : Type ℓ) (isSetA : isSet A) →
+--        (f : (Σ[ x ∈  (ℚ₊ → ℝ) ] (∀ ( δ ε : ℚ₊) → x δ ∼[ δ ℚ₊+ ε ] x ε))
+--          → A) →
+--       (∀ u v → uncurry lim u ≡ uncurry lim v → f u ≡ f v)
+--       → ∃![ g ∈ (ℝ → A) ] f ≡ g ∘ uncurry lim
+-- HoTT-11-3-11 A isSetA f p =
+--
 
 Lipschitz-ℚ→ℚ : ℚ₊ → (ℚ → ℚ) → Type
 Lipschitz-ℚ→ℚ L f =

Cubical/HITs/CauchyReals/Multiplication.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --lossy-unification #-}
+{-# OPTIONS --safe --lossy-unification #-}
 
 module Cubical.HITs.CauchyReals.Multiplication where
 
@@ -686,3 +686,20 @@ cont₂·ᵣWP P f g fC gC = IsContinuousWP∘' P _
 _^ⁿ_ : ℝ → ℕ → ℝ
 x ^ⁿ zero = 1
 x ^ⁿ suc n = (x ^ⁿ n) ·ᵣ x
+
+
+·absᵣ : ∀ x y → absᵣ (x ·ᵣ y) ≡ absᵣ x ·ᵣ absᵣ y
+·absᵣ x = ≡Continuous _ _
+  ((IsContinuous∘ _ _  IsContinuousAbsᵣ (IsContinuous·ᵣL x)
+                    ))
+  (IsContinuous∘ _ _ (IsContinuous·ᵣL (absᵣ x))
+                    IsContinuousAbsᵣ)
+  λ y' →
+    ≡Continuous _ _
+  ((IsContinuous∘ _ _  IsContinuousAbsᵣ (IsContinuous·ᵣR (rat y'))
+                    ))
+  (IsContinuous∘ _ _ (IsContinuous·ᵣR (absᵣ (rat y')))
+                    IsContinuousAbsᵣ)
+                     (λ x' →
+                       cong absᵣ (sym (rat·ᵣrat _ _)) ∙∙
+                        cong rat (sym (ℚ.abs'·abs' _ _)) ∙∙ rat·ᵣrat _ _) x

Cubical/HITs/CauchyReals/Order.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --lossy-unification #-}
+{-# OPTIONS --safe --lossy-unification #-}
 
 module Cubical.HITs.CauchyReals.Order where
 

Cubical/HITs/CauchyReals/Sequence.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --lossy-unification #-}
+{-# OPTIONS --safe --lossy-unification #-}
 
 module Cubical.HITs.CauchyReals.Sequence where
 
@@ -42,22 +42,6 @@ open import Cubical.HITs.CauchyReals.Inverse
 
 
 
-·absᵣ : ∀ x y → absᵣ (x ·ᵣ y) ≡ absᵣ x ·ᵣ absᵣ y
-·absᵣ x = ≡Continuous _ _
-  ((IsContinuous∘ _ _  IsContinuousAbsᵣ (IsContinuous·ᵣL x)
-                    ))
-  (IsContinuous∘ _ _ (IsContinuous·ᵣL (absᵣ x))
-                    IsContinuousAbsᵣ)
-  λ y' →
-    ≡Continuous _ _
-  ((IsContinuous∘ _ _  IsContinuousAbsᵣ (IsContinuous·ᵣR (rat y'))
-                    ))
-  (IsContinuous∘ _ _ (IsContinuous·ᵣR (absᵣ (rat y')))
-                    IsContinuousAbsᵣ)
-                     (λ x' →
-                       cong absᵣ (sym (rat·ᵣrat _ _)) ∙∙
-                        cong rat (sym (ℚ.abs'·abs' _ _)) ∙∙ rat·ᵣrat _ _) x
-
 Seq : Type
 Seq = ℕ → ℝ
 
@@ -554,6 +538,7 @@ isCauchyAprox f = (δ ε : ℚ₊) →
 lim' : ∀ x → isCauchyAprox x → ℝ
 lim' x y = lim x λ δ ε  → (invEq (∼≃abs<ε _ _ _)) (y δ ε)
 
+-- HoTT 11.3.49
 
 fromCauchySequence : ∀ s → IsCauchySequence s → ℝ
 fromCauchySequence s ics =
@@ -586,6 +571,9 @@ fromCauchySequence s ics =
                (subst ((fst ε) ℚ.<_) (ℚ.+Comm _ _)
                (ℚ.<+ℚ₊' (fst ε) (fst ε) δ (ℚ.isRefl≤ (fst ε))))))
 
+
+-- TODO HoTT 11.3.50.
+
 fromCauchySequence' : ∀ s → IsCauchySequence' s → ℝ
 fromCauchySequence' s ics =
   lim x y