whitespace

Author: marcinjangrzybowski

Cubical/Data/Rationals/Fast/Order.agda

@@ -992,14 +992,14 @@ module EqElims where
  lrhsDom [ℚ₊] = ℚ₊
 
 
- lrhsDomFst : ℚTypes → Type 
+ lrhsDomFst : ℚTypes → Type
  lrhsDomFst [ℚ] = ℤ
  lrhsDomFst [ℚ₊] = ℕ
- 
+
  lrhsCtr : ∀ b → lrhsDomFst b → ℕ → (lrhsDom b)
  lrhsCtr [ℚ] k m = [ k , 1+ m ]
  lrhsCtr [ℚ₊] n m = [ ℤ.pos (suc n) , (1+ m) ] , _
- 
+
  LRhs : ℚSignature → Type
  LRhs [] = ℚ × ℚ
  LRhs (x ∷ xs) = lrhsDom x → LRhs xs
@@ -1011,20 +1011,20 @@ module EqElims where
 
  EqType : ∀ s → LRhs s → Type
  EqType [] (lhs , rhs) = lhs ≡ rhs
- EqType (x ∷ xs) lrhs = (q : lrhsDom x) → EqType xs (lrhs q) 
+ EqType (x ∷ xs) lrhs = (q : lrhsDom x) → EqType xs (lrhs q)
 
  isPropEqType : ∀ s → (lrhs : LRhs s) → isProp (EqType s lrhs)
  isPropEqType [] lrhs = isSetℚ _ _
  isPropEqType (_ ∷ s) lrhs = isPropΠ $ isPropEqType s ∘ lrhs
- 
+
  EllimEqₛ : ∀ s → (lrhs : LRhs s) → LemType s lrhs → EqType s lrhs
  EllimEqₛ [] lrhs e = e
  EllimEqₛ ([ℚ] ∷ xs) lrhs e = ElimProp.go w
   where
   w : ElimProp _
   w .ElimProp.isPropB = isPropEqType xs ∘ lrhs
   w .ElimProp.f (k , 1+ m) = EllimEqₛ xs (lrhs _) (e k m)
-  
+
  EllimEqₛ ([ℚ₊] ∷ xs) lrhs e = uncurry (ElimProp.go w)
   where
   w : ElimProp (λ z → ∀ p → EqType xs (lrhs (z , p)))

Cubical/Data/Rationals/Fast/Order/Properties.agda

@@ -726,7 +726,7 @@ invℚ₊-invol x = ℚ!
 
 
 x·invℚ₊[x] : ∀ x → fst x · fst (invℚ₊ x) ≡ 1
-x·invℚ₊[x] x = ℚ! 
+x·invℚ₊[x] x = ℚ!
 
 invℚ₊[x]·x : ∀ x →  fst (invℚ₊ x) · fst x ≡ 1
 invℚ₊[x]·x x = ℚ!
@@ -1608,7 +1608,7 @@ lowerBoundℕ⁻¹ q =
 <Δ : ∀ n → [ 1 / 4 ] < ([ pos (suc n) / 1 ])
 <Δ n = 1/n<sucK 3 (1+ n)
 
-  
+
 clam∈ℚintervalℙ : ∀ a b → (a ≤ b) → ∀ x → clamp a b x ∈ ℚintervalℙ a b
 clam∈ℚintervalℙ a b a≤b x = ≤clamp _ _ _ a≤b , (clamp≤ a _ x)
 

Cubical/Data/Rationals/Fast/Properties.agda

@@ -695,7 +695,7 @@ x+x≡2x x = cong₂ _+_
 -- eqElim₂Ty : (lrhs : ℚ → ℚ → ℚ × ℚ) → Type
 -- eqElim₂Ty lrhs = (∀ {k m k' m'} → fst (lrhs [ (k , 1+ m) ] [ (k' , 1+ m') ])
 --         ≡  snd (lrhs [ (k , 1+ m) ] [ (k' , 1+ m') ]))
-        
+
 -- eqElim₃Ty : (lrhs : ℚ → ℚ → ℚ → ℚ × ℚ) → Type
 -- eqElim₃Ty lrhs = (∀ {k m k' m' k'' m''} → fst (lrhs [ (k , 1+ m) ] [ (k' , 1+ m') ] [ (k'' , 1+ m'') ])
 --         ≡  snd (lrhs [ (k , 1+ m) ] [ (k' , 1+ m') ] [ (k'' , 1+ m'') ]))
@@ -754,7 +754,7 @@ x+x≡2x x = cong₂ _+_
 --   w .SetQuotient.ElimProp4.isPropB _ _ _ _ = isSetℚ _ _
 --   w .SetQuotient.ElimProp4.f (n , (1+ n₁)) (m , (1+ m₁)) (m' , (1+ m₁')) (m'' , (1+ m₁'')) =
 --    p {n} {n₁} {m} {m₁} {m'} {m₁'} {m''} {m₁''}
-   
+
 
 -- eqElim₅ : (lrhs : ℚ → ℚ → ℚ → ℚ → ℚ → ℚ × ℚ) → eqElim₅Ty lrhs
 --     → ∀ (x y z z' z'' : ℚ) → fst (lrhs x y z z' z'') ≡ (snd (lrhs x y z z' z''))
@@ -777,4 +777,4 @@ x+x≡2x x = cong₂ _+_
 --   w .SetQuotient.ElimProp6.f (n , (1+ n₁)) (m , (1+ m₁)) (m' , (1+ m₁')) (m'' , (1+ m₁''))
 --    (m''' , (1+ m₁''')) (m'''' , (1+ m₁'''')) =
 --    p {n} {n₁} {m} {m₁} {m'} {m₁'} {m''} {m₁''} {m'''} {m₁'''} {m''''} {m₁''''}
-   
+

Cubical/HITs/CauchyReals/Continuous.agda

@@ -393,7 +393,7 @@ opaque
  unfolding maxᵣ
 
  ≤lim : ∀ r x y → (∀ δ → rat r ≤ᵣ x δ) → rat r ≤ᵣ lim x y
- ≤lim r x y p = ≡→≤ᵣ $ 
+ ≤lim r x y p = ≡→≤ᵣ $
    snd (NonExpanding₂.β-rat-lim' maxR r x y) ∙
         congLim _ _ _ _ (≤ᵣ→≡ ∘ p)
 
@@ -521,7 +521,7 @@ opaque
              (ℚ.<Weaken≤ _ _ (ℚ.x/2<x (ε))) )
       in zz))
         , ≤ℚ→≤ᵣ _ _ (ℚ.≤+ℚ₊ r r (/2₊ ε) (ℚ.isRefl≤ r)) ∣₁
-  w .Elimℝ-Prop.limA x y R ε = 
+  w .Elimℝ-Prop.limA x y R ε =
     let z = 𝕣-lim-dist x y (/4₊ ε)
     in PT.map (λ (q , z , z') →
          let (_ , Xzz' , Xzz) = from-abs< _ _ _
@@ -534,7 +534,7 @@ opaque
          in q ℚ.+ fst (/2₊ ε) ℚ.+ fst (/2₊ (/4₊ ε))  ,
                let zzz = (≤ᵣ-+o _ _ (rat (fst (/2₊ ε) ℚ.+ fst (/2₊ (/4₊ ε))))
                        (≤ᵣMonotone+ᵣ _ _ _ _ z zz))
-                   
+
                in subst2 _≤ᵣ_
                      (cong (_+ᵣ rat (fst (/2₊ ε) ℚ.+ fst (/2₊ (/4₊ ε))))
                       (sym (+ᵣAssoc (rat q) _ _)) ∙
@@ -543,7 +543,7 @@ opaque
                         (+ᵣComm _ _ ∙ +ᵣ-rat _ _ ∙ cong rat ℚ!!)
                          (cong₂ _+ᵣ_ refl (+ᵣComm _ _) ∙ +ᵣAssoc _ _ _  ∙
                           cong₂ _+ᵣ_ (+ᵣComm _ _ ∙ +-ᵣ _) refl ∙ +IdL _))
-                   
+
                      (_∙_ {x = rat (fst (/2₊ (/4₊ ε))) +ᵣ rat (fst (/4₊ ε)) +ᵣ
                                 rat (fst (/2₊ ε) ℚ.+ fst (/2₊ (/4₊ ε)))}
                                  {y = rat
@@ -560,7 +560,7 @@ opaque
                        cong (_+ᵣ (lim x y)) (+-ᵣ _) ∙ +IdL _)
                      (≤ᵣMonotone+ᵣ _ _ _ _ z' zz'))
                      (isTrans≡≤ᵣ _ _ _ (+ᵣ-rat _  _) $ ≤ℚ→≤ᵣ _ _
-                       
+
                        (subst (q ℚ.+ fst (/4₊ ε) ℚ.≤_)
                          ((ℚ.+Assoc q _ _))
                           (ℚ.≤-o+ _ _ q distℚ≤!
@@ -693,7 +693,7 @@ opaque
   Δ = ℚ.<→ℚ₊ m n m<n
 
 opaque
- unfolding _<ᵣ_ 
+ unfolding _<ᵣ_
  <ᵣ-+o : ∀ m n o →  m <ᵣ n → (m +ᵣ o) <ᵣ (n +ᵣ o)
  <ᵣ-+o m n o = PT.rec (isProp<ᵣ (m +ᵣ o) _)
    λ ((q , q') , x , x' , x'') →
@@ -874,14 +874,14 @@ opaque
 
 opaque
  unfolding _≤ᵣ_
- 
+
  ≤min-lem : ∀ x y y' → x ≤ᵣ y → x ≤ᵣ y' →  x ≤ᵣ minᵣ y y'
  ≤min-lem x y y' p p' =
     minDistMaxᵣ x y y' ∙ cong₂ minᵣ p p'
 
 
 opaque
- unfolding _<ᵣ_ 
+ unfolding _<ᵣ_
 
 
  <min-lem : ∀ x x' y → y <ᵣ x → y <ᵣ x' →  y <ᵣ minᵣ x x'
@@ -1140,7 +1140,7 @@ opaque
  --                 ≤ᵣ f₁ (rat u) (≤ℚ→≤ᵣ _ _ x₀<u) )
  --              → ∀ x x₀≤x → f₀ x x₀≤x ≤ᵣ f₁ x x₀≤x
  -- ≤ContPos'pred {x₀} {f₀} {f₁} f₀C f₁C X x 0≤x =
- --   subst (λ (x , x₀≤x) → f₀ x ?  ≤ᵣ f₁ x ?) -- ? x₀≤x 
+ --   subst (λ (x , x₀≤x) → f₀ x ?  ≤ᵣ f₁ x ?) -- ? x₀≤x
  --      (Σ≡Prop (λ _ → isSetℝ _ _) ?) -- ?
  --     (≤Cont
  --       (IsContinuousWithPred∘IsContinuous _ _ _
@@ -1502,4 +1502,3 @@ sym-intervalℙ⊆ointervalℙ : ∀ a b → a <ᵣ b →
 sym-intervalℙ⊆ointervalℙ a b a<b =
  intervalℙ⊆ointervalℙ _ _ _ _ (-ᵣ<ᵣ _ _ a<b) a<b
 
-

Cubical/HITs/CauchyReals/LiftingExpr.agda

@@ -34,21 +34,21 @@ record _isLiftOf_ (fℝ : ℝ → ℝ) (fℚ : ℚ → ℚ) : Type where
  constructor inj
  field
   prf : ∀ q → rat (fℚ q) ≡ fℝ (rat q)
-  
-record LiftedTo (fℝ : ℝ → ℝ) : Type where 
+
+record LiftedTo (fℝ : ℝ → ℝ) : Type where
  constructor inj
  field
   fℚ : _
   prf : fℝ isLiftOf fℚ
-  
+
  open _isLiftOf_ prf
- 
-record LiftedFrom (fℚ : ℚ → ℚ) : Type where 
+
+record LiftedFrom (fℚ : ℚ → ℚ) : Type where
  constructor inj
  field
   fℝ : _
   prf : fℝ isLiftOf fℚ
-  
+
  open _isLiftOf_ prf
 
 record _isLiftOf₂_ (fℝ : ℝ → ℝ → ℝ) (fℚ : ℚ → ℚ → ℚ) : Type where
@@ -58,15 +58,15 @@ record _isLiftOf₂_ (fℝ : ℝ → ℝ → ℝ) (fℚ : ℚ → ℚ → ℚ) :
 
 
 
-record LiftedTo₂ (fℝ : ℝ → ℝ → ℝ) : Type where 
+record LiftedTo₂ (fℝ : ℝ → ℝ → ℝ) : Type where
  constructor inj
  field
   fℚ : _
   prf : fℝ isLiftOf₂ fℚ
 
  open _isLiftOf₂_ prf
- 
-record LiftedFrom₂ (fℚ : ℚ → ℚ → ℚ) : Type where 
+
+record LiftedFrom₂ (fℚ : ℚ → ℚ → ℚ) : Type where
  constructor inj
  field
   fℝ : _
@@ -94,7 +94,7 @@ instance
 
 
 data ℚExpr : Type where
- 𝕢[_] : ℚ → ℚExpr 
+ 𝕢[_] : ℚ → ℚExpr
  _$𝕢[_] : ∀ fℚ → ⦃ lf : LiftedFrom fℚ ⦄ → ℚExpr → ℚExpr
  _$𝕢₂[_,_] : ∀ fℚ → ⦃ lf : LiftedFrom₂ fℚ ⦄ → ℚExpr → ℚExpr → ℚExpr
 
@@ -103,9 +103,9 @@ evalℚExpr (𝕢[ x ]) = x
 evalℚExpr (fℚ $𝕢[ x ]) = fℚ (evalℚExpr x)
 evalℚExpr (fℚ $𝕢₂[ x , x₁ ]) = fℚ (evalℚExpr x) (evalℚExpr x₁)
 
-module ℝExpr (ratFlag : Type) where 
+module ℝExpr (ratFlag : Type) where
  data ℝExpr : Type where
-  ratE : {ratFlag} → ℚExpr →  ℝExpr 
+  ratE : {ratFlag} → ℚExpr →  ℝExpr
   𝕣[_] : ℝ → ℝExpr
   _$𝕣[_] : ∀ fℝ → ⦃ lt : LiftedTo fℝ ⦄ → ℝExpr → ℝExpr
   _$𝕣₂[_,_] : ∀ fℝ → ⦃ lt : LiftedTo₂ fℝ ⦄ → ℝExpr → ℝExpr → ℝExpr
@@ -127,7 +127,7 @@ open ℝExpr hiding (ℝExpr) public
 ℚExpr→ℝExpr : ℚExpr → ℝExpr
 ℚExpr→ℝExpr 𝕢[ x ] = 𝕣[ rat x ]
 ℚExpr→ℝExpr (_$𝕢[_] fℚ ⦃ inj fℝ prf ⦄ x) = _$𝕣[_] fℝ ⦃ inj _ prf ⦄ (ℚExpr→ℝExpr x)
-ℚExpr→ℝExpr (_$𝕢₂[_,_] fℚ ⦃ inj fℝ prf ⦄ x x₁) = 
+ℚExpr→ℝExpr (_$𝕢₂[_,_] fℚ ⦃ inj fℝ prf ⦄ x x₁) =
  _$𝕣₂[_,_] fℝ ⦃ inj _ prf ⦄ (ℚExpr→ℝExpr x) (ℚExpr→ℝExpr x₁)
 
 ℚℝExpr→ℝExpr : ℚℝExpr → ℝExpr
@@ -154,7 +154,7 @@ evalℚℝExpr 𝕣[ x ] = x
 evalℚℝExpr (fℝ $𝕣[ x ]) = fℝ (evalℚℝExpr x)
 evalℚℝExpr (fℝ $𝕣₂[ x , x₁ ]) = fℝ (evalℚℝExpr x) (evalℚℝExpr x₁)
 evalℚℝExpr (rat-path q i) = rat q
-evalℚℝExpr (lift-path ⦃ lo = lo ⦄ {q} i) = _isLiftOf_.prf lo (evalℚExpr q) i 
+evalℚℝExpr (lift-path ⦃ lo = lo ⦄ {q} i) = _isLiftOf_.prf lo (evalℚExpr q) i
 evalℚℝExpr (lift-path₂ ⦃ lo = lo ⦄ {q} {q'} i) =
   _isLiftOf₂_.prf lo (evalℚExpr q) (evalℚExpr q') i
 evalℚℝExpr (isSetℝExpr x x₁ x₂ y i i₁) =
@@ -163,11 +163,11 @@ evalℚℝExpr (isSetℝExpr x x₁ x₂ y i i₁) =
 
 evalCohRat : ∀ e → rat (evalℚExpr e) ≡ evalℚℝExpr (ℚExpr→ℝExpr e)
 evalCohRat 𝕢[ x ] = refl
-evalCohRat (_$𝕢[_] fℚ ⦃ inj fℝ (inj prf) ⦄ e) = 
-   prf (evalℚExpr e) 
+evalCohRat (_$𝕢[_] fℚ ⦃ inj fℝ (inj prf) ⦄ e) =
+   prf (evalℚExpr e)
    ∙ cong fℝ (evalCohRat e)
 evalCohRat (_$𝕢₂[_,_] fℚ ⦃ inj fℝ (inj prf) ⦄ e e₁) =
-  prf (evalℚExpr e) (evalℚExpr e₁)  
+  prf (evalℚExpr e) (evalℚExpr e₁)
    ∙ cong₂ fℝ (evalCohRat e) (evalCohRat e₁)
 
 evalCoh : ∀ e → evalℚℝExpr e ≡ evalℚℝExpr (ℚℝExpr→ℝExpr e)
@@ -182,7 +182,7 @@ evalCoh (lift-path {fℝ} {fℚ} ⦃ lo = inj prf ⦄ {q} i) j =
     (λ j → fℝ (evalCohRat q j))
     (prf (evalℚExpr q))
     refl
-    i j 
+    i j
 
 evalCoh (lift-path₂ {fℝ} {fℚ} ⦃ lo = inj prf ⦄ {q} {q'} i) j =
    isSet→isSet' isSetℝ
@@ -191,7 +191,7 @@ evalCoh (lift-path₂ {fℝ} {fℚ} ⦃ lo = inj prf ⦄ {q} {q'} i) j =
    (λ j → fℝ (evalCohRat q j) (evalCohRat q' j))
    (prf (evalℚExpr q) (evalℚExpr q'))
    refl
-   i j 
+   i j
 
 evalCoh (isSetℝExpr e e₁ x y i i₁) j =
   isGroupoid→isGroupoid' (isSet→isGroupoid isSetℝ)
@@ -216,13 +216,13 @@ private
  ifHasInstanceℚ₂ nm = runSpeculative $ (_, false) <$> (do
   (meta m _) ← checkType
      unknown (def (quote _isLiftOf₂_) (unknown v∷ v[ (def nm []) ]))
-   where _ → typeError [ "imposible in liftingExpr macro!" ]ₑ  
+   where _ → typeError [ "imposible in liftingExpr macro!" ]ₑ
   [] ← getInstances m
    where (x ∷ _) → pure true
    -- ((solveInstanceConstraints >> pure true) <|> pure false)
-      
+
   pure false)
-  
+
  toExprℚ : Term → TC Term
  toExprℚ (def nm v[ q ]) = do
    e ← toExprℚ q
@@ -235,7 +235,7 @@ private
     then (pure (con (quote _$𝕢₂[_,_]) ((def nm []) v∷ e v∷ v[ e' ])))
     else (pure (con (quote 𝕢[_]) (v[ tm ])))
  toExprℚ tm = pure (con (quote 𝕢[_]) (v[ tm ]))
- 
+
 -- _$𝕣[_] fℝ ⦃ inj fℚ (inj prf) ⦄ (ℚExpr→ℝExpr q)
  toExprℝ : Term → TC Term
  toExprℝ (def nm v[ r ]) = do
@@ -250,7 +250,7 @@ private
    e ← toExprℚ q
    pure (con (quote ratE) (v[ e ]))
  toExprℝ tm = pure (con (quote 𝕣[_]) (v[ tm ]))
- 
+
  quoteℚℝ : Term → TC Term
  quoteℚℝ tm' = do
   tm ← checkType tm' (def (quote ℝ) [])
@@ -266,7 +266,7 @@ private
  ℚℝ!-macro hole = wrdℚ $
    do
      goal ← inferType hole >>= normalise
-    
+
 
      wait-for-type goal
      just (lhs , rhs) ← get-boundary goal
@@ -280,14 +280,14 @@ private
      let solution =
            def (quote _∙_)
             (def (quote evalCoh) v[ lhsE ] v∷ v[
-             def (quote evalCoh') v[ rhsE ] ])   
+             def (quote evalCoh') v[ rhsE ] ])
      unify hole solution
 
  ℚℝ!↘-macro : Term → TC Unit
  ℚℝ!↘-macro hole = wrdℚ $
    do
      goal ← inferType hole >>= normalise
-    
+
 
      wait-for-type goal
      just lhs ← get-boundaryLHS goal
@@ -296,7 +296,7 @@ private
            → typeError(strErr "The ℚℝ↘ failed to parse the goal "
                               ∷ termErr goal ∷ [])
      lhsE ← quoteℚℝ lhs
-     let solution = def (quote evalCoh) v[ lhsE ]   
+     let solution = def (quote evalCoh) v[ lhsE ]
      unify hole solution