- intros.
- simpl.
- destruct f; simpl.
- apply if_id.
- destruct g; simpl.
- apply if_id.
- unfold mf_f; simpl.
- apply (if_respects
- (F0:=((garrow_functor s1 s0 r >>>> RepresentableFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0))
- (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0)))
- (G0:=(RepresentableFunctor s2 (mon_i s2)))
- (G1:=(RepresentableFunctor s2 (mon_i s2))));
- [ idtac | apply if_id ].
- eapply if_comp.
- idtac.
- apply (if_associativity (garrow_functor s1 s0 r) (RepresentableFunctor s0 (mon_i s0)) (garrow_functor s0 s2 r0)).
- Set Printing Coercions.
- idtac.
- unfold garrow_functor at 1.
- unfold step2_functor at 1.
- set (roundtrip_lemma'
- (RepresentableFunctor (enr_c (smme_e s0)) (me_i (smme_mon s0)))
- (ffme_mf_full (smme_mee s0)) (ffme_mf_faithful (smme_mee s0))
- (step1_functor (smme_see s1) (smme_mee s0) r)
- ) as q.
- set (if_respects
- (G0:=garrow_functor (smme_see s0) (smme_mee s2) r0)
- (G1:=garrow_functor (smme_see s0) (smme_mee s2) r0)
- q (if_id _)) as q'.
- apply (if_comp q').
- Unset Printing Coercions.
- clear q' q.
- unfold garrow_functor at 2.
- unfold garrow_functor at 1.
- eapply if_comp.
- eapply if_inv.
- apply (if_associativity _ (step1_functor s0 s2 r0) (step2_functor s2)).
- apply (if_respects
- (G0:=step2_functor s2)
- (G1:=step2_functor s2)); [ idtac | apply if_id ].
- apply step1_lemma.
- Defined.
+ intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros.
+ apply M2_respects; auto.
+ unfold fmor; simpl.
+ apply (@eqv1 _ _ f0 f0).
+ apply if_id.
+ unfold fmor; simpl.
+ apply (@eqv2 _ _ f0 f0).
+ apply if_id.
+ Defined.