Paths Between Quotient Types in Cubical Agda

Question

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!

Answer 1

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)