gaxiiiiiiiiiiii

variable {α : Type}

/-- リストの長さが偶数であることを表す述語 -/
@[grind]
inductive EvenLength : List α → Prop
  | nil : EvenLength []
  | cons_cons {a b : α} {l : List α} (h : EvenLength l) :
    EvenLength (a :: b :: l)

example (xs : List α) : EvenLength xs ↔ xs.length % 2 = 0 := by

gaxiiiiiiiiiiii

import Mathlib

namespace TAL

class BoolAlg (P : Type)  extends DistribLattice P, HasCompl P, BoundedOrder P where
  inf_compl_eq_bot (x : P) : x ⊓ xᶜ = ⊥
  sup_compl_eq_top (x : P) : x ⊔ xᶜ = ⊤

class BoolRing (P : Type _ )extends Ring P where
  idempotent (a : P) : a * a = a

gaxiiiiiiiiiiii

-- Notes on regular, exact and additive categories
-- Marino Gran


import Mathlib

open CategoryTheory
open Limits

#check Balanced

gaxiiiiiiiiiiii

import Mathlib
import Mathlib.CategoryTheory.Limits.Shapes.Terminal
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
import Mathlib.CategoryTheory.Limits.Shapes.Products





open CategoryTheory

gaxiiiiiiiiiiii

import Mathlib

open CategoryTheory

example [Category 𝓐] [Category 𝓑] (U : 𝓐 ⥤ 𝓑) :
  U.IsRightAdjoint ↔  ∀ B : 𝓑, (U ⋙ coyoneda.obj (Opposite.op B)).IsCorepresentable
:= by
  constructor<;> intro H
  · rcases H with ⟨F, ⟨σ⟩⟩
    intro B; constructor

gaxiiiiiiiiiiii

import Mathlib
import Mathlib.CategoryTheory.Limits.Preserves.Basic


open CategoryTheory
open Limits


example [Category 𝓒] (F : 𝓒ᵒᵖ ⥤ Type v) (HF : F.IsRepresentable) :
  PreservesLimits F

gaxiiiiiiiiiiii

import Mathlib
import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Yoneda

open CategoryTheory
open Limits


#check Functor.cones
/-

gaxiiiiiiiiiiii

import Mathlib
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

open CategoryTheory
open Limits

section PB2

variable [Category 𝓒] (A B C D E F : 𝓒)

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