HIIT Cauchy real

Cubical/Data/PositiveRational/Base.agda

@@ -0,0 +1,22 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.PositiveRational.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Rationals.Base
+open import Cubical.Data.Rationals.Order
+open import Cubical.Data.Rationals.Properties
+
+record ℚ₊ : Type₀ where
+  constructor rat₊
+  field
+    value : ℚ
+    positive : value > 0
+
+open ℚ₊ public
+
+infixl 6 _+₊_
+
+_+₊_ : ℚ₊ → ℚ₊ → ℚ₊
+r +₊ s = rat₊
+           (r .value + s .value)
+           (<Monotone+ 0 (r .value) 0 (s .value) (r .positive) (s .positive))

Cubical/HITs/CauchyReal/Base.agda

@@ -0,0 +1,40 @@
+{-# OPTIONS --safe #-}
+module Cubical.HITs.CauchyReal.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Rationals.Base
+open import Cubical.Data.Rationals.Order
+open import Cubical.Data.Rationals.Properties
+open import Cubical.Data.PositiveRational.Base
+
+-- Higher inductive-inductive construction of Cauchy real, as in the HoTT book.
+
+data ℝ : Type₀
+record Cℝ : Type₀
+data close : ℚ₊ → ℝ → ℝ → Type₀
+syntax close ε x y = x ~[ ε ] y
+
+-- Cauchy real
+data ℝ where
+  rat : ℚ → ℝ
+  lim : ∀ (x : Cℝ) → ℝ
+  eqℝ : ∀ (u v : ℝ) → (∀ ε → u ~[ ε ] v) → u ≡ v
+
+-- Cauchy approximation
+record Cℝ where
+  inductive
+  constructor mkCℝ
+  field
+    approx : ℚ₊ → ℝ
+    isCauchy : ∀ (δ ε : ℚ₊) → approx δ ~[ δ +₊ ε ] approx ε
+
+open Cℝ public
+
+-- ε-closeness
+data close where
+  rat~rat : ∀ q r ε     → - (ε .value) < q - r → q - r < ε .value → rat q ~[ ε           ] rat r
+  rat~lim : ∀ q y ε η   → rat q       ~[ ε ] y .approx η          → rat q ~[ ε +₊ η      ] lim y
+  lim~rat : ∀ x r ε δ   → x .approx δ ~[ ε ] rat r                → lim x ~[ ε +₊ δ      ] rat r
+  lim~lim : ∀ x y ε δ η → x .approx δ ~[ ε ] y .approx η          → lim x ~[ ε +₊ δ +₊ η ] lim y
+  squash~ : ∀ u v ε (ξ ζ : u ~[ ε ] v) → ξ ≡ ζ
+

Cubical/HITs/CauchyReal/Properties.agda

@@ -0,0 +1,66 @@
+{-# OPTIONS --safe #-}
+module Cubical.HITs.CauchyReal.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Rationals.Base
+open import Cubical.Data.Rationals.Order
+open import Cubical.Data.Rationals.Properties
+open import Cubical.Data.PositiveRational.Base
+open import Cubical.HITs.CauchyReal.Base
+
+module _
+  {a b}
+  (A : ℝ → Type a)
+  (B : ∀ {ε x y} → A x → A y → x ~[ ε ] y → Type b)
+  where
+
+  record DepCℝ (x : Cℝ) : Type (ℓ-max a b) where
+    inductive
+    field
+      approx : ∀ (ε : ℚ₊) → A (x .approx ε)
+      isCauchy : ∀ (δ ε : ℚ₊) → B (approx δ) (approx ε) (x .isCauchy δ ε)
+
+  open DepCℝ public
+
+module _
+  {a b}
+  (A : ℝ → Type a)
+  (B : ∀ {ε x y} → A x → A y → x ~[ ε ] y → Type b)
+  (case-rat : ∀ (q : ℚ) →
+              A (rat q))
+  (case-lim : ∀ (x : Cℝ) →
+              ∀ (x′ : DepCℝ A B x) →
+              A (lim x))
+  (case-eqℝ : ∀ (u v : ℝ) (h : ∀ ε → u ~[ ε ] v) →
+              ∀ (u′ : A u) (v′ : A v) (h′ : ∀ ε → B u′ v′ (h ε)) →
+              PathP (λ i → A (eqℝ u v h i)) u′ v′)
+  (case-rat~rat : ∀ q r ε (h₁ : - (ε .value) < q - r) (h₂ : q - r < ε .value) →
+                  B (case-rat q) (case-rat r) (rat~rat q r ε h₁ h₂))
+  (case-rat~lim : ∀ q y ε η (ξ : rat q ~[ ε ] y .approx η) →
+                  ∀ (y′ : DepCℝ A B y) (ξ′ : B (case-rat q) (y′ .approx η) ξ) →
+                  B (case-rat q) (case-lim y y′) (rat~lim q y ε η ξ))
+  (case-lim~rat : ∀ x r ε δ (ξ : x .approx δ ~[ ε ] rat r) →
+                  ∀ (x′ : DepCℝ A B x) (ξ′ : B (x′ .approx δ) (case-rat r) ξ) →
+                  B (case-lim x x′) (case-rat r) (lim~rat x r ε δ ξ))
+  (case-lim~lim : ∀ x y ε δ η (ξ : x .approx δ ~[ ε ] y .approx η) →
+                  ∀ (x′ : DepCℝ A B x) (y′ : DepCℝ A B y) (ξ′ : B (x′ .approx δ) (y′ .approx η) ξ) →
+                  B (case-lim x x′) (case-lim y y′) (lim~lim x y ε δ η ξ))
+  (case-squash~ : ∀ u v ε (ξ ζ : u ~[ ε ] v)
+                  (u′ : A u) (v′ : A v) (ξ′ : B u′ v′ ξ) (ζ′ : B u′ v′ ζ) →
+                  PathP (λ i → B u′ v′ (squash~ u v ε ξ ζ i)) ξ′ ζ′)
+  where
+
+  elim-ℝ : ∀ (u : ℝ) → A u
+  elim-Cℝ : ∀ (x : Cℝ) → DepCℝ A B x
+  elim-rel : ∀ {ε x y} (ξ : x ~[ ε ] y) → B (elim-ℝ x) (elim-ℝ y) ξ
+  elim-ℝ (rat q)       = case-rat q
+  elim-ℝ (lim x)       = case-lim x (elim-Cℝ x)
+  elim-ℝ (eqℝ u v h i) = case-eqℝ u v h (elim-ℝ u) (elim-ℝ v) (λ ε → elim-rel (h ε)) i
+  elim-Cℝ x = record { approx = λ ε → elim-ℝ (x .approx ε)
+                     ; isCauchy = λ δ ε → elim-rel (x .isCauchy δ ε)
+                     }
+  elim-rel (rat~rat q r ε h₁ h₂) = case-rat~rat q r ε h₁ h₂
+  elim-rel (rat~lim q y ε η ξ)   = case-rat~lim q y ε η ξ (elim-Cℝ y) (elim-rel ξ)
+  elim-rel (lim~rat x r ε δ ξ)   = case-lim~rat x r ε δ ξ (elim-Cℝ x) (elim-rel ξ)
+  elim-rel (lim~lim x y ε δ η ξ) = case-lim~lim x y ε δ η ξ (elim-Cℝ x) (elim-Cℝ y) (elim-rel ξ)
+  elim-rel (squash~ u v ε ξ ζ i) = case-squash~ u v ε ξ ζ (elim-ℝ u) (elim-ℝ v) (elim-rel ξ) (elim-rel ζ) i