mwe.lean

import category_theory.monad.algebra
import data.sigma

namespace category_theory

open category_theory category_theory.category category_theory.limits comonad

universes v u

variables {C : Type u} [small_category C]

@[simps]
def inner_functor (Y : Type u) : Cᵒᵖ ⥤ Type u :=
{ obj := λ X, Π T, (T ⟶ X.unop) → Y,
  map := λ X Z f t T g, t T (g ≫ f.unop) }

variable (C)
@[simps]
def W : Type u ⥤ Type u :=
{ obj := λ Y, Σ (x : Cᵒᵖ), (inner_functor Y).obj x,
  map := λ Y Z f Ue, ⟨Ue.1, λ T g, f (Ue.2 T g)⟩ }.

instance : comonad (W C) :=
{ ε := { app := λ Y Ue, Ue.2 Ue.1.unop (𝟙 _) },
  δ := { app := λ Y Ue, ⟨Ue.1, λ T f, ⟨opposite.op T, λ S g, Ue.2 S (g ≫ f)⟩⟩ },
  right_counit' :=
  begin
    intro Y,
    ext1 ⟨U, e⟩,
    dsimp [W],
    simp,
  end,
  coassoc' :=
  begin
    intro Y,
    ext ⟨U, e⟩,
    dsimp [W],
    congr' 1,
    ext T f,
    congr' 1,
    ext S g,
    congr' 1,
    dsimp,
    ext k,
    simp,
  end }.

def coalgebra_to_presheaf : coalgebra (W C) ⥤ Cᵒᵖ ⥤ Type u :=
{ obj := λ w,
  { obj := λ X, {i : _ // (w.a i).1 = X},
    map := λ X Y f a,
    begin
      refine ⟨_, _⟩,
      apply (w.a a.1).2 _ (f.unop ≫ eq_to_hom (opposite.op_inj a.2.symm)),
      have t := congr_fun w.coassoc a.1,
      dsimp [comonad.δ, W] at t,
      injection t with t₁ t₂,
      rw heq_iff_eq at t₂,
      replace t₂ := congr_fun t₂ Y.unop,
      replace t₂ := congr_fun t₂ (f.unop ≫ eq_to_hom (opposite.op_inj a.2.symm)),
      replace t₂ := congr_arg sigma.fst t₂,
      apply t₂.symm
    end,
    map_id' := λ X,
    begin
      ext1 ⟨a, ha⟩,
      dsimp,
      congr' 1,
      cases ha,
      rw id_comp,
      exact congr_fun w.counit a,
    end,
    map_comp' := λ X Y Z f g,
    begin
      ext1 ⟨a, ha⟩,
      subst ha,
      dsimp,
      rw comp_id,
      rw comp_id,
      congr' 1,
      have t := congr_fun w.coassoc a,
      dsimp [comonad.δ, W] at t,
      injection t with t₁ t₂,
      rw heq_iff_eq at t₂,
      replace t₂ := congr_fun t₂ Y.unop,
      replace t₂ := congr_fun t₂ f.unop,
      dsimp at t₂,
      rw ← sigma.eta (w.a ((w.a a).snd Y.unop f.unop)) at t₂,
      dsimp at t₂,
      have := sigma.mk.inj t₂,
      rcases this with ⟨t₃, t₄⟩,
      -- by using t₄, we get the result pretty easily

    end

  }

}
end category_theory