gaxiiiiiiiiiiii

import Mathlib.tactic

open CategoryTheory

@[ext]
structure Mnd (X : Type) [Category X] extends T : X ⥤ X where
  η : Functor.id X ⟶ T
  μ : T ⋙ T ⟶ T
  assoc (x : X) : T.map (μ.app x) ≫ μ.app x = μ.app (T.obj x) ≫ μ.app x
  left_unit (x : X) : η.app (T.obj x) ≫ μ.app x = 𝟙 (T.obj x)

gaxiiiiiiiiiiii

import Mathlib.tactic
import Mathlib.CategoryTheory.Limits.HasLimits
import Mathlib.CategoryTheory.Limits.Shapes.Terminal
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
import Mathlib.CategoryTheory.Limits.Creates
import Mathlib.CategoryTheory.Limits.HasLimits

open CategoryTheory
open Limits

gaxiiiiiiiiiiii

import Mathlib.tactic
import Mathlib.CategoryTheory.Limits.Creates


open CategoryTheory
open Limits

#check LiftableCone
/-
  c : Cone (K ⋙ F) がLiftable

gaxiiiiiiiiiiii

import Mathlib

open CategoryTheory

section Conjugate

variable [Category X] [Category A] {F F' : X ⥤ A} {G G' : A ⥤ X}

def isConjugate (φ : F ⊣ G) (φ' : F'⊣ G') (σ : F ⟶ F') (τ : G' ⟶ G) :=
  ∀ (x : X) (a : A) (f : F'.obj x ⟶ a), (φ.homEquiv x a) (σ.app x ≫ f) = (φ'.homEquiv x a) f ≫ τ.app a

gaxiiiiiiiiiiii

import Mathlib.tactic

open CategoryTheory

lemma Functor.hcongr [Category X] [Category Y]
  {a b c d : X} {f : a ⟶ b} {g : c ⟶ d}
   (F : X ⥤ Y) (H : HEq f g) (Eac : a = c) (Ebd : b = d):
   HEq (F.map f) (F.map g)
:= by
  subst c d

gaxiiiiiiiiiiii

import Mathlib.tactic

open CategoryTheory


example [Category X] [Category A] (φ : X ≌ A) :
  φ.functor ⊣ φ.inverse
:= {
  unit := φ.unitIso.hom
  counit := φ.counitIso.hom

gaxiiiiiiiiiiii

import Mathlib.tactic
import Mathlib.CategoryTheory.Functor.Currying
import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
import Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

open CategoryTheory
open Limits

/----------- /
/ 普遍射の定義 /

gaxiiiiiiiiiiii

import Mathlib.tactic
import Mathlib.CategoryTheory.Limits.HasLimits
import Mathlib.CategoryTheory.Limits.Preserves.Basic

open CategoryTheory
open Limits

lemma Adjunction_PreservesLimit [Category 𝓐] [Category 𝓑] (F : 𝓐 ⥤ 𝓑) (G : 𝓑 ⥤ 𝓐) (σ : F ⊣ G) :
  PreservesColimits F
:= by

gaxiiiiiiiiiiii

import Mathlib.tactic
import Mathlib.CategoryTheory.Limits.HasLimits

open CategoryTheory
open Limits


structure Elm [Category.{u, v} 𝓐] (X : 𝓐ᵒᵖ ⥤ Type w) where
  obj : 𝓐
  elm : X.obj (Opposite.op obj)

gaxiiiiiiiiiiii

import Mathlib.tactic
open CategoryTheory

-- F.Full := Function.Surjective F.map
-- F.Faithful := Function.Injective F.map
-- F.FullyFaithful := Function.Bijective F.map


structure equiv (𝓐 𝓑 : Type) [Category 𝓐] [Category 𝓑] where
  func : 𝓐 ⥤ 𝓑