proposition: Proposition univ_property_unique_up_to_unique_iso (c d : C) (t : P c) (s : P d) : Unique (fun p : (c ≅ d) => univ_property_respects_iso c d p t ≈ s).
proof: Proof. exists (uniqueness (univ_property_unique c t) d s). - abstract(simpl; unfold univ_property_respects_iso; simpl; rapply (snd (injectivity_is_monic _) (iso_to_monic (repr_equivalence d))); set (M := (iso_to_from (repr_equivalence d))); simpl in M; rewrite M; clear M; apply to_equiv_implies_iso_equiv; intros j u; simpl in u; simpl; set (ab := (to (repr_equivalence c )) ); assert (K := @naturality _ _ _ _ (to (ab t)) _ _ u); simpl in K; rewrite <- K; clear K; set (A := iso_to_from (ab t) d); simpl in A; unfold op; rewrite A; clear A; set (aj := to (repr_equivalence d )); set (aj' := to (aj s)); change (@id C d) with (@id (C^op) d); rewrite <- 2 (@preyoneda (C^op) _ _ repr_functor aj'); reflexivity). - abstract(intros v respects_iso; simpl uniqueness; apply to_equiv_implies_iso_equiv; simpl; unfold univ_property_respects_iso, Equivalence_Transitive in respects_iso; simpl in respects_iso; set (v' := iso_sym (Isomorphism_Opposite v)) in *; set (yv := fobj_iso C d c v') in *; rewrite <- (id_left (to v)); change (id{C} ∘ to v) with (to yv d id{C}); change (from (to (repr_equivalence c) t) d (to (to (repr_equivalence d) s) d id)) with (((from (to (repr_equivalence c) t)) ∘ (to (to (repr_equivalence d) s))) d id); cut ((iso_sym (to (repr_equivalence c) t)) ⊙ ( (to (repr_equivalence d) s)) ≈ yv); [ intro a; destruct a as [a _]; simpl in a; apply a |]; apply (@proper_morphism _ _ _ _ (to (repr_equivalence d))) in respects_iso; assert (K := (iso_to_from (repr_equivalence d))); simpl in K; rewrite K in respects_iso; clear K; apply (@compose_respects (Groupoid (@Fun.Fun C Sets)) _ _ _ (iso_sym (to (repr_equivalence c) t)) (iso_sym (to (repr_equivalence c) t)) (Equivalence_Reflexive _ )) in respects_iso; rewrite comp_assoc in respects_iso; simpl in respects_iso; rewrite iso_sym_left_inverse in respects_iso; change iso_id with (@id (Groupoid (@Fun.Fun C Sets)) (fobj[C] c)) in respects_iso; rewrite (@id_left (Groupoid (@Fun.Fun C Sets))) in respects_iso; symmetry in respects_iso; exact respects_iso). Defined.
imports: Category.Lib Category.Lib.Tactics2 Category.Theory.Category Category.Theory.Isomorphism Category.Construction.Opposite Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Hom Category.Functor.Hom.Yoneda Category.Instance.Sets Category.Construction.Groupoid