Two types are said to be isomorphic (denoted by ) when they contain the same information. More formally, iff there exists bijective functions and between them and invert each other. See also isomorphism tags:TypeTheory