+data CoercionI = IdCo Type | ACo Coercion
+
+liftCoI :: (Type -> Type) -> CoercionI -> CoercionI
+liftCoI f (IdCo ty) = IdCo (f ty)
+liftCoI f (ACo ty) = ACo (f ty)
+
+liftCoI2 :: (Type -> Type -> Type) -> CoercionI -> CoercionI -> CoercionI
+liftCoI2 f (IdCo ty1) (IdCo ty2) = IdCo (f ty1 ty2)
+liftCoI2 f coi1 coi2 = ACo (f (fromCoI coi1) (fromCoI coi2))
+
+liftCoIs :: ([Type] -> Type) -> [CoercionI] -> CoercionI
+liftCoIs f cois = go_id [] cois
+ where
+ go_id rev_tys [] = IdCo (f (reverse rev_tys))
+ go_id rev_tys (IdCo ty : cois) = go_id (ty:rev_tys) cois
+ go_id rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois
+
+ go_aco rev_tys [] = ACo (f (reverse rev_tys))
+ go_aco rev_tys (IdCo ty : cois) = go_aco (ty:rev_tys) cois
+ go_aco rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois