Abt.Class.HEq1

Documentation

data a :=: b where

Essentially, Martin-Löf's identity type.

Constructors

Refl :: a :=: a

cong :: (a :=: b) -> f a :=: f b

Type constructors are extensional.

class HEq1 f where

Uniform variant of Eq for indexed types. This is different from Eq1 in that it is properly kind polymorphic and crucially heterogeneous, and it places no constraint on the index. Because it is heterogeneous, it is useful to project equality in the base space from equality in the total space.

Minimal complete definition

heq1

Methods

heq1 :: f i -> f j -> Maybe (i :=: j)

When both sides are equal, give in addition a proof that their indices are equal; otherwise return Nothing.

(===) :: f i -> f j -> Bool

A boolean version of heq1, which must agree with it.

Instances

HEq1 [Nat] o => HEq1 Nat (Tm o)

HEq1 [Nat] Lang

HEq1 k el => HEq1 [k] (Rec k el)