圏と関手の説明

def Obj := Type
def Enricher := Type
def Hom (α β : Obj) : Enricher := (α → β)

structure EndoFunctor where
   obj : Obj → Obj -- 台型構成子＝対象パート
   hom : {α β : Obj} → (Hom α β) → (Hom (obj α) (obj β)) -- ホムパート
#check @EndoFunctor.hom
#check EndoFunctor
#print EndoFunctor

def NatStampingFunctor : EndoFunctor := {
  obj := λ α : Obj => α × Nat
  hom := λ {α β : Obj} => 
         λ u : (Hom α β) =>
         λ z : α × Nat => (u z.1, z.2)
}

def IdFunctor : EndoFunctor := {
  obj := λ α : Obj => α
  hom := λ {α β : Obj} => 
         λ u : (Hom α β) =>
         λ z : α => u z
}
#check IdFunctor.obj Nat
#check IdFunctor.hom (λ n:Nat => n)

def TrivialFunctor : EndoFunctor := {
  obj := λ _ : Obj => Unit
  hom := λ {α β : Obj} => 
         λ _ : (Hom α β) =>
         λ _ : Unit => ()
}

inductive MaybeError (α : Type) where
 | ok (x : α) : MaybeError α
 | error (msg : String) : MaybeError α

def MaybeErrorFunctor : EndoFunctor := {
  obj := λ α : Obj => MaybeError α
  hom := λ {α β : Obj} => 
         λ u : (Hom α β) =>
         λ z : MaybeError α => 
           match z with 
           | MaybeError.ok x => MaybeError.ok (u x)
           | MaybeError.error msg => MaybeError.error msg
}

#check @id
structure LawfulEndoFunctor where
   obj : Obj → Obj -- 台型構成子＝対象パート
   hom : {α β : Obj} → (Hom α β) → (Hom (obj α) (obj β)) -- ホムパート
   preserve_comp : -- 関手は結合を保つ
     ∀(α β γ: Obj), ∀(u : Hom α β)(v : Hom β γ), hom (v ∘ u) = (hom v)∘(hom u)
   preserve_id : -- 関手は恒等を保つ
     ∀(α : Obj), hom (@id α) = @id (obj α)