Equality in the PDF

[WhatisRT]

This is somewhat similar to #281 and related to #241. We need some consistent strategy for how to deal with equalities. In particular: Do we assume/pretend to have/use (e.g. via --erased-cubical) quotients?

Here are some equalities we're using:

• [ ] _≡_
• [ ] _≗_
• [ ] _≡ᵉ_

Note: this issue is only for the presentation. The underlying problem of what to actually do in Agda is a much bigger, separate task.

[WhatisRT]

For reference, here's one way how to do quotients in --erased-cubical:

{-# OPTIONS --safe --erased-cubical #-}

module Quotients where

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical

record Quotient (A : Set) (_≈_ : A → A → Set) : Set₁ where
  field Q : Set
        proj : A → Q
        factor : {B : Set} → (f : A → B) → (f-cong : ∀ {a₁ a₂} → a₁ ≈ a₂ → f a₁ ≡ f a₂) → Q → B
open Quotient

module _ (A : Set) (_≈_ : A → A → Set) where

  data Quot : Set where
    [_] : A → Quot
    eq  : (a₁ a₂ : A) → a₁ ≈ a₂ → [ a₁ ] ≡ [ a₂ ]

  mkQuotient : Quotient A _≈_
  mkQuotient .Q = Quot
  mkQuotient .proj = [_]
  mkQuotient .factor f cong [ x ] = f x
  mkQuotient .factor f cong (eq a₁ a₂ x i) = cong x i

It would be a cool project to try and use this to fix this issue. I don't know if this would break anything, but if this works we could rid ourselves of setoids entirely.

[williamdemeo]

I like it! 🚀

I'd be happy to try this and see whether we can adopt it across the board without breaking anything and without the use of setoids... but first I'll see if there are other, higher-priority, lower-hanging fruit in the list of issues.

[WhatisRT]

Yeah, I think this is something for next year when we have more breathing room. Also, I realized that we can't import Relation.Binary.PropositionalEquality with --erased-cubical, so taking this route would actually be a huge task.