iso.v

Program Definition iso_comp_iso
        {C : Category}
        {a b c : C}
        (x : @Isomorphism C a b)
        (y : @Isomorphism C b c) :
  @Isomorphism C a c :=
  {| to := comp (to x) (to y);
     from := comp (from y) (from x)
  |}.
Next Obligation.
Proof.
  destruct x, y.
  simpl in *.
  (* Now what? *)

output.v

1 subgoal, subgoal 1 (ID 135)
  
  C : Category
  a, b, c : C
  to0 : mor a b
  from0 : mor b a
  inv_left0 : comp from0 to0 = id
  inv_right0 : comp to0 from0 = id
  to1 : mor b c
  from1 : mor c b
  inv_left1 : comp from1 to1 = id
  inv_right1 : comp to1 from1 = id
  ============================
   comp (comp from1 from0) (comp to0 to1) = id