# Paths Between Quotient Types in Cubical Agda

I'm new to Cubical Agda and I am trying to define the dependent set eliminator for certain quotient types.

In particular, my quotient type is the integers, quotiented by the absolute value function (Int / rInt), defined as follows:

data Int : Set where
pos : (n : Nat) → Int
neg : (n : Nat) → Int

rNat : Nat -> Nat -> Type
rNat zero zero = True
rNat zero (suc b) = ⊥
rNat (suc a) zero = ⊥
rNat (suc a) (suc b) = rNat a b

abs : Int -> Nat
abs (pos x) = x
abs (neg x) = x

rNatEq : (a : Nat) -> (b : Nat) → (rNat a b) → a ≡ b
rNatEq zero zero x = refl
rNatEq (suc a) (suc b) x = cong suc (rNatEq a b x)

rInt : Int -> Int -> Type
rInt a b = rNat (abs a) (abs b)


I wish to prove/define the following hole:

depElimSetInt/rInt : (P : Int / rInt -> Set) -> (∀ x -> isSet (P x)) -> (P depConstrInt/rInt0) -> (∀ n -> (P n) -> P (depConstrInt/rIntS n)) -> ((x : Int / rInt) -> P x)
depElimSetInt/rInt P set baseCase sucCase = SetQuotients.elim set lem wellDefined where
lem : (a : Int) → P [ a ]
lem (pos zero) = baseCase
lem (pos (suc n)) =  sucCase [ pos n ] (lem (pos n))
lem (neg zero) = transport (cong P (rIntPosNegQ 0)) baseCase
lem (neg (suc n)) = transport (cong P (rIntPosNegQ (suc n))) (sucCase [ pos n ] (lem (pos n)))
wellDefined : (a b : Int) (r : rInt a b) → PathP (λ i → P (eq/ a b r i)) (lem a) (lem b)
wellDefined = {!!}


where depConstrInt/rInt0 corresponds to my base case:

depConstrInt/rInt0 : Int / rInt
depConstrInt/rInt0 = [ pos 0 ]


and depConstrInt/rIntS corresponds to succesion over my quotiented integers:

depConstrInt/rIntS : Int / rInt -> Int / rInt
depConstrInt/rIntS = sucInt/rInt


wellDefined is intuitively true because the construction of r means that lem a and lem b should relate under the equivalence relation (rInt).

As lemmas, I've proven some theorems that I think may help:

rNatEquiv : (a : Nat) -> (rNat a a)
rNatEquiv zero = tt
rNatEquiv (suc a) = rNatEquiv a

rIntPosNeg : (n : Nat) → (rInt (pos n) (neg n))
rIntPosNeg n = rNatEquiv n

rIntPosNegQ : (n : Nat) -> ([_] {A = Int} {R = rInt} (pos n)  ≡ [_] {A = Int} {R = rInt} (neg n))
rIntPosNegQ n = eq/ (pos n) (neg n) (rIntPosNeg n)

rIntEquivGen : (a : Int) -> (b : Int) -> (r : rInt a b) → ([ a ] ≡ [ b ]) ≡ ([ a ] ≡ [ a ])
rIntEquivGen a b r = subst (λ x → ([ a ] ≡ x) ≡ (([_] {R = rInt} a) ≡ [ a ])) (eq/ {R = rInt} a b r) refl


I've attempted to prove this via congP, transport, and subst, with the lemmas I have already shown (after breaking into cases), but am not sure if this is the right strategy. Thanks!

• A general comment (also to others reading this): please include complete working pieces of code when possible, including import statements and comments explaining what version of which proof assistant you're using. This helps others who may have the theoretical knowledge to help you, but are not across your office and don't know what you're doing. It also helps future readers. Mar 2 at 7:55
• Your construction is a special case of a wedge sum (en.wikipedia.org/wiki/Wedge_sum). The well-definedness of such a thing depends on it being a pushout. You've got all the pieces except the universal property, as far as I can tell. If you know category theory, this should help. Otherwise, sorry! Mar 2 at 13:45
• @JacquesCarette: If I am reading the code correctly, it's a quotient $\mathbb{Z}/{\sim}$ where $m \sim n \iff |m| = |n|$. How is this a wedge sum? Mar 2 at 23:33
• @AndrejBauer If I'm reading the code correctly, it's the disjoint union of two copies of ℕ quotiented by making both copies of 0 be equal. It's defining $\mathbb{Z}$ not quotienting it. Mar 3 at 12:33
• Wouldn't the simplest thing here be to show that Nat and Int / rInt are equivalent, and then use ordinary induction on Nat? Mar 3 at 13:02

I have comments inside the code. I am also interested if someone could further simplify the code.

Also, keep in mind that your Int has two zeros, a positive one and a negative one.

{-# OPTIONS --cubical #-}
module test2 where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat
open import Cubical.Data.Unit renaming (Unit to ⊤)
open import Cubical.HITs.SetQuotients as SQ

data Int : Set where
pos    : (n : ℕ) → Int
neg : (n : ℕ) → Int

rNat : ℕ -> ℕ -> Type
rNat zero zero = ⊤
rNat zero (suc y) = ⊥
rNat (suc x) zero = ⊥
rNat (suc x) (suc y) = rNat x y

abs : Int -> ℕ
abs (pos x) = x
abs (neg x) = x

rInt : Int -> Int -> Type
rInt a b = rNat (abs a) (abs b)

dp0 : Int / rInt
dp0 = [ pos 0 ]

dS : Int / rInt -> Int / rInt
dS a = SQ.rec squash/ (λ x → [ l2 x ]) (λ a b r i → eq/ (l2 a) (l2 b) (l1 a b r) i) a where
l2 : Int → Int
l2 (pos n) = pos (suc n)
l2 (neg n) = neg (suc n)
l1 : ∀ (a b : Int) → rInt a b → rInt (l2 a) (l2 b)
l1 (pos x) (pos y) r = r
l1 (pos x) (neg y) r = r
l1 (neg x) (pos y) r = r
l1 (neg x) (neg y) r = r

depElimSetInt/rInt : (P : Int / rInt -> Set) -> (∀ x -> isSet (P x))
-> (P [ pos 0 ])
-> (∀ n -> (P n) -> P (dS n))
-> ((x : Int / rInt) -> P x)
depElimSetInt/rInt P isSet Pp0 sucCase q = SQ.elim isSet lem l2 q where

lem : (a : Int) → P [ a ]
lem (pos zero) = Pp0
lem (pos (suc n)) = sucCase [ pos n ] (lem (pos n))
lem (neg zero) = transport (λ i → P (eq/ (pos zero) (neg zero) tt i)) Pp0
lem (neg (suc n)) = sucCase [ neg n ] (lem (neg n))

l2 : (a b : Int) (r : rInt a b) →
PathP (λ i → P (eq/ a b r i)) (lem a) (lem b)
l2 (pos zero) (pos zero) r = subst (λ q → PathP (λ i → P (q i)) Pp0 Pp0) l5 refl where
-- Since Pp0 is equal with itself, we only need to prove that the path due to to eq/ is equal to the
-- path due to refl.
l5 : refl ≡ eq/ (pos zero) (pos zero) r
l5 = squash/ [ pos zero ] [ pos zero ] refl (eq/ (pos zero) (pos zero) r)
l2 (pos (suc x)) (pos (suc y)) r i
-- Here we take advantage of the fact that sucCase is defined on (eq/ a b r i), in other words
-- it respects the boundaries.
= sucCase (eq/ (pos x) (pos y) r i) (l2 (pos x) (pos y) r i)
l2 (pos zero) (neg zero) r
-- Check the definition of toPathP
= toPathP refl
l2 (pos (suc x)) (neg (suc y)) r i
-- lem has changed so as to take advantage of the fact that sucCase respects the boundaries.
= sucCase (eq/ (pos x) (neg y) r i) (l2 (pos x) (neg y) r i)
l2 (neg zero) (neg zero) r = subst (λ q → PathP (λ i → P (q i)) Pn0 Pn0) l5 refl where
Pn0 = transport (λ i → P (eq/ (pos zero) (neg zero) tt i)) Pp0
l5 : refl ≡ eq/ (neg zero) (neg zero) r
l5 = squash/ [ neg zero ] [ neg zero ] refl (eq/ (neg zero) (neg zero) r)
l2 (neg zero) (pos zero) r = subst
(λ q →
PathP (λ i → P (q i))
(transport (λ i → P (eq/ (pos zero) (neg zero) tt i)) Pp0) Pp0)
(sym l6) (symP (toPathP refl)) where
-- keep in mind that eq (neg zero) (pos zero) tt is not necessary equal to eq (pos zero) (neg zero) tt
-- They define two differrent paths, thank gods, our quotient is a Set.
l6 : eq/ (neg zero) (pos zero) tt ≡ sym (eq/ (pos zero) (neg zero) tt)
l6 = squash/ [ neg zero ] [ pos zero ] (eq/ (neg zero) (pos zero) _) (λ i → eq/ (pos 0) (neg 0) _ (~ i))
l2 (neg (suc x)) (pos (suc y)) r i = sucCase (eq/ (neg x) (pos y) r i) (l2 (neg x) (pos y) r i)
l2 (neg (suc x)) (neg (suc y)) r i = sucCase (eq/ (neg x) (neg y) r i) (l2 (neg x) (neg y) r i)