cats.lean

universes u v
variables {α : Type u}

structure category :=
    (ob : Type u)
    (hom : ob -> ob -> Type v)
    (i(A : ob) : hom A A)
    (comp : (Π {A B C : ob}, hom B C -> hom A B -> hom A C))
    (comp_assoc : ∀ A B C D : ob, ∀ f : hom A B, ∀ g : hom B C, ∀ h : hom C D,
        comp (comp h g) f = comp h (comp g f))
    (comp_i_R : ∀ A B : ob, ∀ f : hom A B, comp f (i A) = f)
    (comp_i_L : ∀ A B : ob, ∀ f : hom A B, comp (i B) f = f)


def comp {C : category} := C.comp
infix ` ▰ `:90 := comp

def i {C : category}:= C.i

def hom {C : category} := C.hom
infix ` => `: 100 := hom

structure ftor (C D : category) :=
    (o : C.ob -> D.ob)
    (h : Π {A B : C.ob}, (A => B) -> (o A) => (o B))
    (hom_prop : ∀ A B C : C.ob, ∀ g : A => B, ∀ f : B => C, h(f ▰ g) = h(f) ▰ h(g))
    (i_prop : ∀ A : C.ob, h (i A) = i (o A))

infix ` ==> `: 200 := ftor

def ftor_comp {C D E : category}  (G : D ==> E)  (F : C ==> D) : C ==> E := 
    ftor.mk
        (λ A, G.o (F.o A)) 
        (λ {A B : C.ob}, λ f, G.h (F.h f)) 
        (by simp_intros [F.hom_prop, G.hom_prop]  ) 
        (by simp_intros [F.i_prop, G.i_prop] )

infix ` << `:90 := ftor_comp

def ftor_i (C : category) : C ==> C :=
    ftor.mk
        (λ A, A)
        (λ {A B : C.ob}, λ f, f)
        (by simp_intros)
        (by simp_intros)


lemma ftor_comp_assoc (C0 C1 C2 C3 : category) (F : C0 ==> C1) (G : C1 ==> C2) (H : C2 ==> C3) 
    : (H << G) << F = H << (G << F) := by simp_intros [ftor_comp]

lemma ftor_i_R (C D : category) (F : C ==> D) 
    : F << (ftor_i C) = F 
    := 
        begin 
            simp_intros [ftor_comp, ftor_i],
            sorry
        end
lemma ftor_i_L (C D : category) (F : C ==> D) 
    : (ftor_i D) << F = F 
    := 
        begin 
            simp_intros [ftor_comp, ftor_i], 
            sorry
        end

def Cat := 
    category.mk
        (category)
        (λ C D, C ==> D)
        (ftor_i)
        (λ {C D E}, ftor_comp)
        (ftor_comp_assoc)
        (ftor_i_R)
        (ftor_i_L)