cat.lean

import tactic.rcases
import tactic.ext
import tactic.simp_rw

set_option pp.coercions false

universes u v

class category (obj : Sort u) :=
  (mor : obj → obj → Sort v)
  (id : ∀{x}, mor x x)
  (comp : ∀{a b c}, mor b c → mor a b → mor a c)
  (assoc' : ∀{a b c d} (f : mor c d) (g : mor b c) (h : mor a b),
    comp f (comp g h) = comp (comp f g) h)
  (right_id' : ∀{a b} (f : mor a b), comp f id = f)
  (left_id' : ∀{a b} (f : mor a b), comp id f = f)

notation a ` ⟶ ` b := category.mor a b
notation a ` [`cat`]⟶ ` b := @category.mor cat _ a b
notation `𝟭` := category.id
notation `@𝟭 ` a := @category.id _ _ a
infixr ` · `:80 := category.comp

lemma assoc {C} [category C] {a b c d : C} (f : c ⟶ d) (g : b ⟶ c) (h : a ⟶ b) :
  f·(g·h) = (f·g)·h :=
by rw category.assoc'

lemma left_id {C} [category C] {a b : C} (f : a ⟶ b) :
  𝟭·f = f :=
by rw category.left_id'

lemma right_id {C} [category C] {a b : C} (f : a ⟶ b) :
  f·𝟭 = f :=
by rw category.right_id'

def opposite (C : Sort u) := C
notation C `ᵒᵖ`:std.prec.max_plus := opposite C
def op {C : Sort u} : C → Cᵒᵖ := id
def opposite.unop {{C : Sort u}} : Cᵒᵖ → C := id
open opposite
attribute [irreducible] opposite

instance {C} [cat : category C] : category Cᵒᵖ :=
  { mor := λa b, @category.mor C cat b.unop a.unop
  , id := λx, @category.id C cat x.unop
  , comp := by intros; apply category.comp; assumption
  , assoc' := by intros; rw assoc
  , right_id' := by intros; rw left_id
  , left_id' := by intros; rw right_id
  }

section
  @[instance]
  def SET : category (Sort u) :=
    { mor := (→), id := @id, comp := @function.comp
    , assoc' := by intros; refl
    , right_id' := by intros; refl
    , left_id' := by intros; refl
    }
  instance NAT : category ℕ :=
    { mor := (≤)
    , id := by intro; refl
    , comp := by intros; transitivity; assumption
    , assoc' := by intros; refl
    , right_id' := by intros; refl
    , left_id' := by intros; refl
    }

  namespace test
    open nat.less_than_or_equal
    def a : 0 ⟶ 1 := step refl
    def b : op 1 ⟶ op 0 := a
    def x : ℕ ⟶ ℕ := (+ 1)
    def y : ℕᵒᵖ ⟶ ℕ := λx, unop x
  end test

end

section
  structure functor' C D [category C] [category D] :=
    (obj : C → D)
    (map : ∀{a b}, (a ⟶ b) → (obj a ⟶ obj b))
    (respect_id : ∀{a}, map (@𝟭 a) = @𝟭 (obj a))
    (respect_comp : ∀{a b c} {f : a ⟶ b} {g : b ⟶ c},
      map (g·f) = map g · map f)

  open functor'

  infixr `⥤`:26 := functor'

  -- instance {C D} [category C] [category D] :
  --   has_coe_to_fun (C ⥤ D) :=
  --   { F := λ_, C → D, coe := functor'.obj }

  structure natural_transformation {C D} [category C] [category D] (F G : C ⥤ D) :=
  (hom : ∀a, F.obj a ⟶ G.obj a)
  (nat : ∀{a b} (f : a ⟶ b), G.map f · hom a = hom b · F.map f)

  namespace natural_transformation
    infixr `~>`:26 := natural_transformation
  
    universes u₁ u₂
    variables {C : Sort u₁} {D : Sort u₂} [category C] [category D]
    variables {F G H T : C ⥤ D}

    @[refl]
    def id {F : C ⥤ D} : F ~> F :=
      { hom := λ_, 𝟭
      , nat := by intros; rw [left_id, right_id]
      }

    @[trans]
    def vcomp : G ~> H → F ~> G → F ~> H
    | ⟨β, β_nat⟩ ⟨α, α_nat⟩ :=
      { hom := λx, β x · α x
      , nat := begin
          intros,
          rw [assoc, β_nat, ←assoc],
          rw [α_nat, assoc],
        end
      }

    lemma assoc : ∀{γ : F ~> G} {β : G ~> H} {α : H ~> T},
      α.vcomp (β.vcomp γ) = (α.vcomp β).vcomp γ :=
    begin
      rintro ⟨α, α_nat⟩ ⟨β, β_nat⟩ ⟨γ, γ_nat⟩,
      unfold vcomp, simp,
      funext x,
      apply assoc,
    end

    lemma left_id : ∀α : F ~> G,
      id.vcomp α = α :=
    begin
      rintro ⟨α, α_nat⟩,
      unfold id vcomp, simp,
      funext, apply left_id
    end

    lemma right_id : ∀α : F ~> G,
      α.vcomp id = α :=
    begin
      rintro ⟨α, α_nat⟩,
      unfold id vcomp, simp,
      funext, apply right_id
    end

  instance : category (C ⥤ D) :=
    { mor := (~>)
    , id := λ_, id
    , comp := λ{_ _ _}, vcomp
    , assoc' := λ{_ _ _ _} _ _ _, assoc
    , right_id' := λ{_ _}, right_id
    , left_id' := λ{_ _}, left_id
    }

  end natural_transformation

  notation `Hom[` c `](` `_` `,`  y  `)` := λx, unop x [c]⟶ y
  notation `Hom[` c `](`  x  `,` `_` `)` := λy, unop x [c]⟶ y

  -- lemma left_id_partial {C} [category C] {a b : C} :
  --   category.comp 𝟭 = @id (a ⟶ b) := by funext; simp; apply left_id
  
  -- set_option pp.implicit true

  def yoneda {C} [category.{u v} C] : C ⥤ (Cᵒᵖ ⥤ Sort v) :=
    { obj := λx,
      { obj := Hom[C](_, x)
      , map := λy₁ y₂ f g, g·f
      , respect_id := by { intro, funext, apply right_id }
      , respect_comp := by { intros, funext, apply assoc }
      }
    , map := λx₁ x₂ f,
      { hom := (λy g, f·g)
      , nat := begin
          intros y₁ y₂ g,
          funext,
          unfold category.comp,
          simp,
          rw assoc,
        end
      }
    , respect_id := begin
        intro x,
        unfold category.id natural_transformation.id,
        have q : (λ (y : Cᵒᵖ), ((category.comp 𝟭) : (y.unop ⟶ x) → (y.unop ⟶ x)))
          = λ (_x : Cᵒᵖ), id := begin
          funext, rw left_id, refl
        end,
        simp,
        -- simp_rw q,
        refl,
      end
    , respect_comp := sorry
    }
  -- { obj := λ X,
  --   { obj := λ Y, unop Y ⟶ X,
  --     map := λ Y Y' f g, f.unop ≫ g,
  --     map_comp' := λ _ _ _ f g, begin ext, dsimp, erw [category.assoc] end,
  --     map_id' := λ Y, begin ext, dsimp, erw [category.id_comp] end },
  --   map := λ X X' f, { app := λ Y g, g ≫ f } }

  def inc : ℕ ⥤ ℕ :=
    { obj := (+ 1)
    , map := by apply nat.succ_le_succ
    , respect_id := by intros; refl
    , respect_comp := by intros; refl
    }

end

section
  variables {C : Sort u} [category C]

  def is_inversion {a b : C} (f : a ⟶ b) (g : b ⟶ a) :=
    g·f = 𝟭 ∧ f·g = 𝟭

  def is_iso {a b : C} (f : a ⟶ b) :=
    ∃g : b ⟶ a, is_inversion f g

  structure iso (a b : C) :=
  mk :: (f : a ⟶ b) (g : b ⟶ a) (inv : is_inversion f g)

  notation a `≅` b := iso a b
  notation a `[`cat`]≅` b := iso (a : cat) b

  instance {a b : C} : has_coe (a ≅ b) (a ⟶ b) :=
    ⟨iso.f⟩

  def is_epi {a b : C} (f : a ⟶ b) :=
    ∀c (g₁ g₂ : b ⟶ c), g₁·f = g₂·f → g₁ = g₂

  def is_mono {a b : C} (f : a ⟶ b) :=
    ∀c (g₁ g₂ : c ⟶ a), f·g₁ = f·g₂ → g₁ = g₂

  lemma iso_is_epi {a b : C} :
    ∀f : a ⟶ b, is_iso f → is_epi f :=
  begin
    intros f f_iso,
    intros c g₁ g₂ h₀,
    cases f_iso with g h₁,
    cases h₁ with gf1 fg1, clear gf1,
    rw [←right_id g₁, ←right_id g₂],
    rw ←fg1,
    repeat { rw assoc },
    rw h₀,
  end

  lemma iso_is_mono {a b : C} :
    ∀f : a ⟶ b, is_iso f → is_mono f :=
  begin
    intros f f_iso,
    intros c g₁ g₂ h₀,
    cases f_iso with g h₁,
    cases h₁ with gf1 fg1, clear fg1,
    rw ←left_id g₁,
    rw ←left_id g₂,
    rw ←gf1,
    repeat { rw ←assoc },
    rw h₀,
  end

  instance {a b : C} {f : a ⟶ b} : has_coe (is_iso f) (is_mono f) :=
    ⟨iso_is_mono f⟩

  instance {a b : C} {f : a ⟶ b} : has_coe (is_iso f) (is_epi f) :=
    ⟨iso_is_epi f⟩

  lemma iso_invert_is_uniq {a b : C} :
    ∀f : a ⟶ b, is_iso f → ∀g₁ g₂,
      is_inversion f g₁ → is_inversion f g₂ → g₁ = g₂ :=
  begin
    intros f f_iso g₁ g₂ g₁_inv g₂_inv,
    apply (f_iso : is_mono f),
    rw [g₁_inv.2, g₂_inv.2],
  end
end

def is_singleton (A) : Prop :=
  ∃a : A, ∀b, a = b

section
  def is_initial {C} [category C] (a : C) :=
    ∀b, is_singleton (a ⟶ b)

  def initial (C) [category C] :=
    { a : C // is_initial a }

  instance initial_to_obj {C} [category C] :
    has_coe (initial C) C := coe_subtype

  lemma initial_unique {C} [category C] :
    ∀a b : initial C, is_singleton (a [C]≅ b) :=
  begin
    intros a, cases a with a a_init,
    intros b, cases b with b b_init,
    cases (a_init b) with f f_uniq,
    cases (b_init a) with g g_uniq,

    have fg_inv : is_inversion f g := begin
      split,
      cases (a_init a) with id_a id_a_uniq,
      rw [← id_a_uniq 𝟭, id_a_uniq (g·f)],
      cases (b_init b) with id_b id_b_uniq,
      rw [← id_b_uniq 𝟭, id_b_uniq (f·g)],
    end,

    existsi (iso.mk f g fg_inv),

    intro h, cases h with h h' h_inv, simp, split,
    rw [← f_uniq h],
    rw [← g_uniq h'],
  end
end


section
  def is_terminal {C} [category C] (a : C) :=
    ∀b, is_singleton (b ⟶ a)

  def terminal (C) [category C] :=
    { a : C // is_terminal a }

  instance terminal_to_obj {C} [category C] :
    has_coe (terminal C) C := coe_subtype

  -- lemma terminal_unique {C} [category C] :
  --   ∀a b : terminal C, is_singleton (a [C]≅ b) := begin
  --     intros a b,
  --     cases (@initial_unique (Cᵒᵖ) _ a b) with q w,
  --     unfold is_singleton,
  --     existsi q,
  --   end
end

lemma map_iso {C D} [category C] [category D] {a b : C} (F : C ⥤ D) :
  (a ≅ b) → (F.obj a ≅ F.obj b) :=
begin
  rintro ⟨f, g, ⟨gf, fg⟩⟩,
  apply iso.mk (F.map f) (F.map g),
  split,
  rw [←F.respect_comp, gf, F.respect_id],
  rw [←F.respect_comp, fg, F.respect_id],
end

lemma init_term_dual {C} [c : category C] :
  ∀a : C, is_initial a → is_terminal (op a) :=
  λa init b, init b.unop

example {C} [category C] {a b : C} {f g : a ⟶ b} (h : ∀{c} (h : b ⟶ c), h·f = h·g) :
  f = g :=
begin
  rw [←left_id f, ←left_id g],
  apply h,
end