- apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto.
-
- intros; unfold eqv; simpl; auto.
-
- intros; unfold eqv; simpl; auto.
-
- intros; unfold eqv; simpl.
- apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- setoid_rewrite ndr_comp_left_identity.
- setoid_rewrite ndr_comp_right_identity.
- apply ndr_prod_respects; try reflexivity.
- apply ndr_structural_indistinguishable; auto.
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- setoid_rewrite ndr_comp_left_identity.
- setoid_rewrite ndr_comp_right_identity.
- apply ndr_prod_respects; try reflexivity.
- apply ndr_structural_indistinguishable; auto.
-
- intros; unfold eqv; simpl.
- apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- setoid_rewrite ndr_comp_left_identity.
- setoid_rewrite ndr_comp_right_identity.
- apply ndr_prod_respects; try reflexivity.
- apply ndr_structural_indistinguishable; auto.
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- setoid_rewrite ndr_comp_left_identity.
- setoid_rewrite ndr_comp_right_identity.
- apply ndr_prod_respects; try reflexivity.
- apply ndr_structural_indistinguishable; auto.
-
- intros; unfold eqv; simpl.
- apply Build_CentralMorphism; intros; unfold eqv; simpl in *; auto.
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- setoid_rewrite ndr_comp_left_identity.
- setoid_rewrite ndr_comp_right_identity.
- apply ndr_prod_respects; try reflexivity.
- apply ndr_structural_indistinguishable; auto.
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- symmetry.
- etransitivity; [ idtac | apply ndr_prod_preserves_comp ].
- setoid_rewrite ndr_comp_left_identity.
- setoid_rewrite ndr_comp_right_identity.
- apply ndr_prod_respects; try reflexivity.
- apply ndr_structural_indistinguishable; auto.
-