[Agda] dependent equality in Cubical Agda

[James Wood]

Hi Vlad,

I was able to find a fairly direct proof. The key is that it'd be really 
nice if the second path were a PathP instead of a subst + a path. Notice 
(where `p [ x ≡ y ]` is another notation for `PathP p x y`):

Σ-intro-≡P :
   ∀ {a b} {A : Type a} {B : A → Type b} {x x′ : A} {y : B x} {y′ : B x′} →
   Σ (x ≡ x′) (λ p → (λ i → B (p i)) [ y ≡ y′ ]) →
   Path (Σ A B) (x , y) (x′ , y′)
Σ-intro-≡P (p , q) i = p i , q i

This works because B (p i0) = B x and B (p i1) = B x′, making the type 
of q match up, and then q i0 = y and q i1 = y′, which is what we needed 
in terms of values.

To retool this to subst + ≡, we use `toPathP`. Here is the full file:

{-# OPTIONS --cubical --safe #-}
module Scratch where

open import Data.Product
open import Cubical.Foundations.Everything

Σ-intro-≡ :
   ∀ {a b} {A : Type a} {B : A → Type b} {x x′ : A} {y : B x} {y′ : B x′} →
   Σ (x ≡ x′) (λ p → subst B p y ≡ y′) → Path (Σ A B) (x , y) (x′ , y′)
Σ-intro-≡ {B = B} (p , q) i = p i , toPathP {A = λ i → B (p i)} q i

All the best,
James

On 19/01/2021 19:55, Vlad Rusu wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
> Dear all,
> 
> Is there a Cubical Agda equivalent of the following Agda statement for 
> dependent equality ? With appropriate imports the statement is accepted 
> by Cubical Agda. Obviously, the proof is not.
> 
> Best regards,
> 
>   - Vlad
> 
> |Σ-≡-intro : ∀ {α β}{A : Set α}{B : A → Set β}{a a' : A}{b : B a}{b' : B 
> a'} → (Σ (a ≡ a') λ p → subst B p b ≡ b') → (a , b) ≡ (a' , b') 
> Σ-≡-intro (refl , refl) = refl |
> ||
> 
> |
> |
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>