A series of equality lemmas for SetQuotient

[reswatson]

A series of equality lemmas for SetQuotients.

[maxsnew]

I think these should be added to SetQuotients.Properties rather than a new file

[reswatson]

@maxsnew: OK.

Whilst adding my code to Properties I noticed that in that case maybe the explanatory code from iso/R→≡→Iso to R*≡λtt could be removed as being not about SetQuotient properties diretcly but about the Iso/R construction. Should I leave that explanatory code in or take it out, or something else?

[maxsnew]

what code are you referring to?

[anshwad10]

This seems redundant with https://agda.github.io/cubical/Cubical.Relation.Binary.Base.html#6711

[reswatson]

I'd like another opinion, but I could try rewriting it using that if that's agreed to be the better way. SetQuotients should use equivalence relations, but maybe I can start with RelIso instead?

[reswatson]

Re: anshwad10's suggestion: Trying to use RelIso becomes complicated and confusing I think. It can certainly be done, but it's like you are fighting the initial assumption that there are two general possibly unrelated relations instead of needing just 1 equivalence relation with its dual R* induced. Below are 3 ways of defining the induced relation R* by employing RelIso first:

-- OPTION 1: Will lead to more complicated functions as there is more stuff being carried around (which I could be just put in the record Iso/R or similar):
IsEquivRelIso : {A A' : Type ℓ}{R : A → A → Type ℓ} → (ER : isEquivRel R) →
          (fun : A → A') → (inv : A' → A) → (leftInv : ∀ a → R (inv (fun a)) a) → RelIso {A = A} R {A' = A'} (λ x y → R (inv x) (inv y))
IsEquivRelIso {A}{A'}{R} ER fun inv leftInv = reliso fun inv (λ a' → leftInv (inv a')) leftInv

R*-Alt : {A A' : Type ℓ}{R : A → A → Type ℓ}{ER : isEquivRel R}{fun : A → A'}{inv : A' → A}{leftInv : ∀ a → R (inv (fun a)) a} → A' → A' → Type ℓ
R*-Alt {R = R}{inv = inv} x y = R (inv x) (inv y) 

--OPTION 2: Encapsulate requirements in a Sigma type (not pretty!):
SigmaR* : {A B : Type ℓ}{R : A → A → Type ℓ}{ER : isEquivRel R} →
  (fun : A → B) → (inv : B → A) → (leftInv : ∀ a → R (inv (fun a)) a) →
  Σ (B → B → Type ℓ) λ R* → (RelIso {A = A} R {B} R*) 
SigmaR* {ℓ}{A}{B}{R}{ER} fun inv leftInv = (λ b b' → R (inv b) (inv b')) , reliso fun inv (λ a' → leftInv (inv a')) leftInv

R*-Alt2 : {A B : Type ℓ}{R : A → A → Type ℓ}{ER : isEquivRel R} →
  (fun : A → B) → (inv : B → A) → (leftInv : ∀ a → R (inv (fun a)) a) → B → B → Type ℓ
R*-Alt2 {ℓ}{A}{B}{R}{ER} fun inv leftInv = fst (SigmaR* {ER = ER} fun inv leftInv) 

-- OPTION 3 : Although this one seems simpler it is confusing that rightInv and R' aren't needed since
--            they're acting as dummies to be discarded, and we really want "R (iso/r .inv/ x) (iso/r .inv/ x')", 
--            for rightInv and R* for R', which was the idea for OPTION 1 and 2.
R*-Alt3 : {A A' : Type ℓ}{R : A → A → Type ℓ}{R' : A' → A' → Type ℓ} {ER : isEquivRel R} (iso/r : RelIso {A = A} R {A' = A'} R') → A' → A' → Type ℓ
R*-Alt3 {ℓ}{A}{A'}{R}{R'} {ER} iso/r@(reliso fun inv rightInv₁ leftInv₁) x y =  R (iso/r .inv/ x) (iso/r .inv/ y)

Maybe I'm wrong, but I can't see a better way than putting the essentials into a Record type in an analogous, but not identical way to RelIso. It sort of explains what's happening, the essence of what is needed.

[anshwad10]

Ok, that makes sense. You don't need to use RelIso here, but you can at least put something like Iso/R→RelIso in Relations.Binary?

[reswatson]

Nice idea. I'll put it in this file presently and leave rearranging where it goes until further comments are received.

[reswatson]

Done.

[reswatson]

what code are you referring to?

Line 64 to 223.

[reswatson]

what code are you referring to?

Maybe the thing to do is just remove the auto-generated proof that R** = R (lines 129 to 162)? It doesn't need two proofs. The hand-written version on line 192 [This is now line 157] is more instructive anyway.

[reswatson]

Any other comments? Maybe a maintainer should step in now?

[reswatson]

Copilot told me I could try removing subtle white-space violations with 'sed', specifically: sed -i 's/[ \t]*$//' Cubical/HITs/SetQuotients/Properties.agda. I hope that was right! If not I have a backup version.

[maxsnew]

To fix whitespace issues you can run make fix-whitespace.

[reswatson]

To fix whitespace issues you can run make fix-whitespace.

OK, I ran that as well. Should be good.

[reswatson]

@maxsnew : I guess it can be merged now