Int as a HIT
{-# OPTIONS --cubical #-} | |
module Int where | |
open import Data.Nat renaming (_+_ to _+̂_) | |
open import Cubical.Core.Prelude | |
open import Utils | |
Same : ℕ → ℕ → ℕ → ℕ → Set | |
Same x y x′ y′ = x +̂ y′ ≡ x′ +̂ y | |
data ℤ : Set where | |
_-_ : (x : ℕ) → (y : ℕ) → ℤ | |
quot : ∀ {x y x′ y′} → Same x y x′ y′ → (x - y) ≡ (x′ - y′) | |
trunc : {x y : ℤ} → (p q : x ≡ y) → p ≡ q | |
module ℤElim {ℓ} {P : ℤ → Set ℓ} | |
(point* : ∀ x y → P (x - y)) | |
(quot* : ∀ {x y x′ y′} same → PathP (λ i → P (quot {x} {y} {x′} {y′} same i)) (point* x y) (point* x′ y′)) | |
(trunc* : ∀ {x y} {p q : x ≡ y} → ∀ {fx : P x} {fy : P y} (eq₁ : PathP (λ i → P (p i)) fx fy) (eq₂ : PathP (λ i → P (q i)) fx fy) → PathP (λ i → PathP (λ j → P (trunc p q i j)) fx fy) eq₁ eq₂) | |
where | |
ℤ-elim : ∀ x → P x | |
ℤ-elim (x - y) = point* x y | |
ℤ-elim (quot p i) = quot* p i | |
ℤ-elim (trunc p q i j) = trunc* (cong ℤ-elim p) (cong ℤ-elim q) i j | |
open ℤElim public | |
_+1 : ℤ → ℤ | |
(x - y) +1 = suc x - y | |
quot {x} {y} eq i +1 = quot {suc x} {y} (cong suc eq) i | |
trunc p q i j +1 = trunc (cong _+1 p) (cong _+1 q) i j | |
_+1′ : ℤ → ℤ | |
_+1′ = ℤ-elim | |
(λ x y → suc x - y) | |
(λ eq → quot (cong suc eq)) | |
trunc | |
open import Relation.Binary.PropositionalEquality renaming (refl to prefl; _≡_ to _=̂_) using () | |
fromPropEq : ∀ {ℓ A} {x y : A} → _=̂_ {ℓ} {A} x y → x ≡ y | |
fromPropEq prefl = refl | |
open import Function using (_$_) | |
import Data.Nat.Properties | |
open Data.Nat.Properties.SemiringSolver | |
using (prove; solve; _:=_; con; var; _:+_; _:*_; :-_; _:-_) | |
reorder : ∀ x y a b → (x +̂ a) +̂ (y +̂ b) ≡ (x +̂ y) +̂ (a +̂ b) | |
reorder x y a b = fromPropEq $ solve 4 (λ x y a b → (x :+ a) :+ (y :+ b) := (x :+ y) :+ (a :+ b)) prefl x y a b | |
inner-lemma : ∀ x y {a b a′ b′} → a +̂ b′ ≡ a′ +̂ b → (x +̂ a) +̂ (y +̂ b′) ≡ (x +̂ a′) +̂ (y +̂ b) | |
inner-lemma x y {a} {b} {a′} {b′} prf = begin | |
(x +̂ a) +̂ (y +̂ b′) ≡⟨ reorder x y a b′ ⟩ | |
(x +̂ y) +̂ (a +̂ b′) ≡⟨ cong (x +̂ y +̂_) prf ⟩ | |
(x +̂ y) +̂ (a′ +̂ b) ≡⟨ sym (reorder x y a′ b) ⟩ | |
(x +̂ a′) +̂ (y +̂ b) ∎ | |
outer-lemma : ∀ x y {x′} {y′} {a b} → x +̂ y′ ≡ x′ +̂ y → (x +̂ a) +̂ (y′ +̂ b) ≡ (x′ +̂ a) +̂ (y +̂ b) | |
outer-lemma x y {x′} {y′} {a} {b} prf = begin | |
(x +̂ a) +̂ (y′ +̂ b) ≡⟨ reorder x y′ a b ⟩ | |
(x +̂ y′) +̂ (a +̂ b) ≡⟨ cong (_+̂ (a +̂ b)) prf ⟩ | |
(x′ +̂ y) +̂ (a +̂ b) ≡⟨ sym (reorder x′ y a b) ⟩ | |
(x′ +̂ a) +̂ (y +̂ b) ∎ | |
_+_ : ℤ → ℤ → ℤ | |
_+_ = ℤ-elim | |
(λ x y → ℤ-elim | |
(λ a b → (x +̂ a) - (y +̂ b)) | |
(λ eq₂ → quot (inner-lemma x y eq₂)) | |
trunc) | |
(λ {x} {y} {x′} {y′} eq₁ i → ℤ-elim | |
(λ a b → quot (outer-lemma x y eq₁) i) | |
(λ {a} {b} {a′} {b′} eq₂ j → lemma {x} {y} {x′} {y′} {a} {b} {a′} {b′} eq₁ eq₂ i j ) | |
trunc) | |
(λ {_} {_} {_} {_} {x+} {y+} eq₁ eq₂ i → | |
funExt λ a → λ j → trunc {x+ a} {y+ a} (ap eq₁ a) (ap eq₂ a) i j) | |
where | |
lemma : ∀ {x y x′ y′ a b a′ b′} → Same x y x′ y′ → Same a b a′ b′ → I → I → ℤ | |
lemma {x} {y} {x′} {y′} {a} {b} {a′} {b′} eq₁ eq₂ i j = surface i j | |
where | |
{- | |
p Xᵢ | |
X ---------+---> X′ | |
p₀ i | |
A X+A --------\---> X′+A | |
| | | | |
q| q₀ | | qᵢ | |
| | | | |
Aⱼ + j+ [+] <--- This is where we want to get to! | |
| | | | |
V V p₁ | | |
A′ X+A′ -------/---> X′+A′ | |
i | |
-} | |
X = x - y | |
X′ = x′ - y′ | |
A = a - b | |
A′ = a′ - b′ | |
X+A = (x +̂ a) - (y +̂ b) | |
X′+A = (x′ +̂ a) - (y′ +̂ b) | |
X+A′ = (x +̂ a′) - (y +̂ b′) | |
X′+A′ = (x′ +̂ a′) - (y′ +̂ b′) | |
p : X ≡ X′ | |
p = quot eq₁ | |
q : A ≡ A′ | |
q = quot eq₂ | |
p₀ : X+A ≡ X′+A | |
p₀ = quot (outer-lemma x y eq₁) | |
p₁ : X+A′ ≡ X′+A′ | |
p₁ = quot (outer-lemma x y eq₁) | |
q₀ : X+A ≡ X+A′ | |
q₀ = quot (inner-lemma x y eq₂) | |
q₁ : X′+A ≡ X′+A′ | |
q₁ = quot (inner-lemma x′ y′ eq₂) | |
qᵢ : ∀ i → p₀ i ≡ p₁ i | |
qᵢ = slidingLid p₀ p₁ q₀ | |
left : qᵢ i0 ≡ q₀ | |
left = refl | |
right : qᵢ i1 ≡ q₁ | |
right = trunc (qᵢ i1) q₁ | |
surface : PathP (λ i → p₀ i ≡ p₁ i) q₀ q₁ | |
surface i = comp (λ j → p₀ i ≡ p₁ i) | |
(λ { j (i = i0) → left j | |
; j (i = i1) → right j | |
}) | |
(inc (qᵢ i)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment