ViewCubical.agda

{-# OPTIONS --cubical #-}

module Scratch where

open import Cubical.Foundations.Everything
open import Cubical.Data.Equality

module _ {a} {A : Type a} where

  data View {x : A} : {y : A} → x ≡ y → Type a where
    vrefl : View refl

  view : ∀ {x y} (p : x ≡ y) → View p
  view = J (λ y p → View p) vrefl

  -- Test:

  test : ∀ {x y z : A} → x ≡ y → y ≡ z → x ≡ z
  test p q with vrefl ← view p = q

  test2 : isSet A → ∀ {x y : A} (p : x ≡ y) (q : y ≡ x) → test p q ≡ refl
  test2 set p q with vrefl ← view p = set _ _ q refl