Skip to content

Instantly share code, notes, and snippets.

@gergoerdi

gergoerdi/Int.agda

Created Nov 11, 2018
Embed
What would you like to do?
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
You can’t perform that action at this time.