Functors_pointwise_equal.lean

meta def blast : tactic unit := using_smt $ return ()

structure Category :=
  (Obj : Type)
  (Hom : Obj → Obj → Type)

structure Functor (C : Category) (D : Category) :=
  (onObjects   : C^.Obj → D^.Obj)
  (onMorphisms : Π { X Y : C^.Obj },
                C^.Hom X Y → D^.Hom (onObjects X) (onObjects Y))

/-
Write a tactic for automatically generating the type casts, and notation for invoking it.
Cons: the tactic may create "ugly" proofs, and these proofs will be nested in the 
statement of your theorem.
-/

open smt_tactic
/- Very simple tactic that uses hypotheses from the local context for performing 3
   rounds of heuristic instantiation, and congruence closure. -/
meta def simple_tac : tactic unit :=
using_smt $ intros >> add_lemmas_from_facts >> repeat_at_most 3 ematch

/- Version of cast operator that "hides" the "ugly" proof -/
def {u} auto_cast {α β : Type u} {h : α = β} (a : α) :=
cast h a

notation `⟦` p `⟧` := @auto_cast _ _ (by simple_tac) p

lemma Functors_pointwise_equal
  { C D : Category }
  { F G : Functor C D }
  ( objectWitness : ∀ X : C^.Obj, F^.onObjects X = G^.onObjects X )
  ( morphismWitness : ∀ X Y : C^.Obj, ∀ f : C^.Hom X Y, ⟦ F^.onMorphisms f ⟧ = G^.onMorphisms f ) : F = G :=
begin
  induction F with F_onObjects F_onMorphisms,
  induction G with G_onObjects G_onMorphisms,
  assert h_objects : F_onObjects = G_onObjects, exact funext objectWitness,
  subst h_objects,
  assert h_morphisms : @F_onMorphisms = @G_onMorphisms, 
  apply funext, intro X, apply funext, intro Y, apply funext, intro f,
  exact morphismWitness X Y f,
  subst h_morphisms
end


print Functors_pointwise_equal

@[reducible] definition IdentityFunctor ( C: Category ) : Functor C C :=
{
  onObjects     := id,
  onMorphisms   := λ _ _ f, f
}


@[reducible] definition FunctorComposition { C D E : Category } ( F : Functor C D ) ( G : Functor D E ) : Functor C E :=
{
  onObjects     := λ X, G^.onObjects (F^.onObjects X),
  onMorphisms   := λ _ _ f, G^.onMorphisms (F^.onMorphisms f)
}

lemma FunctorComposition_left_identity { C D : Category } ( F : Functor C D ) :
  FunctorComposition (IdentityFunctor C) F = F :=
  begin
    apply Functors_pointwise_equal,
    intros,
    blast
  end