+ Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) :=
+ { iso_forward := snd_initial _ ;; cnd_ant_cossa _ a b c
+ ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c
+ }.
+ simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
+ simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
+ Defined.
+
+ Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a :=
+ { iso_forward := snd_initial _ ;; cnd_ant_rlecnac _ a
+ ; iso_backward := snd_initial _ ;; cnd_ant_cancelr _ a
+ }.
+ unfold eqv; unfold comp; simpl.
+ eapply cndr_inert. apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
+ unfold eqv; unfold comp; simpl.
+ eapply cndr_inert. apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
+ Defined.
+
+ Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a :=
+ { iso_forward := snd_initial _ ;; cnd_ant_llecnac _ a
+ ; iso_backward := snd_initial _ ;; cnd_ant_cancell _ a
+ }.
+ unfold eqv; unfold comp; simpl.
+ eapply cndr_inert. apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
+ unfold eqv; unfold comp; simpl.
+ eapply cndr_inert. apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
+ Defined.
+
+ Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a :=
+ { ni_iso := fun c => Types_assoc_iso a c b }.
+ intros; unfold eqv; simpl.