[Agda] heterogeneous equality, library functions

[Florent Balestrieri]

Hello,
I feel that some of the library functions dealing with heterogeneous 
equality could be made more general.
Especially the `subst2' function which actually (lib 2.2.7) takes a 
predicate `P : A -> B -> Set' when it could instead use a dependant type 
`P : (x : A) -> B x -> Set'.
The `cong2' function already used dependent types, but then it asked for 
an hetero equality on `x' and `y' which both have the same type `A' so I 
made it a propositional equality instead. It makes life easier because I 
was always converting from prop to hetero for this argument.
I also generalised the datatype Inspect, although I'm not sure about its 
usefulness ; but I definitely needed the generalised subst.

Attached is a module with some replacement definitions for the above 
functions.
-- Florent

-------------- next part --------------
{-# OPTIONS --universe-polymorphism #-}

module Extra.HeteroEq where

open import Level
  using (Level ; suc ; _⊔_)

open import Relation.Binary.PropositionalEquality
  using ( _≡_ ; refl )

open import Relation.Binary.HeterogeneousEquality
 using ( _â‰
_ ; refl )

------------------------------------------------------------
substâ‚‚
  : {a b c : Level}
    {A : Set a}
    {B : A → Set b}
    (C : (x : A) → B x → Set c)
    {x₁ x₂ : A}
    {y₁ : B x₁}
    {yâ‚‚ : B xâ‚‚}
  → x₁ ≡ x₂
  → y₁ â‰
 yâ‚‚
  → C x₁ y₁
  → C x₂ y₂

substâ‚‚ _ refl refl c
  = c

subst₃
  : {a b c d : Level}
    {A : Set a}
    {B : A → Set b}
    {C : (x : A) → B x → Set c}
    (D : (x : A) → (y : B x) → C x y → Set d)
    {x₁ x₂ : A}
    {y₁ : B x₁}
    {yâ‚‚ : B xâ‚‚}
    {z₁ : C x₁ y₁}
    {zâ‚‚ : C xâ‚‚ yâ‚‚}
  → x₁ ≡ x₂
  → y₁ â‰
 yâ‚‚
  → z₁ â‰
 zâ‚‚
  → D x₁ y₁ z₁
  → D x₂ y₂ z₂

subst₃ _ refl refl refl d
  = d

------------------------------------------------------------
substâ‚‚-removable
  : {a b c : Level}
    {A : Set a}
    {B : A → Set b}
    (C : (x : A) → B x → Set c)
    {x₁ x₂ : A}
    {y₁ : B x₁}
    {yâ‚‚ : B xâ‚‚}
    (x : x₁ ≡ x₂)
    (y : y₁ â‰
 yâ‚‚)
    (t : C x₁ y₁)
  → substâ‚‚ C x y t â‰
 t

substâ‚‚-removable _ refl refl t
  = refl

subst₃-removable
  : {a b c d : Level}
    {A : Set a}
    {B : A → Set b}
    {C : (x : A) → B x → Set c}
    (D : (x : A) → (y : B x) → C x y → Set d)
    {x₁ x₂ : A}
    {y₁ : B x₁}
    {yâ‚‚ : B xâ‚‚}
    {z₁ : C x₁ y₁}
    {zâ‚‚ : C xâ‚‚ yâ‚‚}
    (x : x₁ ≡ x₂)
    (y : y₁ â‰
 yâ‚‚)
    (z : z₁ â‰
 zâ‚‚)
    (t : D x₁ y₁ z₁)
  → subst₃ D x y z t â‰
 t

subst₃-removable _ refl refl refl t
  = refl

------------------------------------------------------------
congâ‚‚
  : {a b c : Level}
    {A : Set a}
    {B : A → Set b}
    {C : (x : A) → B x → Set c}
    (f : (x : A) → (y : B x) → C x y)
    {x₁ x₂ : A}
    {y₁ : B x₁}
    {yâ‚‚ : B xâ‚‚}
  → x₁ ≡ x₂
  → y₁ â‰
 yâ‚‚
  → f x₁ y₁ â‰
 f xâ‚‚ yâ‚‚

congâ‚‚ f refl refl
  = refl

cong₃
  : {a b c d : Level}  
    {A : Set a}
    {B : A → Set b}
    {C : (x : A) → B x → Set c}
    {D : (x : A) → (y : B x) → C x y → Set d}
    (f : (x : A) → (y : B x) → (z : C x y) → D x y z)
    {x₁ x₂ : A}
    {y₁ : B x₁}
    {yâ‚‚ : B xâ‚‚}
    {z₁ : C x₁ y₁}
    {zâ‚‚ : C xâ‚‚ yâ‚‚}
  → x₁ ≡ x₂
  → y₁ â‰
 yâ‚‚
  → z₁ â‰
 zâ‚‚
  → f x₁ y₁ z₁ â‰
 f xâ‚‚ yâ‚‚ zâ‚‚

cong₃ f refl refl refl
  = refl

------------------------------------------------------------
data Inspect {a b : Level} {A : Set a} (x : A)
  : Set (a ⊔ suc b)
  where
  _with-â‰
_ : {B : Set b} (y : B) (eq : y â‰
 x) → Inspect x

inspect : ∀ {a} {A : Set a} (x : A) → Inspect x
inspect x = x with-â‰
 refl