gistfile1.ml

Class dep  {T: Type} (n:nat) (t:T): Type.
Generalizable Variable c.

Axiom C : Type.
Axiom Arrows: ∀ x y: C, Type.
Axiom iso_arrows: ∀ {x y: C} (f:Arrows x y) (g: Arrows y x), Prop.
Section def.
Context (limit: C).
Class ElimLimit := limit_proj: dep 0 limit.
Class IntroLimit := make_limit: ∀ x (x_j: dep 0 x), dep 1 x → Arrows x limit.
Class Limit `{ElimLimit} `{IntroLimit} := { limit_compat :> dep 1 limit }.
End def.

Lemma unique `{Limit c} `{Limit c'}: iso_arrows (make_limit c c' (limit_proj c') _) (make_limit c' c (limit_proj c) _).
(* is there any Ltac code that can do this, without knowing the structure of the fold function, and in particular without knowing
   the number dependent parameters? *)
change (iso_arrows
      ((fun x I1 I2 I3 x' I1' I2' I3' => make_limit x x' (limit_proj x') (limit_compat x')) c H H0 H1 c' H2 H3 H4)
      ((fun x I1 I2 I3 x' I1' I2' I3' => make_limit x x' (limit_proj x') (limit_compat x')) c' H2 H3 H4 c H H0 H1)
      ).
   match goal with 
      | [ |- iso_arrows (?f c _ _ _ c' _ _ _) (?f c' _ _ _ c _ _ _) ] => pose f as P; fold P
   end.