Quot indexed by Quot

Stream: general

[Max Nowak 🐉]

I have two types A : Type, B : A -> Type, where one is indexed by the other. I want to quotient them both, but I do not know what the proper way of doing that is. Below is an MWE, but I can not figure out how to implement consQ.

-- import Mathlib.Data.Quot

inductive A : Type
inductive B : A -> Type
opaque cons : (a : A) -> B a -> A := sorry -- this is given

inductive A.Rel : A -> A -> Prop
inductive B.Rel : B a1 -> B a2 -> Prop
instance A.setoid : Setoid A := ⟨A.Rel, sorry⟩
instance B.setoid : Setoid (B a) := ⟨B.Rel, sorry⟩

def AQ : Type := Quotient (α := A) A.setoid
def BQ (aq : AQ) : Type := Quotient.liftOn aq (fun a => Quotient (α := B a) B.setoid) sorry

def consQ (aq : AQ) (bq : BQ aq) : AQ :=
  Quotient.liftOn aq
    (fun (a : A) =>
      let b : B a := bq -- how??
      ⟦cons a b⟧
    )
    sorry

[Robin Arnez]

You can use Quotient.recOn here or Quotient.pliftOn:

def consQ (aq : AQ) (bq : BQ aq) : AQ :=
  Quotient.recOn aq
    (fun (a : A) bq =>
      let b : Quotient B.setoid := bq
      sorry)
    sorry bq

or

def consQ (aq : AQ) (bq : BQ aq) : AQ :=
  Quotient.pliftOn aq
    (fun (a : A) h =>
      let b : Quotient B.setoid := h ▸ bq
      sorry)
    sorry

recOn is more general but for pliftOn the last sorry is easier to prove.

[Max Nowak 🐉]

Oh! Yeah that works, awesome. Thanks so much. I was stuck at this for way longer than I like to admit.

[Kenny Lau]

@Max Nowak 🐉

-- import Mathlib.Data.Quot

inductive A : Type
inductive B : A -> Type
opaque cons : (a : A) -> B a -> A := sorry -- this is given

inductive A.Rel : A -> A -> Prop
inductive B.Rel : B a1 -> B a2 -> Prop
instance A.setoid : Setoid A := ⟨A.Rel, sorry⟩
instance B.setoid : Setoid (B a) := ⟨B.Rel, sorry⟩

def AQ : Type := Quotient (α := A) A.setoid
def BQ (aq : AQ) : Type := Quotient.liftOn aq (fun a => Quotient (α := B a) B.setoid) sorry

def consQ (aq : AQ) : BQ aq → AQ :=
  Quotient.recOn aq
    (fun (a : A) =>
      fun bq => Quotient.recOn bq (fun b => Quotient.mk _ (cons a b))
        sorry
    )
    sorry

[Max Nowak 🐉]

Yeah, once I have bq : B ⟦a⟧ instead of bq : B aq this works. I had not realized you can use Quotient.recOn to do that. That was the key insight I learned from this.

[Max Nowak 🐉]

Is there a convenience function, similar to lift₂, which packages this up in some nicer way? Especially having to prove two different but related sorry seems like a lot of tedious work.

[Max Nowak 🐉]

Especially since I have some functions taking 5 different arguments, all quotiented :)....

[Kenny Lau]

do you need 5 quotients... :melt:
(I'm sure you have a good reason, don't mind me)