A first attempt at using typeclasses for proving things in category theory.

AdjointPointwise.v

Require Export Adjoint.
Require Import Notations Common FunctorCategoryFunctorial Duals.

Set Implicit Arguments.

Generalizable All Variables.

Section SimplifiedMorphism.
  Section single_category.
    Context `{C : SpecializedCategory objC}.

    Class SimplifiedMorphism {s d} (m : Morphism C s d) :=
      { SimplifiedMorphismValue : Morphism C s d;
        SimplifiedMorphismOk : m = SimplifiedMorphismValue }.

    Local Ltac t := repeat rewrite <- SimplifiedMorphismOk; autorewrite with category; try reflexivity.

    Global Instance UnchangedMorphism s d (m : Morphism C s d) : SimplifiedMorphism m | 1000 :=
      {| SimplifiedMorphismValue := m;
         SimplifiedMorphismOk := eq_refl |}.

    Global Instance SimplifyLeftIdentity `(SimplifiedMorphism s d m) : SimplifiedMorphism (Compose (Identity _) m) | 10
      := {| SimplifiedMorphismValue := SimplifiedMorphismValue (m := m) |}.
    Proof. abstract t. Defined.

    Global Instance SimplifyRightIdentity `(SimplifiedMorphism s d m) : SimplifiedMorphism (Compose m (Identity _)) | 10
      := {| SimplifiedMorphismValue := SimplifiedMorphismValue (m := m) |}.
    Proof. abstract t. Defined.

    Global Instance SimplifyComposition `(SimplifiedMorphism d d' m1) `(SimplifiedMorphism s d m2)
    : SimplifiedMorphism (Compose m1 m2) | 50
      := {| SimplifiedMorphismValue := Compose (SimplifiedMorphismValue (m := m1)) (SimplifiedMorphismValue (m := m2)) |}.
    Proof. abstract t. Defined.

    Definition NormalizeLeftAssociativity `(SimplifiedMorphism s d m1) `(SimplifiedMorphism d d' m2) `(SimplifiedMorphism d' d'' m3)
    : SimplifiedMorphism (Compose m3 (Compose m2 m1)).
      refine {| SimplifiedMorphismValue := (Compose (Compose (SimplifiedMorphismValue (m := m3)) (SimplifiedMorphismValue (m := m2)))
                                                    (SimplifiedMorphismValue (m := m1))) |}.
      abstract t.
    Defined.

    Definition NormalizeRightAssociativity `(SimplifiedMorphism s d m1) `(SimplifiedMorphism d d' m2) `(SimplifiedMorphism d' d'' m3)
    : SimplifiedMorphism (Compose (Compose m3 m2) m1).
      refine {| SimplifiedMorphismValue := (Compose (SimplifiedMorphismValue (m := m3))
                                                    (Compose (SimplifiedMorphismValue (m := m2))
                                                             (SimplifiedMorphismValue (m := m1)))) |}.
      abstract t.
    Defined.
  End single_category.

  Local Ltac t := repeat rewrite <- SimplifiedMorphismOk;
                 repeat rewrite Associativity;
                 repeat rewrite FCompositionOf;
                 repeat rewrite Commutes;
                 autorewrite with category; try reflexivity.

  Section functor.
    Context `{C : SpecializedCategory objC}.
    Context `{D : SpecializedCategory objD}.
    Variable F : SpecializedFunctor C D.

    Global Instance SimplifyFIdentityOf x : SimplifiedMorphism (MorphismOf F (Identity x)) | 5
      := {| SimplifiedMorphismValue := Identity (F x) |}.
    Proof. abstract t. Defined.

    Definition NormalizeFCompositionOfRight `(SimplifiedMorphism objC C d d' m1) `(SimplifiedMorphism objC C s d m2)
    : SimplifiedMorphism (MorphismOf F (Compose m1 m2)).
      refine {| SimplifiedMorphismValue := Compose (MorphismOf F (SimplifiedMorphismValue (m := m1)))
                                                   (MorphismOf F (SimplifiedMorphismValue (m := m2))) |}.
      abstract t. Defined.

    Definition NormalizeFCompositionOfLeft `(SimplifiedMorphism objC C d d' m1) `(SimplifiedMorphism objC C s d m2)
    : SimplifiedMorphism (Compose (MorphismOf F m1) (MorphismOf F m2)).
      refine {| SimplifiedMorphismValue := MorphismOf F (Compose (SimplifiedMorphismValue (m := m1))
                                                                 (SimplifiedMorphismValue (m := m2))) |}.
      abstract t. Defined.

    Global Instance SimplifyFunctorOf `(@SimplifiedMorphism objC C s d m) : SimplifiedMorphism (MorphismOf F m) | 500
      := {| SimplifiedMorphismValue := MorphismOf F (SimplifiedMorphismValue (m := m)) |}.
    Proof. abstract t. Defined.
  End functor.

  Section natural_transformation.
    Context `{C : SpecializedCategory objC}.
    Context `{D : SpecializedCategory objD}.
    Variables F G : SpecializedFunctor C D.
    Variable T : SpecializedNaturalTransformation F G.

    Global Instance SimplifyNTOf x : SimplifiedMorphism (T x) | 500
      := {| SimplifiedMorphismValue := T x;
            SimplifiedMorphismOk := eq_refl |}.

    Definition NormalizeTCommutesRight `(SimplifiedMorphism objC C s d m)
    : SimplifiedMorphism (Compose (T d) (MorphismOf F m)).
      refine {| SimplifiedMorphismValue := SimplifiedMorphismValue (m := Compose (MorphismOf G m) (T s)) |}.
      abstract t. Defined.

    Definition NormalizeTCommutesLeft `(SimplifiedMorphism objC C s d m)
    : SimplifiedMorphism (Compose (MorphismOf G m) (T s)).
      refine {| SimplifiedMorphismValue := SimplifiedMorphismValue (m := Compose (T d) (MorphismOf F m)) |}.
      abstract t. Defined.
  End natural_transformation.
End SimplifiedMorphism.
(*
Inductive SimpleMorphism objC (C : SpecializedCategory objC) : C -> C -> Type :=
    | SimpleIdentityMorphism : forall x, SimpleMorphism C x x
    | SimpleComposedMorphism : forall s d d', SimpleMorphism C d d' -> SimpleMorphism C s d -> SimpleMorphism C s d'
    | SimpleNaturalTransformationMorphism : forall objB (B : SpecializedCategory objB)
                                                   (F G : SpecializedFunctor B C)
                                                   (T : SpecializedNaturalTransformation F G)
                                                   x,
                                              SimpleMorphism C (F x) (G x)
    | SimpleGenericMorphism : forall s d, Morphism C s d -> SimpleMorphism C s d.
    Inductive ComplicatedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
    | ComplicatedIdentityMorphism : forall objC C x, @ComplicatedMorphism objC C x x
    | ComplicatedComposedMorphism : forall objC C s d d', ComplicatedMorphism C d d' -> ComplicatedMorphism C s d -> @ComplicatedMorphism objC C s d'
    | ComplicatedNaturalTransformationMorphism : forall objB (B : SpecializedCategory objB)
                                                        objC (C : SpecializedCategory objC)
                                                        (F G : SpecializedFunctor B C)
                                                        (T : SpecializedNaturalTransformation F G)
                                                        x,
                                                   ComplicatedMorphism C (F x) (G x)
    | ComplicatedFunctorMorphism : forall objB (B : SpecializedCategory objB)
                                          objC (C : SpecializedCategory objC)
                                          (F : SpecializedFunctor B C)
                                          s d,
                                     @ComplicatedMorphism objB B s d -> @ComplicatedMorphism objC C (F s) (F d)
    | ComplicatedGenericMorphism : forall objC (C : SpecializedCategory objC) s d, Morphism C s d -> @ComplicatedMorphism objC C s d.

    Fixpoint ComplicatedMorphismDenote objC C s d (m : @ComplicatedMorphism objC C s d) : Morphism C s d :=
      match m in @ComplicatedMorphism objC C s d return Morphism C s d with
        | ComplicatedIdentityMorphism _ _ x => Identity x
        | ComplicatedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ComplicatedMorphismDenote _ _ _ _ m1)
                                                                 (@ComplicatedMorphismDenote _ _ _ _ m2)
        | ComplicatedNaturalTransformationMorphism _ _ _ _ _ _ T x => T x
        | ComplicatedFunctorMorphism _ _ _ _ F _ _ m => MorphismOf F (@ComplicatedMorphismDenote _ _ _ _ m)
        | ComplicatedGenericMorphism _ _ _ _ m => m
      end.

    Fixpoint ComplicatedMorphismSimplify0 objC C s d (m : @ComplicatedMorphism objC C s d) : ComplicatedMorphism C s d.
    refine (match m in @ComplicatedMorphism objC C s d return @ComplicatedMorphism objC C s d with
              | ComplicatedComposedMorphism objC C _ _ d m1 m2 => _
              | ComplicatedIdentityMorphism _ _ x => ComplicatedIdentityMorphism _ x
              (*| ComplicatedComposedMorphism _ _ _ _ _ m1 m2 => ComplicatedComposedMorphism m1 m2*)
              | ComplicatedNaturalTransformationMorphism _ _ _ _ _ _ T x => ComplicatedNaturalTransformationMorphism T x
              | ComplicatedFunctorMorphism _ _ _ _ F _ _ m => ComplicatedFunctorMorphism F m
              | ComplicatedGenericMorphism _ _ _ _ m => ComplicatedGenericMorphism _ _ _ m
            end).
    Fixpoint ComplicatedMorphismSimplify0 objC C s d (m : @ComplicatedMorphism objC C s d) : ComplicatedMorphism C s d.
    refine (match m in @ComplicatedMorphism objC C s d return @ComplicatedMorphism objC C s d with
              | ComplicatedComposedMorphism objC C _ _ d m1 m2 => _
              | ComplicatedIdentityMorphism _ _ x => ComplicatedIdentityMorphism _ x
              (*| ComplicatedComposedMorphism _ _ _ _ _ m1 m2 => ComplicatedComposedMorphism m1 m2*)
              | ComplicatedNaturalTransformationMorphism _ _ _ _ _ _ T x => ComplicatedNaturalTransformationMorphism T x
              | ComplicatedFunctorMorphism _ _ _ _ F _ _ m => ComplicatedFunctorMorphism F m
              | ComplicatedGenericMorphism _ _ _ _ m => ComplicatedGenericMorphism _ _ _ m
            end).
    refine (match (@ComplicatedMorphismSimplify _ _ _ _ m1, @ComplicatedMorphismSimplify _ _ _ _ m2) with
              | (ComplicatedIdentityMorphism _ _ x, m2') => _
              | _ => _
            end).
              | ComplicatedComposedMorphism objC C _ _ d m1 m2 => _
              | ComplicatedIdentityMorphism _ _ x => ComplicatedIdentityMorphism _ x
              (*| ComplicatedComposedMorphism _ _ _ _ _ m1 m2 => ComplicatedComposedMorphism m1 m2*)
              | ComplicatedNaturalTransformationMorphism _ _ _ _ _ _ T x => ComplicatedNaturalTransformationMorphism T x
              | ComplicatedFunctorMorphism _ _ _ _ F _ _ m => ComplicatedFunctorMorphism F m
              | ComplicatedGenericMorphism _ _ _ _ m => ComplicatedGenericMorphism _ _ _ m
            end).
*)
Section AdjointPointwise.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Context `(E : @SpecializedCategory objE).
  Context `(C' : @SpecializedCategory objC').
  Context `(D' : @SpecializedCategory objD').

  Variable F : SpecializedFunctor C D.
  Variable G : SpecializedFunctor D C.

  Variable A : Adjunction F G.

  Variables F' G' : SpecializedFunctor C' D'.

(*  Variable T' : SpecializedNaturalTransformation F' G'.*)

  Definition AdjointPointwise_NT_Unit : SpecializedNaturalTransformation (IdentityFunctor (C ^ E))
                                                                    (ComposeFunctors (G ^ IdentityFunctor E) (F ^ IdentityFunctor E)).
    pose proof (A : AdjunctionUnit _ _) as A'.
    refine (NTComposeT _ (LiftIdentityPointwise _ _)).
    refine (NTComposeT _ (projT1 A' ^ (IdentityNaturalTransformation (IdentityFunctor E)))).
    refine (NTComposeT (LiftComposeFunctorsPointwise _ _ (IdentityFunctor E) (IdentityFunctor E)) _).
    refine (LiftNaturalTransformationPointwise (IdentityNaturalTransformation _) _).
    exact (LeftIdentityFunctorNaturalTransformation2 _).
  Defined.

  Definition AdjointPointwise_NT_Counit : SpecializedNaturalTransformation (ComposeFunctors (F ^ IdentityFunctor E) (G ^ IdentityFunctor E))
                                                                           (IdentityFunctor (D ^ E)).
    pose proof (A : AdjunctionCounit _ _) as A'.
    refine (NTComposeT (LiftIdentityPointwise_Inverse _ _) _).
    refine (NTComposeT (projT1 A' ^ (IdentityNaturalTransformation (IdentityFunctor E))) _).
    refine (NTComposeT _ (LiftComposeFunctorsPointwise_Inverse _ _ (IdentityFunctor E) (IdentityFunctor E))).
    refine (LiftNaturalTransformationPointwise (IdentityNaturalTransformation _) _).
    exact (LeftIdentityFunctorNaturalTransformation1 _).
  Defined.

  Definition AdjointPointwise : Adjunction (F ^ (IdentityFunctor E)) (G ^ (IdentityFunctor E)).
    match goal with
      | [ |- Adjunction ?F ?G ] =>
        refine (_ : AdjunctionUnitCounit F G)
    end.
    exists AdjointPointwise_NT_Unit
           AdjointPointwise_NT_Counit.
    nt_eq.
    Time (do 5 (rewrite SimplifiedMorphismOk; simpl)). (* Finished transaction in 6. secs (5.477u,0.s) *)
    Undo 1.
    Time (autorewrite with morphism;
          autorewrite with functor;
          autorewrite with morphism). (* Finished transaction in 15. secs (14.854u,0.s) *)