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

[Andrea Vezzosi]

Assuming K, you should be able to implement P by using heterogeneous
equality for _≅_.

On Tue, Oct 6, 2015 at 4:47 PM, Matteo Acerbi <matteo.acerbi at gmail.com> wrote:
>
> 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