6
$\begingroup$

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!

$\endgroup$
6
  • 5
    $\begingroup$ 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. $\endgroup$ Mar 2, 2023 at 7:55
  • $\begingroup$ 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! $\endgroup$ Mar 2, 2023 at 13:45
  • $\begingroup$ @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? $\endgroup$ Mar 2, 2023 at 23:33
  • $\begingroup$ @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. $\endgroup$ Mar 3, 2023 at 12:33
  • 1
    $\begingroup$ Wouldn't the simplest thing here be to show that Nat and Int / rInt are equivalent, and then use ordinary induction on Nat? $\endgroup$ Mar 3, 2023 at 13:02

1 Answer 1

0
$\begingroup$

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)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.