quotient types

rhi commented

2023-05-31 11:15:23 -04:00

Owner

idk. i don't see why they'd need univalence, so

rhi added the

language

label 2023-06-11 12:58:27 -04:00

rhi changed title from ~~qits, maybe~~ to quotient types

2024-04-30 19:50:03 -04:00

rhi commented

2024-04-30 20:23:57 -04:00

Author

Owner

$$
\begin{aligned}
s, t, p, A, B, C, R &::=
\cdots \mid A⇂R \mid |s| \mid \mathsf{qeq} ; p
& \text{terms} \
\mathfrak{B} &::=
\cdots \mid |x| ⇒ s; : y, y', z ⇒ p
& \text{case bodies}
\end{aligned}

A⇂R is A : ★ quotiented by R : A → A → ★
|s| is the projection of s : A into A⇂R
- i probably won't use vertical bars for it tho
caseπ e return x ⇒ C of { |x| ⇒ s; y, y', z ⇒ p } applies s to the contents of
e : A⇂R, if p witnesses that the relation is preserved
qeq lifts a proof of a relation to an equality over the quotient

$$
\frac{
\begin{gathered}
Ψ \mid Γ ⊢₀ A ⇐ ★_ℓ \qquad
Ψ \mid Γ ⊢₀ R ⇐ A → A → ★_ℓ
\end{gathered}
}{
Ψ \mid Γ ⊢₀ A⇂R ⇐ ★_ℓ
} \text{[form]}

$$
\frac{
Ψ \mid Γ ⊢ σ \cdot s ⇐ A \rhd Σ
}{
Ψ \mid Γ ⊢ σ \cdot |s| ⇐ A⇂R \rhd Σ
} \text{[intro]}

$$
\frac{
\begin{gathered}
Ψ \mid Γ ⊢₀ s ⇐ A \qquad
Ψ \mid Γ ⊢₀ t ⇐ A \qquad
Ψ \mid Γ ⊢₀ p ⇐ R ; s ; t
\end{gathered}
}{
Ψ \mid Γ ⊢₀ \mathsf{qeq} ; p ⇐ |s| ≡ |t| : A⇂R
} \text{[ax]}

$$
\frac{
\begin{gathered}
Ψ \mid Γ ⊢ σ \cdot e ⇒ A⇂R \rhd Σ_e \qquad
Ψ \mid Γ, x : A⇂R ⊢₀ C ⇐ ★ \
Ψ \mid Γ, x : A ⊢ σ \cdot s ⇐ C[(|x| ∷ A⇂R)/x] \rhd Σ_s, ρ_x \qquad
ρ_x ≼ πσ \
Ψ \mid Γ, y : A, y' : A, z : R ; y ; y' ⊢₀
p ⇐ \mathsf{Eq} ; (i ⇒ C[\mathsf{qeq} ; z ; @i/x]) ; s[y/x] ; s[y'/x]
\end{gathered}
}{
Ψ \mid Γ ⊢ σ \cdot
\mathsf{case}_π ; e ;
\mathsf{return} ; x ⇒ C ; \mathsf{of} ;
{ |x| ⇒ s; : y, y', z ⇒ p }
⇒ C[e/x] \rhd Σ_e + πΣ_s
} \text{[elim]}

$$
\frac{}{
\mathsf{case}_π ; |t| ∷ A ⇂ R ;
\mathsf{return} ; x ⇒ C ; \mathsf{of} ;
{ |x| ⇒ s; : y, y', z ⇒ p } ⇝ s[(t ∷ A)/x]
} [β]

$$ \begin{aligned} s, t, p, A, B, C, R &::= \cdots \mid A⇂R \mid |s| \mid \mathsf{qeq} \; p & \text{terms} \\ \mathfrak{B} &::= \cdots \mid |x| ⇒ s; \: y, y', z ⇒ p & \text{case bodies} \end{aligned} $$ - `A⇂R` is `A : ★` quotiented by `R : A → A → ★` - `|s|` is the projection of `s : A` into `A⇂R` - i probably won't use vertical bars for it tho - `caseπ e return x ⇒ C of { |x| ⇒ s; y, y', z ⇒ p }` applies `s` to the contents of `e : A⇂R`, if `p` witnesses that the relation is preserved - `qeq` lifts a proof of a relation to an equality over the quotient $$ \frac{ \begin{gathered} Ψ \mid Γ ⊢₀ A ⇐ ★_ℓ \qquad Ψ \mid Γ ⊢₀ R ⇐ A → A → ★_ℓ \end{gathered} }{ Ψ \mid Γ ⊢₀ A⇂R ⇐ ★_ℓ } \text{[form]} $$ $$ \frac{ Ψ \mid Γ ⊢ σ \cdot s ⇐ A \rhd Σ }{ Ψ \mid Γ ⊢ σ \cdot |s| ⇐ A⇂R \rhd Σ } \text{[intro]} $$ $$ \frac{ \begin{gathered} Ψ \mid Γ ⊢₀ s ⇐ A \qquad Ψ \mid Γ ⊢₀ t ⇐ A \qquad Ψ \mid Γ ⊢₀ p ⇐ R \; s \; t \end{gathered} }{ Ψ \mid Γ ⊢₀ \mathsf{qeq} \; p ⇐ |s| ≡ |t| : A⇂R } \text{[ax]} $$ $$ \frac{ \begin{gathered} Ψ \mid Γ ⊢ σ \cdot e ⇒ A⇂R \rhd Σ_e \qquad Ψ \mid Γ, x : A⇂R ⊢₀ C ⇐ ★ \\ Ψ \mid Γ, x : A ⊢ σ \cdot s ⇐ C[(|x| ∷ A⇂R)/x] \rhd Σ_s, ρ_x \qquad ρ_x ≼ πσ \\ Ψ \mid Γ, y : A, y' : A, z : R \; y \; y' ⊢₀ p ⇐ \mathsf{Eq} \; (i ⇒ C[\mathsf{qeq} \; z \; @i/x]) \; s[y/x] \; s[y'/x] \end{gathered} }{ Ψ \mid Γ ⊢ σ \cdot \mathsf{case}_π \; e \; \mathsf{return} \; x ⇒ C \; \mathsf{of} \; \{ |x| ⇒ s; \: y, y', z ⇒ p \} ⇒ C[e/x] \rhd Σ_e + πΣ_s } \text{[elim]} $$ $$ \frac{}{ \mathsf{case}_π \; |t| ∷ A ⇂ R \; \mathsf{return} \; x ⇒ C \; \mathsf{of} \; \{ |x| ⇒ s; \: y, y', z ⇒ p \} ⇝ s[(t ∷ A)/x] } [β] $$

rhi commented

2024-05-22 19:37:00 -04:00

Author

Owner

{-# OPTIONS --hidden-argument-puns --cubical #-}

open import Level
open import Function
open import Cubical.Foundations.Prelude

variable
  𝒿 𝓀 ℓ : Level
  A B : Type 𝓀
  a b : A
  f : A → B

Pred Rel : Type ℓ → ∀ 𝓀 → Type _
Pred A 𝓀 = A → Type 𝓀
Rel  A 𝓀 = A → A → Type 𝓀

variable
  P : Pred A ℓ
  R : Rel A ℓ


module Dependent where
  postulate
    _/_ : (A : Type 𝓀) → Rel A ℓ → Type (𝓀 ⊔ ℓ)
    [_] : A → A / R
    qax   : R a b → (A / R ∋ [ a ]) ≡ [ b ]

  record IsOK {A : Set 𝒿} (R : Rel A 𝓀) (P : A / R → Type ℓ)
              (f : ∀ x → P [ x ]) : Type (𝒿 ⊔ 𝓀 ⊔ ℓ) where
    constructor isOK
    field get : (r : R a b) → PathP (λ 𝑖 → P (qax r 𝑖)) (f a) (f b)

  postulate
    qelim : (P : A / R → Type ℓ) →
            (f : ∀ x → P [ x ]) →
            (ok : IsOK R P f) →
            (s : A / R) → P s

    qcomp : {f : ∀ x → P [ x ]} →
            {ok : IsOK R P f} →
            ∀ a → qelim P f ok [ a ] ≡ f a


module Nondependent where
  open Dependent public using (_/_; [_]; qax; isOK)

  IsOK : (f : A → B) (R : Rel A ℓ) → Type _
  IsOK {B} f R = Dependent.IsOK R (λ _ → B) f

  qelim : (f : A → B) → IsOK f R → A / R → B
  qelim f (isOK ok) x = Dependent.qelim _ f (isOK ok) x

  qcomp : ∀ {ok : IsOK f R} a → qelim f ok [ a ] ≡ f a
  qcomp = Dependent.qcomp

open Dependent
private module N = Nondependent

η⁻¹ : (x : A / R) → N.qelim [_] (isOK qax) x ≡ x
η⁻¹ {R} = qelim _ (λ x → qcomp x) (isOK ok′) where
  ok′ : (r : R a b) → PathP _ (qcomp a) (qcomp b)
  ok′ r = {!λ 𝑖 → qcomp (qax r 𝑖) 𝑖!} -- needs uip but otherwise ok

```agda {-# OPTIONS --hidden-argument-puns --cubical #-} open import Level open import Function open import Cubical.Foundations.Prelude variable 𝒿 𝓀 ℓ : Level A B : Type 𝓀 a b : A f : A → B Pred Rel : Type ℓ → ∀ 𝓀 → Type _ Pred A 𝓀 = A → Type 𝓀 Rel A 𝓀 = A → A → Type 𝓀 variable P : Pred A ℓ R : Rel A ℓ module Dependent where postulate _/_ : (A : Type 𝓀) → Rel A ℓ → Type (𝓀 ⊔ ℓ) [_] : A → A / R qax : R a b → (A / R ∋ [ a ]) ≡ [ b ] record IsOK {A : Set 𝒿} (R : Rel A 𝓀) (P : A / R → Type ℓ) (f : ∀ x → P [ x ]) : Type (𝒿 ⊔ 𝓀 ⊔ ℓ) where constructor isOK field get : (r : R a b) → PathP (λ 𝑖 → P (qax r 𝑖)) (f a) (f b) postulate qelim : (P : A / R → Type ℓ) → (f : ∀ x → P [ x ]) → (ok : IsOK R P f) → (s : A / R) → P s qcomp : {f : ∀ x → P [ x ]} → {ok : IsOK R P f} → ∀ a → qelim P f ok [ a ] ≡ f a module Nondependent where open Dependent public using (_/_; [_]; qax; isOK) IsOK : (f : A → B) (R : Rel A ℓ) → Type _ IsOK {B} f R = Dependent.IsOK R (λ _ → B) f qelim : (f : A → B) → IsOK f R → A / R → B qelim f (isOK ok) x = Dependent.qelim _ f (isOK ok) x qcomp : ∀ {ok : IsOK f R} a → qelim f ok [ a ] ≡ f a qcomp = Dependent.qcomp open Dependent private module N = Nondependent η⁻¹ : (x : A / R) → N.qelim [_] (isOK qax) x ≡ x η⁻¹ {R} = qelim _ (λ x → qcomp x) (isOK ok′) where ok′ : (r : R a b) → PathP _ (qcomp a) (qcomp b) ok′ r = {!λ 𝑖 → qcomp (qax r 𝑖) 𝑖!} -- needs uip but otherwise ok ```

quotient types #10