Type of a subSetoid

Question

Is there a way for a function to ask for two Setoids where equality in the first Setoid implies equality in the latter? Of course this requires that both Setoids share their Carrier and Carrier is not a parameter, but a record field instead. A naive attempt to request Carrier equality gets rejected by the type checker:

f : {S₁ S₂ : Setoid _ _} → Setoid.Carrier S₁ ≡ Setoid.Carrier S₂ →
    ({x y : Setoid.Carrier S₁} → Setoid._≈_ S₁ x y → Setoid._≈_ S₂ x y ) → ...

This does not work, because we do not pattern match on the equality proof, so the different Carrier types are not unified. I have not found a way to express this using subst.

Answer 1

You have two options. I'm using the following shortcuts:

A = Setoid.Carrier S₁
B = Setoid.Carrier S₂

You can either transport the elements x and y from A to B, or you can transport the relation Setoid._≈_ S₂ from B → B → Set _ to A → A → Set _.

Transporting elements can be done via subst id:

f : ∀ {c ℓ} {S₁ S₂ : Setoid c ℓ}
    (p : Setoid.Carrier S₁ ≡ Setoid.Carrier S₂) →
    (∀ {x y} → Setoid._≈_ S₁ x y →
               Setoid._≈_ S₂ (subst id p x) (subst id p y)) →
    ?

Notice that subst id : A ≡ B → A → B (roughly).

Transporting the whole relation can then be done via subst (λ x → x → x → Set _). We start with B → B → Set _, so we need a proof B ≡ A instead of A ≡ B - that's why we use sym:

g : ∀ {c ℓ} {S₁ S₂ : Setoid c ℓ}
    (p : Setoid.Carrier S₁ ≡ Setoid.Carrier S₂) →
    (∀ {x y} → Setoid._≈_ S₁ x y →
               subst (λ x → x → x → Set _) (sym p) (Setoid._≈_ S₂) x y) →
    ?

---

It's hard to tell which one will be easier to work with. Another option is to work directly with IsEquivalence, this allows you to simply force the relations to be over the same domain:

h : ∀ {a ℓ} {A : Set a} {_≈₁_ _≈₂_ : Rel A ℓ}
    {E₁ : IsEquivalence _≈₁_} {E₂ : IsEquivalence _≈₂_} →
    (∀ {x y} → x ≈₁ y → x ≈₂ y) →
    ?