Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Cubical quotient types
{-# OPTIONS --cubical #-}
module Quotient where
open import Cubical.Core.Prelude
Reflexive : {ℓ} {A : Set ℓ} (A A Set ℓ) Set _
Reflexive _∼_ = x x ∼ x
module Quot {ℓ} (A : Set ℓ) (_∼_ : A A Set ℓ) (∼-refl : Reflexive _∼_) where
data Q : Setwhere
point : A Q
quot : {x y : A} x ∼ y point x ≡ point y
trunc : {x y : Q} (p q : x ≡ y) p ≡ q
module _ {ℓ} {P : Q Set ℓ}
(point* : x P (point x))
(quot* : {x y} eq PathP (λ i P (quot {x} {y} eq i)) (point* x) (point* 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
Q-elim : x P x
Q-elim (point x) = point* x
Q-elim (quot eq i) = quot* eq i
Q-elim (trunc {x} {y} p q i j) = trunc* (cong Q-elim p) (cong Q-elim q) i j
Rel : {ℓ} Set Set _
Rel {ℓ} A = A A Set
rel-pair : {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (_∼_ : Rel A) (_≈_ : Rel B) Rel (A × B)
rel-pair _∼_ _≈_ = λ { (x , y) (x′ , y′) x ∼ x′ × y ≈ y′ }
refl-pair : {ℓ₁ ℓ₂} {A B} (∼ ≈)
Reflexive {ℓ₁} {A} ∼ Reflexive {ℓ₂} {B} ≈ Reflexive (rel-pair ∼ ≈)
refl-pair _ _ ∼-refl ≈-refl = λ { (x , y) (∼-refl x , ≈-refl y) }
module Quot² {ℓ₁ ℓ₂} {A₁ _∼_} (∼-refl : Reflexive {ℓ₁} {A₁} _∼_) {A₂ _≈_} (≈-refl : Reflexive {ℓ₂} {A₂} _≈_) where
open Quot A₁ _∼_ ∼-refl renaming (Q to Q₁; Q-elim to Q₁-elim) hiding (quot; point; trunc)
open Quot A₂ _≈_ ≈-refl renaming (Q to Q₂; Q-elim to Q₂-elim) hiding (quot; point; trunc)
open Quot (A₁ × A₂) (rel-pair _∼_ _≈_) (refl-pair _∼_ _≈_ ∼-refl ≈-refl)
open import Utils
module _ where
fromPair : Q₁ Q₂ Q
fromPair = Q₁-elim
(λ x Q₂-elim
(λ y point (x , y))
(λ {y} {y′} y≈y′ quot (∼-refl x , y≈y′))
trunc)
(λ {x} {y} eq₁ i Q₂-elim
(λ a quot (eq₁ , ≈-refl a) i)
(λ {a} {b} eq₂ j lemma eq₁ eq₂ i j)
trunc)
(λ {x} {y} {p} {q} {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 : A₁} {a b : A₂} (x ∼ y) (a ≈ b) I I Q
lemma {x} {y} {a} {b} eq₁ eq₂ i j = surface i j
where
X Y : Q₁
X = Quot.point x
Y = Quot.point y
A B : Q₂
A = Quot.point a
B = Quot.point b
XA = point (x , a)
XB = point (x , b)
YA = point (y , a)
YB = point (y , b)
p : X ≡ Y
p = Quot.quot eq₁
q : A ≡ B
q = Quot.quot eq₂
p₀ : XA ≡ YA
p₀ = quot (eq₁ , ≈-refl _)
p₁ : XB ≡ YB
p₁ = quot (eq₁ , ≈-refl _)
q₀ : XA ≡ XB
q₀ = quot (∼-refl _ , eq₂)
q₁ : YA ≡ YB
q₁ = quot (∼-refl _ , 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.