proposition: Lemma from_to {a b c} : Basics.compose from to = @Datatypes.id (a + (b + (a * b)) → option c).
proof: Proof. extensionality f. simpl. extensionality x. unfold to, from. destruct x; simpl. - admit. - destruct s; simpl. + admit. + destruct p; auto. Abort. Lemma from_to_impossible {a b c} : Basics.compose from to = @Datatypes.id (a + (b + (a * b)) → option c) → inhabited a ∨ inhabited b → inhabited c → False. Proof. intros. pose proof (equal_f H). destruct H1. pose proof (equal_f (H2 (fun _ => Some X))). simpl in H1. unfold to, from in H1. destruct H0, i. - specialize (H1 (inl X0)). discriminate. - specialize (H1 (inr (inl X0))). discriminate. Qed.
imports: Category.Lib Category.Theory.Category Category.Instance.Sets Category.Structure.Cartesian