for the few of us.

An indcutive type μF is simulated by forall x . (F x -> x) -> x, while a coinductive type νF is simulatd by exists x . (x -> F x, x). When they coincide, we can build hylomorphisms, but also introduces non-termination into the language.

Proving De Morgan’s laws and the double negation law in boolean algebra. Notes taken while listening to Max’s course on logic.