Recent versions of base have type families `&&`

and `||`

on kind `Bool`

.

Can we do type-level logic with them? I’d like to use the facts that `&&`

and `||`

are the categorical product and coproduct on the following

category.

```
data HomBool (x :: Bool) (y :: Bool) where
Id :: HomBool x x
ExFalso :: HomBool 'False 'True
instance Category HomBool where
id = Id
Id . f = f
f . Id = f
```

To that end, we would e.g. need to define a homomorphism

```
homFst :: HomBool (x && y) x
```

but that seems to require pattern-matching on the type of `(x && y)`

which (a) type families don’t support, (b) GHC won’t even accept the

type signature because `&&`

is not injective.

Similar problems arise when considering deMorgan laws for the two type

families. I remember there exist quite complete libraries for type-level

arithmetic theorems. Has anyone implemented theorems for kind `Bool`

?