proposition: Lemma bijective_is_iso {A B : SetoidObject} (h : A ~{Sets}~> B) : injective h -> surjective h -> IsIsomorphism h.
proof: Proof. intros [i] [lift] ; unshelve econstructor. - exists (fun b => `1 (lift b)). abstract(intros a b eq; simpl; apply i; now rewrite `2 (lift a), `2 (lift b)). - abstract(intro x; now rewrite `2 (lift x)). - abstract(intro x; apply i; now rewrite `2 (lift (h x))). Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Functor Category.Theory.Isomorphism Category.Structure.Terminal Category.Structure.Initial Category.Structure.Monoidal