The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

In the code below I'm trying to develop a notion of "isomorphism" that allows
for rewriting. However, I'm getting a strange error that I can't yet make any
sense of:

    Error: Illegal application: 
    The term "@flip" of type "∀ A B C : Type, (A → B → C) → B → A → C"
    cannot be applied to the terms
     "Type" : "Type"
     "Type" : "Type"
     "Type" : "Type"
     "arrow" : "Type → Type → Type"
    The 4th term has type
     "Type@{Top.8164} → Type@{Top.8165} → Type@{max(Top.8164, Top.8165)}"
    which should be coercible to
     "Type@{max(Coq.Classes.CEquivalence.6, Top.4)}
      → Type@{max(Coq.Classes.CEquivalence.6, Top.4)} → Type@{Top.8166}".

If instead I use transitivity, the same proof passes easily.

Below is the test case, if anyone has any thoughts.

Thank you,
  John

Require Export
  Coq.Unicode.Utf8
  Coq.Program.Program
  Coq.Classes.CEquivalence.

Close Scope nat_scope.

Notation "f ≈ g" := (equiv f g) (at level 79, only parsing).

Reserved Infix "~>" (at level 90, right associativity).
Reserved Infix "∘" (at level 40, left associativity).

Class Category := {
  ob : Type;

  uhom := Type : Type;
  hom : ob -> ob -> uhom where "a ~> b" := (hom a b);

  id {A} : A ~> A;
  compose {A B C} (f: B ~> C) (g : A ~> B) : A ~> C
    where "f ∘ g" := (compose f g);

  id_left  {X Y} (f : X ~> Y) : id ∘ f ≈ f;

  comp_assoc {X Y Z W} (f : Z ~> W) (g : Y ~> Z) (h : X ~> Y) :
    f ∘ (g ∘ h) ≈ (f ∘ g) ∘ h
}.

Notation "X ~> Y" := (@hom _ X Y) (at level 90, right associativity).
Notation "f ∘ g" := (@compose _ _ _ _ f g).

Coercion ob : Category >-> Sortclass.

Class Isomorphism `{C : Category} (X Y : C) : Type := {
  to   :> X ~> Y;
  from :  Y ~> X;

  iso_to_from : to ∘ from ≈ id;
  iso_from_to : from ∘ to ≈ id
}.

Ltac reassoc f :=
  repeat match goal with
    | [ |- context[(?F ∘ f) ∘ ?G] ] => rewrite <- (comp_assoc F f G)
    | [ |- context[f ∘ (?G ∘ ?H)] ] => rewrite (comp_assoc f G H)
    end.

Program Instance isomorphism_equivalence `{C : Category} :
  Equivalence Isomorphism.
Next Obligation.
  repeat intro.
  apply Build_Isomorphism with (to:=id) (from:=id);
  rewrite id_left; reflexivity.
Defined.
Next Obligation.
  repeat intro; destruct X.
  apply Build_Isomorphism with (to:=from0) (from:=to0); assumption.
Defined.
Next Obligation.
  repeat intro; destruct X, X0.
  apply Build_Isomorphism with (to:=to1 ∘ to0) (from:=from0 ∘ from1).
    repeat match goal with
    | [ H : equiv (?F ∘ ?G) _
      |- context[(_ ∘ ?F) ∘ (?G ∘ _)] ] => reassoc F; rewrite H
    | [ H : equiv (?F ∘ ?G) _
      |- context[?F ∘ (?G ∘ _)] ] => reassoc F; rewrite H
    | [ H : equiv (?F ∘ ?G) _
      |- context[(_ ∘ ?F) ∘ ?G] ] => reassoc F; rewrite H
    | [ H : equiv (?F ∘ ?G) _
      |- context[?F ∘ ?G] ] => rewrite H
    | [ |- equiv ?F ?F ] => reflexivity
    | [ |- context[id ∘ ?F] ] => rewrite (id_left F)
    end.
  reassoc from1; rewrite iso_from_to1.
  rewrite id_left; assumption.
Defined.

Notation "X ≅ Y" := (@Isomorphism _ X Y) (at level 91).

Goal forall `{C : Category} {X Y Z : C} (f : Y ≅ Z) (g : X ≅ Y), X ≅ Z.
  intros.
  (* transitivity Y; auto. *)
  rewrite g.
-- 
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2