Prop vs. Set vs. Type

これを見ればカリー・ハワード対応の神髄が見える……かもしれない。

そのものの種類での比較
`Prop`	`Set`	`Type`
`I : True`	`tt : unit`
`False`	`Empty_set`
	`true, false : bool`
		`Some _, None : option A`
`or_introl _, or_intror _ : or P Q`	`left _, right _ : sumbool P Q`	`inl _, inr _ : sum A B` `inleft _, inright _ : sumor A Q`
`conj _ _ : and P Q`		`pair _ _ : prod A B`
`proj1 : and P Q -> P`		`fst : prod A B -> A`
`proj2 : and P Q -> Q`		`snd : prod A B -> B`
`ex_intro _ : ex P`		`exist _ : sig P` `existT _ : sigT B`
		`proj1_sig : sig P -> A` `projT1 : sigT B -> A`
		`proj2_sig : sig P -> P x` `projT2 : sigT B -> B x`
`ex_intro2 _ : ex2 P Q`		`exist2 _ : sig2 P Q` `existT2 _ : sigT2 B C`
`refl_equal : eq a a`		`refl_identity : identity a a`
`inhabits _ : inhabited A`

引数の種類での比較
`Prop`	`Type`
`not : Prop -> Prop`	`notT : Type -> Prop`
`sig : forall A : Type, (A -> Prop) -> Type`	`sigT : forall A : Type, (A -> Type) -> Type`