Since you are all functionally inclined. In the c...

# functional

[raulraja]

Since you are all functionally inclined.
In the category of the Kotlin types where the morphisms are the functions type proofs establishes a trust relationship with the Kotlin compiler where you can tell it you know the path between two types and the implication that has. The arrow prelude demonstrates the Kotlin type system can be extended by providing a custom typechecker based on proofs that eliminate the need for inheritance by exploiting subtype Polymorphism and the top Any? and bottom types Nothing. In Kotlin we can have value holes we can fill in with type proofs in any expression position.