cats.lean

import tactic
import data.set

namespace mycat
universes u v

-- Just use ob in place of β
--class HasObj {α : Type*} (β : α) :=
--(ob : Type*)

class HasHom {α β : Type*} (x : α) (y : β) :=
(Hom : Type*)
local infixr ` => `:25 := HasHom.Hom
abbreviation End {α : Type*} (x : α) [HasHom x x] := x => x

class HasComp {α β γ : Type*} {x : α} {y : β} {z : γ} [HasHom x y] [HasHom y z] [HasHom x z] (f : x => y) (g : y => z) :=
(comp : x => z)
local infixl ` * `:90  := HasComp.comp

class HasComp2 (α β γ : Type*) {x : α} {y : β} {z : γ} [HasHom x y] [HasHom y z] [HasHom x z]
  {f f' : x => y} {g g' : y => z} [HasHom f f'] [HasHom g g'] [HasComp f g] [HasComp f' g'] [HasHom (f * g) (f' * g')]
  (A : f => f') (B : g => g') :=
(comp2 : f * g => f' * g')

class HomOne {α : Type*} (x : α) [HasHom x x] :=
(one : End x)

instance {α : Type*} (x : α) [HasHom x x] [HomOne x] : has_one (End x) := ⟨HomOne.one⟩


class HasCompAssoc {α β γ δ : Type*} {x : α} {y : β} {z : γ} {w : δ}
  [HasHom x y] [HasHom y z] [HasHom z w] [HasHom x z] [HasHom y w] [HasHom x w]
  (f : x => y) (g : y => z) (h : z => w)
  [HasComp f g] [HasComp (f * g) h] [HasComp g h] [HasComp f (g * h)] : Prop :=
(comp_assoc [] : f * g * h = f * (g * h))
open HasCompAssoc

class HasHomUnit {α β : Type*} {x : α} {y : β} [HasHom x y] (f : x => y) [HasHom x x] [HasHom y y]
  [HomOne x] [HomOne y] [HasComp f (1 : End y)] [HasComp (1 : End x) f] : Prop :=
(comp_one : f * 1 = f)
(one_comp : 1 * f = f)

open HasHomUnit

attribute [simp] comp_one one_comp

class SemiCat (α : Type*) :=
  [to_HasHom : Π (x y : α), HasHom x y]
  [to_HasComp : Π {x y z : α} (f : x => y) (g : y => z), HasComp f g]
  [to_HasCompAssoc : Π {x y z w : α} (f : x => y) (g : y => z) (h : z => w), HasCompAssoc f g h]
attribute [instance] SemiCat.to_HasHom SemiCat.to_HasComp SemiCat.to_HasCompAssoc

class Cat (α : Type*) extends SemiCat α :=
  [to_HomOne : Π (x : α), HomOne x]
  [to_HasHomUnit : Π {x y : α} (f : x => y), HasHomUnit f]
attribute [instance] Cat.to_HomOne Cat.to_HasHomUnit

/- These are unfortunately a bad idea because I made functor (later on) be the HasHom between types! -/
@[priority 0]
instance type.HasHom (x y : Type*) : HasHom x y := ⟨x → y⟩
@[priority 0]
instance type.HasComp (x y z : Type*) (f : x => y) (g : y => z) : HasComp f g := ⟨g ∘ f⟩
@[priority 0]
instance type.HasCompAssoci (x y z w : Type*) (f : x => y) (g : y => z) (h : z => w) : HasCompAssoc f g h :=
⟨rfl⟩
@[priority 0]
instance type.HasHomOne (x : Type*) : HomOne x := ⟨id⟩
@[priority 0]
instance type.HasHomUnit (x y : Type*) (f : x => y) : HasHomUnit f :=
⟨rfl, rfl⟩
@[priority 0]
instance type.Cat : Cat Type* := {}

@[simps]
instance HasHom.cart {α β α' β' : Type*} (p : α × β) (q : α' × β') [HasHom p.1 q.1] [HasHom p.2 q.2] : HasHom p q :=
{ Hom := (p.1 => q.1) × (p.2 => q.2) }
@[simps]
instance HomOne.cart {α β : Type*} (p : α × β) [HasHom p.1 p.1] [HasHom p.2 p.2] [HomOne p.1] [HomOne p.2] : HomOne p :=
{ one := (1, 1) }
@[simps]
instance HasComp.cart {α β α' β' α'' β'' : Type*} {x : α × β} {y : α' × β'} {z : α'' × β''}
  [HasHom x.1 y.1] [HasHom y.1 z.1] [HasHom x.1 z.1]
  [HasHom x.2 y.2] [HasHom y.2 z.2] [HasHom x.2 z.2]
  (f : x => y) (g : y => z) [HasComp f.1 g.1] [HasComp f.2 g.2] : HasComp f g :=
{ comp := (f.1 * g.1, f.2 * g.2) }

instance HasCompAssoc.cart {α β α' β' α'' β'' α''' β''' : Type*} {x : α × β} {y : α' × β'} {z : α'' × β''} {w : α''' × β'''}
  [HasHom x.1 y.1] [HasHom y.1 z.1] [HasHom z.1 w.1] [HasHom x.1 z.1] [HasHom y.1 w.1] [HasHom x.1 w.1]
  [HasHom x.2 y.2] [HasHom y.2 z.2] [HasHom z.2 w.2] [HasHom x.2 z.2] [HasHom y.2 w.2] [HasHom x.2 w.2]
  (f : x => y) (g : y => z) (h : z => w)
  [HasComp f.1 g.1] [HasComp (f.1 * g.1) h.1] [HasComp g.1 h.1] [HasComp f.1 (g.1 * h.1)]
  [HasComp f.2 g.2] [HasComp (f.2 * g.2) h.2] [HasComp g.2 h.2] [HasComp f.2 (g.2 * h.2)]
  [HasCompAssoc f.1 g.1 h.1] [HasCompAssoc f.2 g.2 h.2] : HasCompAssoc f g h :=
{ comp_assoc := by { tactic.unfreeze_local_instances, cases f with f f', cases g with g g', cases h with h h', ext; dsimp; rw comp_assoc, } }

instance HasHomUnit.cart {α β α' β' : Type*} {x : α × β} {y : α' × β'} [HasHom x.1 y.1] [HasHom x.2 y.2] (f : x => y)
  [HasHom x.1 x.1] [HasHom y.1 y.1] [HasHom x.2 x.2] [HasHom y.2 y.2] [HomOne x.1] [HomOne x.2] [HomOne y.1] [HomOne y.2]
  [HasComp f.1 (1 : End y.1)] [HasComp f.2 (1 : End y.2)] [HasComp (1 : End x.1) f.1] [HasComp (1 : End x.2) f.2]
  [HasHomUnit f.1] [HasHomUnit f.2]
  : HasHomUnit f :=
{ comp_one := by { tactic.unfreeze_local_instances, cases f, ext; apply comp_one, },
  one_comp := by { tactic.unfreeze_local_instances, cases f, ext; apply one_comp } }

instance {α β : Type*} [SemiCat α] [SemiCat β] : SemiCat (α × β) := {}
instance {α β : Type*} [Cat α] [Cat β] : Cat (α × β) := {}

@[ext]
structure Fun (α β : Type*) [Cat α] [Cat β] :=
(ob : α → β)
(map' : Π {x y : α}, (x => y) → (ob x => ob y))
(map_comp' : ∀ {x y z : α} (f : x => y) (g : y => z), map' (f * g) = map' f * map' g)
(map_one' : ∀ (x : α), map' (1 : End x) = 1)

instance Fun.coe {α β : Type*} [Cat α] [Cat β] : has_coe_to_fun (Fun α β) := ⟨_, Fun.ob⟩

instance Fun.HasHom (α β : Type*) [Cat α] [Cat β] : HasHom α β := ⟨Fun α β⟩

namespace Fun
variables {α β : Type*} [Cat α] [Cat β] (F : α => β)

def map {x y : α} (f : x => y) : F x => F y := F.map' f

end Fun

local infixr ` <$> `:100 := Fun.map

namespace Fun
variables {α β : Type*} [Cat α] [Cat β] (F : α => β)

def map_comp {x y z : α} (f : x => y) (g : y => z) : F <$> (f * g) = F <$> f * F <$> g := F.map_comp' f g
def map_one (x : α) : F <$> (1 : End x) = 1 := F.map_one' x

@[simps]
protected def id : Fun α α :=
{ ob := id,
  map' := λ _ _, id,
  map_comp' := λ _ _ _ _ _, rfl,
  map_one' := λ _, rfl }

@[simps]
instance : HomOne α := ⟨Fun.id⟩

@[simps]
def comp {α β γ : Type*} [Cat α] [Cat β] [Cat γ] (F : α => β) (G : β => γ) : α => γ :=
{ ob := G.ob ∘ F.ob,
  map' := λ _ _ f, G <$> F <$> f,
  map_comp' := by { intros, rw [Fun.map_comp, Fun.map_comp] },
  map_one' := by { intros, rw [Fun.map_one, Fun.map_one] } }

instance Fun.HasComp {α β γ : Type*} [Cat α] [Cat β] [Cat γ] (F : α => β) (G : β => γ) : HasComp F G :=
⟨comp F G⟩

instance Fun.HasHomUnit : HasHomUnit F :=
{ comp_one := by { ext, refl, refl, intros a a', rw heq_iff_eq, rintro rfl, rw heq_iff_eq, refl },
  one_comp := by { ext, refl, refl, intros a a', rw heq_iff_eq, rintro rfl, rw heq_iff_eq, refl } }

end Fun


structure Nat {α β : Type*} [Cat α] [Cat β] (F F' : α => β) :=
(c : Π (x : α), F x => F' x)
(comp_c_map' : Π {x y : α} (f : x => y), c x * F' <$> f = F <$> f * c y)

instance Nat.HasHom {α β : Type*} [Cat α] [Cat β] (F F' : α => β) : HasHom F F' := ⟨Nat F F'⟩

instance Nat.coe {α β : Type*} [Cat α] [Cat β] (F F' : α => β) : has_coe_to_fun (F => F') :=
⟨_, Nat.c⟩

namespace Nat
variables {α β : Type*} [Cat α] [Cat β] {F F' : α => β} (η : F => F')

lemma comp_c_map {x y : α} (f : x => y) : η x * F' <$> f = F <$> f * η y := η.comp_c_map' f

@[simps]
protected def id : F => F :=
{ c := λ x, 1,
  comp_c_map' := λ x y f, by rw [one_comp, comp_one] }

instance Nat.HomOne : HomOne F := ⟨Nat.id⟩

@[simps]
def comp {α β : Type*} [Cat α] [Cat β] {F F' F'' : α => β} (η : F => F') (η' : F' => F'') : F => F'' :=
{ c := λ x, η x * η' x,
  comp_c_map' := λ x y f, by rw [comp_assoc, comp_c_map, ←comp_assoc, comp_c_map, comp_assoc] }

instance Nat.HasComp' {α β : Type*} [Cat α] [Cat β] {F F' F'' : α => β} (η : F => F') (η' : F' => F'') :
  HasComp η η' := ⟨Nat.comp η η'⟩

@[ext]
protected
lemma ext (η η' : F => F') (h : (η : Π (x : α), F x => F' x) = η') : η = η' :=
by { cases η, cases η', change η_c = η'_c at h, subst η_c }

lemma comp_apply {α β : Type*} [Cat α] [Cat β] {F F' F'' : α => β} (η : F => F') (η' : F' => F'') (x : α) :
  (η * η' : F => F'') x = η x * η' x := rfl

instance Nat.HasCompAssoc {α β : Type*} [Cat α] [Cat β] {F F' F'' F''' : α => β}
  (η : F => F') (η' : F' => F'') (η'' : F'' => F''') : HasCompAssoc η η' η'' :=
{ comp_assoc := by { ext, repeat { rw Nat.comp_apply }, rw comp_assoc } }

instance Nat.HasHomUnit (η : F => F') : HasHomUnit η :=
{ comp_one := by { ext, rw comp_apply, exact comp_one },
  one_comp := by { ext, rw comp_apply, exact one_comp } }

/-- The functors between two categories form a functor, with morphisms being the natural transformations -/
instance Fun.HasCat {α β : Type*} [Cat α] [Cat β] : Cat (α => β) := {}

end Nat

@[simps]
def Fun.prod {α β α' β' : Type*} [Cat α] [Cat β] [Cat α'] [Cat β'] (F : α => α') (G : β => β') : α × β => α' × β' :=
{ ob := λ p, (F p.1, G p.2),
  map' := λ p q f, (F <$> f.1, G <$> f.2),
  map_comp' := by { intros, ext; apply Fun.map_comp, },
  map_one' := by { intros, ext; apply Fun.map_one, } }

@[simp]
lemma Fun.prod_map {α β α' β' : Type*} [Cat α] [Cat β] [Cat α'] [Cat β'] (F : α => α') (G : β => β') (p q : α × β) (f : p => q) :
  Fun.prod F G <$> f = (F <$> f.fst, G <$> f.snd) := Fun.prod_map' F G p q f

@[simps]
def Nat.prod {α β α' β' : Type*} [Cat α] [Cat β] [Cat α'] [Cat β'] {F F' : α => α'} {G G' : β => β'}
  (η : F => F') (η' : G => G') : Fun.prod F G => Fun.prod F' G' :=
{ c := λ p, (η p.1, η' p.2),
  comp_c_map' := by { intros, repeat {rw Fun.prod_map }, ext; dsimp; rw Nat.comp_c_map, } }


/-- Evaluation map.  (F, a) ↦ F(a) is a bifunctor. -/
def ev {α β : Type*} [Cat α] [Cat β] : (α => β) × α => β :=
{ ob := λ p, p.fst p.snd,
  map' := λ p p' f, p.fst <$> f.snd * f.fst p'.snd,
  map_comp' := begin
    rintros ⟨F, a⟩ ⟨G, b⟩ ⟨H, c⟩ ⟨η, f⟩ ⟨η', f'⟩,
    dsimp,
    rw [Fun.map_comp, Nat.comp_apply, comp_assoc, ←comp_assoc (F <$> f') (η c) (η' c), ←Nat.comp_c_map, comp_assoc, comp_assoc],
  end,
  map_one' := by { rintros ⟨F, a⟩, dsimp, rw [Fun.map_one, one_comp], refl } }

def Fun.ev₁ {α β γ : Type*} [Cat α] [Cat β] [Cat γ] (F : α × β => γ) (a : α) : β => γ :=
{ ob := λ b, F (a, b),
    map' := λ b b' f, F <$> (1, f),
    map_comp' := begin
      intros,
      rw ←Fun.map_comp,
      change _ = F <$> (_, _),
      rw comp_one,
    end,
    map_one' := λ x, by apply Fun.map_one }

def Fun.curry' {α β γ : Type*} [Cat α] [Cat β] [Cat γ] (F : α × β => γ) : α => β => γ :=
{ ob := λ a, Fun.ev₁ F a,
  map' := λ x y f,
  { c := λ b, begin change F (x, b) => F (y, b), exact F <$> (f, 1), end,
    comp_c_map' := begin
      intros b b' f',
      dsimp, 
      change F <$> _ * F <$> _ = F <$> _ * F <$> _,
      rw [←Fun.map_comp, ←Fun.map_comp],
      change F <$> (_, _) = F <$> (_, _),
      rw [comp_one, comp_one, one_comp, one_comp],
    end },
  map_comp' := begin
    intros,
    ext b,
    change F <$> _ = F <$> _ * F <$> _,
    rw [←Fun.map_comp],
    change F <$> _ = F <$> (_, _),
    rw comp_one,
  end,
  map_one' := begin
    intros,
    ext b,
    apply Fun.map_one,
  end }

def Fun.curry {α β γ : Type*} [Cat α] [Cat β] [Cat γ] : (α × β => γ) => α => β => γ :=
{ ob := Fun.curry',
  map' := λ F F' η,
          { c := λ a,
                 { c := λ b, η (a, b),
                   comp_c_map' := λ x y f, Nat.comp_c_map _ _},
            comp_c_map' := λ x y f, begin
              ext b,
              rw [Nat.comp_apply, Nat.comp_apply],
              change η _ * F' <$> _ = F <$> _ * η _,
              rw Nat.comp_c_map,
            end },
  map_comp' := begin
    intros x y z f g,
    refl,
  end,
  map_one' := begin
    intros f,
    refl,
  end }

def Fun.ev {α β : Type*} [Cat α] [Cat β] : (α => β) => α => β := Fun.curry ev

/-
def Fun.flip {α β γ : Type*} [Cat α] [Cat β] [Cat γ] : (α => β => γ) => (β => α => γ) :=
{ Fun .
  ob := λ F, begin  end,
}
-/

def Fun.reader {α : Type*} [Cat α] (a : α) : α => Type* :=
{ ob := λ (b : α), (a => b),
  map' := λ a b f h, h * f,
  map_comp' := by { intros, ext h, symmetry, apply comp_assoc },
  map_one' := by { intros, ext h, apply comp_one } }

/-
def Yoneda' {α : Type*} [Cat α] : (α => Type*) × α => Type* :=
{ ob := λ p, (Fun.reader p.2 : α => Type u) => (p.1 : α => Type u),
  map' := λ p q η, begin
    sorry
  end,
  map_comp' := sorry,
  map_one' := sorry }
-/

structure op (α : Type*) := (val : α)

namespace op
variables {α : Type*} [Cat α]

instance op.HasHom (x y : op α) : HasHom x y := ⟨op (y.val => x.val)⟩
instance op.HasComp (x y z : op α) (f : x => y) (g : y => z) : HasComp f g := ⟨op.mk (g.val * f.val)⟩
instance op.HasCompAssoci (x y z w : op α) (f : x => y) (g : y => z) (h : z => w) : HasCompAssoc f g h :=
⟨begin apply congr_arg op.mk, exact (comp_assoc _ _ _).symm end⟩
instance op.HasHomOne (x : op α) : HomOne x := ⟨op.mk 1⟩
instance op.HasHomUnit (x y : op α) (f : x => y) : HasHomUnit f :=
⟨begin cases f, apply congr_arg op.mk, apply one_comp end, begin cases f, apply congr_arg op.mk, apply comp_one end⟩
instance op.Cat : Cat (op α) := {}
end op

def Fun.Hom {α : Type*} [Cat α] : op α × α => Type* :=
{ ob := λ p, p.1.val => p.2,
  map' := λ p p' f h, f.1.val * h * f.2,
  map_comp' := begin rintros x y z ⟨⟨f'⟩, f⟩ ⟨⟨g'⟩, g⟩, ext h, dsimp [HasComp.comp], repeat { rw comp_assoc } end,
  map_one' := begin intros, ext h, erw [one_comp, comp_one], refl end }

def Fun.I {α : Type*} [Cat α] : α => α := Fun.id
def Fun.K {α β : Type*} [Cat α] [Cat β] : α => β => α :=
{ ob := λ a,
  { ob := λ b, a,
    map' := λ b b' f, 1,
    map_comp' := by { intros, rw comp_one },
    map_one' := λ _, rfl },
  map' := λ a a' f,
  { c := λ x, f,
    comp_c_map' := begin intros, change f * 1 = 1 * f, rw [comp_one, one_comp], end },
  map_comp' := begin intros, refl, end,
  map_one' := begin intro, refl, end }
def Fun.S {α β γ : Type*} [Cat α] [Cat β] [Cat γ] : (α => β) => (α => β => γ) => α => γ :=
{ ob := λ F,
  { ob := λ G,
    { ob := λ a, Fun.ev (Fun.ev G a) (Fun.ev F a),
      map' := λ x y f, begin end
    }
  }
}

def Fun.S {α β γ : Type*} [Cat α] [Cat β] [Cat γ] : (α => β) => (α => β => γ) => α => γ :=
{ ob := λ F,
  { ob := λ G,
    { ob := λ a, G a (F a),
      map' := λ a a' f, (G a <$> (F <$> f)) * ((G <$> f) (F a')),
      map_comp' := begin sorry
/-        intros,
        repeat { rw Fun.map_comp, },
        repeat { rw comp_assoc, },
        apply congr_arg (λ w, G x <$> F <$> f * w),
        repeat { rw Nat.comp_apply, },
        rw [←comp_assoc, ←comp_assoc],
        repeat { rw Nat.comp_c_map, },-/
      end,
      map_one' := begin sorry
--        intros, rw [Fun.map_one, Fun.map_one, Fun.map_one, one_comp], refl,
      end
    },
    map' := λ G G' η,
    { c := λ x, begin end,
    },
  }
}

/-- The contravariant Yonead lemma, since I don't have swap or flip yet -/
def Yoneda {α : Type*} [Cat α] : op α => α => Type* :=
Fun.curry Fun.Hom

end mycat