Data.Category.Functor

Contents

• Cat
• Functors
  • Functor instances
• Universal properties

Description

Synopsis

• data Cat where
  • CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag))
• data CatW
• type family Dom ftag :: * -> * -> *
• type family Cod ftag :: * -> * -> *
• class Functor ftag where
  • (%%) :: ftag -> Obj (Dom ftag) a -> Obj (Cod ftag) (ftag :% a)
  • (%) :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
• type family ftag :% a :: *
• data Id (~>) = Id
• data g :.: h where
  • :.: :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h
• data Const c1 c2 x where
  • Const :: Category c2 => Obj c2 x -> Const c1 c2 x
• type ConstF f = Const (Dom f) (Cod f)
• data :*-: where
  • HomX_ :: Category ~> => Obj ~> x -> x :*-: ~>
• data :-*: where
  • Hom_X :: Category ~> => Obj ~> x -> ~> :-*: x
• data Opposite f where
  • Opposite :: Functor f => f -> Opposite f
• data EndoHask where
  • EndoHask :: Functor f => EndoHask f
• data InitialUniversal x u a = InitialUniversal {
  • iuObject :: Obj (Dom u) a
  • initialMorphism :: Cod u x (u :% a)
  • initialFactorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y
  }
• data TerminalUniversal x u a = TerminalUniversal {
  • tuObject :: Obj (Dom u) a
  • terminalMorphism :: Cod u (u :% a) x
  • terminalFactorizer :: forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a
  }

Cat

Functors

Functor instances

Universal properties