[Agda] Heterogeneous equality of pairs and records: some questions.

[Matteo Acerbi]

Andrea Vezzosi writes:

> The right to left direction of that equality seems inconsistent with MLTT.
>
> Take
>
> A = C = Bool
> a = c = true
>
> B true = Unit
> B false = Unit
>
> D true = Unit
> D false = Bool
>
> then you can prove ((A , a ≡ C , c) × (B a , b ≡ D c , d)) so you get
> in particular Σ A B ≡ Σ C D.
>
> But  Σ A B  has 2 elements, while  Σ C D  has 3 elements, so you can
> disprove that equality.

Nice, thanks!

You answered to B, C, D, E, parts of G and H, and proved that most of
that file made little sense, as the axiom adds inhabitants to Eq Set
that lead to inconsistency.

I should have asked this here before. :-)

I now see that the difference with OTT is a crucial one, and that
DistrEqPtdΣ is not weaker as I thought, but inconsistent.

Do you think assuming `P` is safer?

record P : Set₁ where
  field
    _≅_   : {A B : Set} → A → B → Set
    _≅,_  : {A : Set}{B : A → Set}{C : Set}{D : C → Set}
            {a : A}{b : B a}{c : C}{d : D c} →
            a ≅ c → b ≅ d → _≅_ {Σ A B}{Σ C D} (a , b) (c , d)
    ≡→≅   : {A : Set}(x y : A) → x ≡ y → x ≅ y
    ≅→≡   : {A : Set}(x y : A) → x ≅ y → x ≡ y

Best,
Matteo