proposition: Lemma left_inverse_unique (X : C) (f : X ~> grp) (f_inv : X ~> grp) (f_left_inverse : mappend ∘ f_inv ⨂ f ∘ ∆ X ≈ mempty ∘ eliminate) : f_inv ≈ inverse[grp] ∘ f.
proof: Proof. rewrite <- (id_left f_inv). rewrite <- mempty_right_diagonal. rewrite <- (comp_assoc _ ∆grp f_inv). rewrite <- (diagonal_natural _ _ f_inv); simpl. rewrite !comp_assoc; rewrite <- (comp_assoc _ (_ ⨂ _) (_ ⨂ _)). rewrite <- bimap_comp. rewrite <- (comp_assoc _ eliminate _). rewrite (unit_terminal (eliminate ∘ f_inv) (eliminate ∘ f)). rewrite !comp_assoc. rewrite <- right_inverse. assert (mappend ∘ id ⨂ inverse[grp] ∘ ∆grp ∘ f ≈ mappend ∘ (id ⨂ inverse[grp] ∘ ∆grp ∘ f)) as R by (rewrite comp_assoc; cat); rewrite R; clear R. rewrite bimap_comp. rewrite !comp_assoc. rewrite mappend_assoc_sym. rewrite <- (comp_assoc _ _ f). rewrite <- (diagonal_natural _ _ f); simpl. rewrite !comp_assoc. rewrite <- bimap_comp; rewrite id_left. rewrite <- (id_right f_inv). rewrite bimap_comp. rewrite !comp_assoc; rewrite <- (comp_assoc _ (tensor_assoc ⁻¹) _). rewrite <- from_tensor_assoc_natural. rewrite !comp_assoc; rewrite <- (comp_assoc _ (id ⨂ ∆X) (∆X)). rewrite diagonal_tensor_assoc. rewrite <- (comp_assoc tensor_assoc _ _); rewrite (comp_assoc _ tensor_assoc _); rewrite <- (comp_assoc _ (tensor_assoc ⁻¹) _). rewrite iso_from_to; rewrite id_right. rewrite !comp_assoc; rewrite <- 2!(comp_assoc mappend _ _). rewrite <- 2!bimap_comp; rewrite id_right. rewrite !comp_assoc. rewrite f_left_inverse. rewrite (unit_terminal eliminate (eliminate ∘ (inverse[grp] ∘ f))). rewrite !comp_assoc; rewrite <- 2!(comp_assoc _ inverse[grp] f). rewrite bimap_comp. rewrite <- (comp_assoc _ _ ∆X). assert ((inverse[grp] ∘ f) ⨂ (inverse[grp] ∘ f) ≈ map (inverse[grp] ∘ f)) as R by reflexivity; rewrite R; clear R. rewrite <- (comp_assoc _ _ ∆X). rewrite (diagonal_natural _ _ (inverse[grp] ∘ f)). simpl. rewrite !comp_assoc. rewrite mempty_left_diagonal. cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Naturality Category.Functor.Bifunctor Category.Structure.Monoidal.Proofs Category.Structure.Monoidal.Cartesian Category.Structure.Monoid Category.Structure.Group