agda/examples/outdated-and-incorrect/cat/Functor.agda

module Functor where

import Logic.Identity as Id
import Category
import Logic.ChainReasoning

open Category
open Poly-Cat

private
 module Fun where

  data Functor (ℂ ⅅ : Cat) : Set1 where
    functor : (F     : Obj ℂ -> Obj ⅅ)
              (map   : {A B : Obj ℂ} -> A ─→ B -> F A ─→ F B)
              (mapId : {A : Obj ℂ} -> map (id {A = A}) == id)
              (mapCompose : {A B C : Obj ℂ}{f : B ─→ C}{g : A ─→ B} ->
                            map (f ∘ g) == map f ∘ map g
              ) -> Functor ℂ ⅅ

open Fun public

module Projections where

  Map : {ℂ ⅅ : Cat} -> Functor ℂ ⅅ -> Obj ℂ -> Obj ⅅ
  Map (functor F _ _ _) = F

  map : {ℂ ⅅ : Cat}(F : Functor ℂ ⅅ)
        {A B : Obj ℂ} -> A ─→ B -> Map F A ─→ Map F B
  map (functor _ m _ _) = m

  mapId : {ℂ ⅅ : Cat}(F : Functor ℂ ⅅ)
          {A : Obj ℂ} -> map F id == id {A = Map F A}
  mapId (functor _ _ i _) = i

  mapCompose : {ℂ ⅅ : Cat}(F : Functor ℂ ⅅ)
               {A B C : Obj ℂ}{f : B ─→ C}{g : A ─→ B} ->
               map F (f ∘ g) == map F f ∘ map F g
  mapCompose (functor _ _ _ c) = c

module Functor {ℂ ⅅ : Cat}(F : Functor ℂ ⅅ) where

  module P = Projections

  Map : Obj ℂ -> Obj ⅅ
  Map = P.Map F

  map : {A B : Obj ℂ} -> A ─→ B -> Map A ─→ Map B
  map = P.map F

  mapId : {A : Obj ℂ} -> map id == id {A = Map A}
  mapId = P.mapId F

  mapCompose : {A B C : Obj ℂ}{f : B ─→ C}{g : A ─→ B} ->
               map (f ∘ g) == map f ∘ map g
  mapCompose = P.mapCompose F

module Functors where

  Id : {ℂ : Cat} -> Functor ℂ ℂ
  Id = functor (\A -> A) (\f -> f) (\{A} -> refl) (\{A}{B}{C}{f}{g} -> refl)

  _○_ : {ℂ ℚ ℝ : Cat} -> Functor ℚ ℝ -> Functor ℂ ℚ -> Functor ℂ ℝ
  _○_ {ℂ}{ℚ}{ℝ} F G = functor FG m mid mcomp
    where

      module F = Functor F
      module G = Functor G

      FG : Obj ℂ -> Obj ℝ
      FG A = F.Map (G.Map A)

      m : {A B : Obj ℂ} -> A ─→ B -> FG A ─→ FG B
      m f = F.map (G.map f)

      mid : {A : Obj ℂ} -> m (id {A = A}) == id
      mid = chain> F.map (G.map id)
               === F.map id   by ? -- cong F.map G.mapId
               === id         by F.mapId
        where
          open module Chain = Logic.ChainReasoning.Mono.Homogenous _==_
                              (\f -> refl)
                              (\f g h -> trans)

      mcomp : {A B C : Obj ℂ}{f : B ─→ C}{g : A ─→ B} ->
              m (f ∘ g) == m f ∘ m g
      mcomp {f = f}{g = g} =
        chain> F.map (G.map (f ∘ g))
           === F.map (G.map f ∘ G.map g)
               by ? -- cong F.map G.mapCompose
           === F.map (G.map f) ∘ F.map (G.map g)
               by F.mapCompose
        where
          open module Chain = Logic.ChainReasoning.Mono.Homogenous _==_
                              (\f -> refl)
                              (\f g h -> trans)