Profunctors.lean

import Mathlib.CategoryTheory.Action
import Mathlib.CategoryTheory.Category.Cat
import Mathlib.CategoryTheory.DiscreteCategory
import Mathlib.CategoryTheory.Functor.Category
import Mathlib.CategoryTheory.Functor.Hom
import Mathlib.CategoryTheory.Sigma.Basic
import Mathlib.CategoryTheory.Limits.Shapes.Types

open CategoryTheory CategoryTheory.Limits Equiv

universe u₁ u₂ u₃ u₄ v₁ v₂ v₃ v₄ w

def Prof (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
  := Dᵒᵖ × C ⥤ Type w
def Prof.Id (C : Type u₁) [Category.{v₁} C] : Prof C C := Functor.hom C

instance (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
  : Category (Prof C D) := Functor.category

variable {A : Type u₁} [Category.{v₁} A] {B : Type u₂} [Category.{v₂} B]
         {C : Type u₃} [Category.{v₃} C] {D : Type u₄} [Category.{v₄} D]

def Prof.precomp (F : A ⥤ C) (G : B ⥤ D) (H : Prof.{u₃, u₄, v₃, v₄, w} C D)
  : Prof A B := Functor.prod (Functor.op G) F ⋙ H

def square (F : A ⥤ C) (G : B ⥤ D)
  (H : Prof.{u₁, u₂, v₁, v₂, w} A B) (K : Prof.{u₃, u₄, v₃, v₄, w} C D)
  := H ⟶ K.precomp F G

def UniversalCover (G : Type u₁) [Monoid G] := ActionCategory G G

instance (G : Type u₁) [Monoid G] : Category (UniversalCover G) :=
  instCategoryActionCategory _ _
instance (G : Type u₁) [Monoid G] : CoeTC G (UniversalCover G) :=
  ActionCategory.instCoeTCActionCategory
instance (G : Type u₁) [Group G] : Groupoid (UniversalCover G) :=
  ActionCategory.instGroupoidActionCategoryToMonoidToDivInvMonoid

def UniversalCover.π (G : Type u₁) [Monoid G]
  : UniversalCover G ⥤ SingleObj G := ActionCategory.π G G

def IsThin (C : Type u₁) [Category.{v₁} C] := ∀ X Y : C, Subsingleton (X ⟶ Y)
lemma UniversalCover.IsThin (G : Type u₁) [RightCancelMonoid G] : IsThin (UniversalCover G)
| Sigma.mk _ g, Sigma.mk _ h => by
  dsimp at g h
  constructor
  intros p q
  obtain ⟨p, hyp1⟩ := p; obtain ⟨q, hyp2⟩ := q
  apply Subtype.ext
  exact mul_left_injective g (Eq.trans hyp1 hyp2.symm)

instance UniversalCover.HomUnique (G : Type u₁) [Group G]
  (x y : UniversalCover G) : Unique (x ⟶ y) :=
  @uniqueOfSubsingleton _ (UniversalCover.IsThin G x y)
                        ⟨y.back * x.back⁻¹, inv_mul_cancel_right y.back x.back⟩

instance UniversalCover.IsConnected (G : Type u₁) [Group G] : IsConnected (UniversalCover G) :=
  ActionCategory.instIsConnectedActionCategoryInstCategoryActionCategory

def SingleObj.OpIso (G : Type u₁) [Monoid G]
  : @CategoryTheory.Iso Cat _ (Bundled.of (SingleObj G)ᵒᵖ)
                              (Bundled.of (SingleObj Gᵐᵒᵖ))
  where
    hom := {
      obj := fun _ => SingleObj.star G
      map := fun g => MulOpposite.op (Opposite.unop g)
    }
    inv := {
      obj := fun _ => Opposite.op (SingleObj.star _)
      map := fun g => Opposite.op (MulOpposite.unop g)
    }

-- def Sigma.ToOp {J : Type w} {C : J → Type u₁} [(j : J) → Category.{v₁, u₁} (C j)]
--   : (Σ j, C j)ᵒᵖ ⥤ Σ j, (C j)ᵒᵖ
--   where
--     hom := CategoryTheory.Sigma.desc _
--     inv := sorry

def Sigma.OpIso {J : Type w} {C : J → Type u₁} [(j : J) → Category.{v₁, u₁} (C j)]
  : @CategoryTheory.Iso Cat _ (Bundled.of (Σ j, C j)ᵒᵖ)
                              (Bundled.of (Σ j, (C j)ᵒᵖ))
  where
    hom := (Sigma.desc (fun j => (@Sigma.incl _ (fun j' => (C j')ᵒᵖ) _ j).rightOp)).leftOp
    inv := Sigma.desc (fun j => Functor.leftOp (Sigma.incl j ⋙ opOp _))
    hom_inv_id := by
      apply Functor.hext
      . intros
        exact Eq.refl _
      . apply Opposite.rec'; intro X
        apply Opposite.rec'; intro Y
        apply Opposite.rec'; intro f
        change Y ⟶ X at f
        induction f
        exact HEq.refl _
    inv_hom_id := by
      apply Functor.hext
      . intros
        exact Eq.refl _
      . intros X Y f
        induction f
        exact HEq.refl _

def SingleObj.Inv (G : Type u₁) [Group G] : (SingleObj G)ᵒᵖ ⥤ SingleObj G where
  obj _        := SingleObj.star _
  map g        := g.unop⁻¹
  map_id _     := inv_one
  map_comp _ _ := mul_inv_rev _ _

def UniversalCover.Inv (G : Type u₁) [Group G] : UniversalCover G ⥤ UniversalCover G where
  obj g := (g.back⁻¹ : G)
  map {g h} _ := ⟨h.back⁻¹ * g.back, mul_inv_cancel_right h.back⁻¹ g.back⟩
  map_comp := by { intros; apply Subsingleton.elim }

variable {J : Type u₂} (G : J → Type u₁) [∀ j, Group (G j)]
abbrev Tot := Σ j, SingleObj (G j)
abbrev Cov := Σ j, UniversalCover (G j)

def Cov.Inv : Cov G ⥤ Cov G :=
  Sigma.Functor.sigma (fun j => UniversalCover.Inv (G j))

def Sigma.Functor.sigma' {I : Type w}
  {C : I → Type u₁} [(i : I) → Category.{v₁} (C i)]
  {D : I → Type u₂} [(i : I) → Category.{v₁} (D i)]
  (F : (i : I) → C i ⥤ D i) : (Σi, C i) ⥤ Σi, D i :=
  Sigma.desc (fun i => F i ⋙ Sigma.incl i)

def Cov.π : Cov G ⥤ Tot G := Sigma.Functor.sigma' (fun j => UniversalCover.π (G j))

def Pt (C : Type u₁) [Category.{v₂} C] : Prof C C := (Functor.const _).obj PUnit
def CofreeBiAct : Prof.{u₂, u₂, max u₁ u₂, max u₁ u₂} (Tot G) (Tot G) :=
  Functor.prod (Sigma.OpIso.hom ⋙ Sigma.desc (fun j => (SingleObj.OpIso (G j)).hom
                                                       ⋙ actionAsFunctor (G j)ᵐᵒᵖ (G j)))
               (Sigma.desc (fun j => actionAsFunctor (G j) (G j)))
  ⋙ uncurry.obj Types.binaryProductFunctor

def TheMap : square (Cov.π G) (Cov.π G) (Pt (Cov G)) (CofreeBiAct G) where
  app
  | ⟨⟨⟨i, ⟨_, s⟩⟩⟩, ⟨j, ⟨_, t⟩⟩⟩ => fun _ => (@Inv.inv (G i) _ s, t)
  naturality
  | ⟨⟨X⟩, Y⟩, ⟨⟨X'⟩, Y'⟩, ⟨⟨p⟩, q⟩ => by
    dsimp at p q
    induction p with | @mk j₁ s₁ t₁ p =>
    induction q with | @mk j₂ s₂ t₂ q =>
    obtain ⟨_, s₁⟩ := s₁; obtain ⟨_, t₁⟩ := t₁
    obtain ⟨_, s₂⟩ := s₂; obtain ⟨_, t₂⟩ := t₂
    obtain ⟨g, hyp1⟩ := p
    obtain ⟨h, hyp2⟩ := q
    ext
    refine Prod.mk.inj_iff.mpr ⟨?_, hyp2.symm⟩
    change (G j₁) at t₁
    change (G j₁) at s₁
    change s₁⁻¹ = t₁⁻¹ * g
    exact eq_inv_mul_of_mul_eq (mul_inv_eq_of_eq_mul hyp1.symm)

-- abbrev PermGrpd := Σ (n : ℕ), SingleObj (Perm (Fin n))
-- abbrev PermGrpdCover := Σ (n : ℕ), UniversalCover (Perm (Fin n))
-- def I : Discrete ℕ ⥤ PermGrpd := Discrete.functor (fun n => ⟨n, SingleObj.star _⟩)
-- def J : Discrete ℕ ⥤ PermGrpdCover := Discrete.functor (fun n => ⟨n, ActionCategory.objEquiv _ _ (Equiv.refl (Fin n))⟩)
-- def π : PermGrpdCover ⥤ PermGrpd := Sigma.Functor.sigma (fun _ => ActionCategory.π _ _)
-- def A : PermGrpdCover ⥤ PermGrpdCover := Sigma.Functor.sigma (fun _ => UniversalCover.Inv _)
-- def r : PermGrpd ⥤ Discrete ℕ := Sigma.desc (fun n => (Functor.const _).obj (Discrete.mk n))

-- lemma lem1 : I ⋙ r = 𝟭 (Discrete ℕ) := by
--   apply Functor.hext
--   . intro n; cases n
--     exact Eq.refl _
--   . intro n m f; cases n; cases m
--     obtain ⟨⟨h⟩⟩ := f
--     exact HEq.refl _

-- lemma lem2 : J ⋙ π = I := by
--   apply Functor.hext
--   . intro n; cases n
--     exact Eq.refl _
--   . intro n m f; cases n; cases m
--     obtain ⟨⟨h⟩⟩ := f; dsimp at h
--     subst h
--     exact HEq.refl _