proposition: Lemma to_from {a b c} : Basics.compose to from = @Datatypes.id (a → option (b → option c)).
proof: Proof. extensionality f. simpl. extensionality x. unfold to, from. destruct (f x). - f_equal. - Abort. Lemma to_from_impossible {a b c} : Basics.compose to from = @Datatypes.id (a → option (b → option c)) → inhabited a → False. Proof. intros. pose proof (equal_f H). pose proof (equal_f (H1 (fun _ => None))). simpl in H2. destruct H0. specialize (H2 X). unfold to, from in H2. discriminate. Qed.
imports: Category.Lib Category.Theory.Category Category.Instance.Sets Category.Structure.Cartesian