Sets-as-Types, Functions-as-Terms Algebra-as-Types, Morphisms-as-Terms Coalgebra-as-Types, Morphisms-as-Terms Categories-as-Types, Functors-as-Terms Propositions-as-Types, Proofs-as-Terms Sets-as-Types と (Co)Algebras-as-Types は、単純型＝…