[Agda] dependent equality in Cubical Agda

[Vlad Rusu]

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 |
||

|
|
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210119/33e08eed/attachment.html>