- destruct a as [[a1 a1'] [a2 a2']].
- destruct b as [[b1 b1'] [b2 b2']].
- destruct c as [[c1 c1'] [c2 c2']].
- destruct f as [[f1 f1'] [f2 f2']].
- destruct g as [[g1 g1'] [g2 g2']].
- simpl in *.
- setoid_rewrite juggle3.
- setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')).
- setoid_rewrite <- juggle3.
- setoid_rewrite <- fmor_preserves_comp.
- reflexivity.
- Defined.
-
- Definition center_I : Center mc := exist _ pI I.
-
- Definition center_cancelr : (func_rlecnac center_I >>>> CenterMonoidal_F) <~~~> functor_id (Center mc).
- Definition center_cancelr_niso : ∀A : Center mc, CenterMonoidal_Fobj (pair_obj A center_I) ≅ A.
- intros.
- destruct A; simpl.
- set (ni_iso (pmon_cancelr mc) x) as q.
- (*refine {| iso_forward := #q ; iso_backward := iso_backward q |}.*)
- admit.
- Defined.
- refine {| ni_iso := center_cancelr_niso |}.
- admit.
- Defined.
-
- Definition center_cancell : (func_llecnac center_I >>>> CenterMonoidal_F) <~~~> functor_id (Center mc).
- Definition center_cancell_niso : ∀A : Center mc, CenterMonoidal_Fobj (pair_obj center_I A) ≅ A.
- admit.
- Defined.
- refine {| ni_iso := center_cancell_niso |}.
- admit.