Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data IxEq :: (k -> Type) -> k -> k -> Type where
- data Inject :: (k -> Type) -> k -> k -> Type where
- InjectRefl :: forall f a b. IxEq f a b -> Inject f a b
- CompactCompose :: forall f i j. IxEq f i i -> IxEq f j j -> Natural -> Inject f i j
- newtype Extract :: (k -> Type) -> k -> k -> Type where
- data TreeEq :: (k -> Type) -> k -> k -> Type where
- TreeInject :: Inject f a b -> TreeEq f a b
- TreeExtract :: Extract f a b -> TreeEq f a b
- TreeRefl :: TreeEq f c c
- treeElimination :: TestEquality f => Inject f a b -> Extract f b c -> TreeEq f a c
Documentation
data IxEq :: (k -> Type) -> k -> k -> Type where Source #
TestEquality k f => TestEquality k (IxEq k f i) Source # | |
data Inject :: (k -> Type) -> k -> k -> Type where Source #
Inject
is about
InjectRefl :: forall f a b. IxEq f a b -> Inject f a b | |
CompactCompose :: forall f i j. IxEq f i i -> IxEq f j j -> Natural -> Inject f i j |
Semigroupoid k (Inject k f) Source # | |
newtype Extract :: (k -> Type) -> k -> k -> Type where Source #
Semigroupoid k (Extract k f) Source # | |
data TreeEq :: (k -> Type) -> k -> k -> Type where Source #
TreeInject :: Inject f a b -> TreeEq f a b | |
TreeExtract :: Extract f a b -> TreeEq f a b | |
TreeRefl :: TreeEq f c c |
treeElimination :: TestEquality f => Inject f a b -> Extract f b c -> TreeEq f a c Source #