поправка про изоморфизмы

Я в предыдущем посте всех обманул, а меня никто не поправил опять. Я сказал, что если на коммутирующей диаграмме между двумя объектами есть стрелки туда-сюда, то они получаются изоморфизмами. Однако ж нифига, и вот простой контрпример. Возьмем объект А и его произведение с самим собой АхА:

По определению произведения из АхА есть стрелки fst и snd в А, и для любого объекта (например, А), из которого тоже есть стрелки f и g в А (например, f=g=id), есть уникальная стрелка pair(f,g) из этого объекта (А) в АхА, такая, что fst . pair(f,g) = f и snd . pair(f,g) = g, т.е. fst . pair(id,id) = id.
В CPL pair(id,id) имеет тип *a -> prod(*a,*a), а fst имеет тип prod(*a,*b) -> *a, и их композиция fst . pair(id,id) равна id, это нам дает определение произведения. Но вот обратная композиция pair(id,id) . fst нифига не равна id. А значит, определение изоморфизма не вывполнено, и А не изоморфен АхА, что и следовало ожидать. Так что построение стрелок на CPL туда-сюда еще не доказывает изоморфность, нужно явно показать, что обе их композиции равны соответствующим id. Упомянутые в прошлом посте изоморфизмы, дающие арифметические законы, остаются в силе, просто обоснования там неполные, не хватает кое-каких доказательств.