+ Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) :=
+ { iso_forward := nd_seq_reflexive _ ;; tsr_ant_cossa _ a b c
+ ; iso_backward := nd_seq_reflexive _ ;; tsr_ant_assoc _ a b c
+ }.
+ admit.
+ admit.
+ 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 }.
+ admit.
+ Defined.
+
+ Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a :=
+ { iso_forward := nd_seq_reflexive _ ;; tsr_ant_rlecnac _ a
+ ; iso_backward := nd_seq_reflexive _ ;; tsr_ant_cancelr _ a
+ }.
+ admit.