[Agda] running out of memory in formalization of category theory

Dan Licata drl at cs.cmu.edu
Tue Jun 8 18:38:40 CEST 2010


Thanks for the replies, everyone!

Ulf, I see your point about the terms getting very large.  For example,
a goal 

  Cat.Ob (rawc (Y ⊙r o))

(roughly "an object of the category given by Y(o), where Y is a functor
into Cat) seems innocuous enough, but when you print it with implicit
arguments, it pretty prints at about 450 lines along!  (Attached at the
bottom of this message, in case anyone can make anything out of it.)
I'll try making some things abstract like Nisse suggested to see if I
can blank out some of the equational bits, like the fact that a functor
preserves identity and composition.

Conor and Nisse, I'm not using records, so it's less eta-expandable,
though the category theory defintions do use a lot of functions, so
there is still that.  Is there a way to turn off eta equality to test
this hypothesis?  I think I remember seeing something like "temporarily
disable eta" in the change logs recently.  

-Dan

Cat.Ob {l}
(rawc {l}
 (_⊙r_ {S l} {Γ}
  {func {_} {_} {_}
   (λ _ →
      category {_}
      (cat {_} (Category l) (λ o1 o2 → ⟰ {l} (Functor {l} o1 o2)))
      (iscat {_} {_}
       (λ {.A} →
          record
            {⟱ =
               functor {_} {_} {_}
               (func {_} {_} {_} (λ A → A) (λ {.A'} {.B} f → f))
               (isfunc {_} {_} {_} {_}
                (λ {.o1} →
                   Refl {_} {_} {IsCategory.id {l} {rawc {l} .A} (isc {l} .A) {.o1}})
                (λ {.o1} {.o2} {.o3} _ _ →
                   Refl {_} {_}
                   {IsCategory.comp {l} {rawc {l} .A} (isc {l} .A) {.o1} {.o2} {.o3} _
                    _}))})
       (λ {.A} {.B} {.C} F G →
          record
            {⟱ =
               functor {_} {_} {_}
               (func {_} {_} {_}
                (λ A →
                   _·r_ {l} {rawc {l} .B} {rawc {l} .C}
                   (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                   (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                    (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) A))
                (λ {.A'} {.B'} f →
                   fmapr {l} {rawc {l} .B} {rawc {l} .C}
                   (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                   {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                    (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .A'}
                   {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                    (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .B'}
                   (fmapr {l} {rawc {l} .A} {rawc {l} .B}
                    (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.A'} {.B'} f)))
               (isfunc {_} {_} {_} {_}
                (λ {.o1} →
                   IdM.trans {l}
                   {Cat.Arrow {l} (rawc {l} .C)
                    (_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1))
                    (_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1))}
                   {fmapr {l} {rawc {l} .B} {rawc {l} .C}
                    (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                    (fmapr {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o1} {.o1}
                     (IsCategory.id {l} {rawc {l} .A} (isc {l} .A) {.o1}))}
                   {fmapr {l} {rawc {l} .B} {rawc {l} .C}
                    (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                    (IsCategory.id {l} {rawc {l} .B} (isc {l} .B)
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1})}
                   {IsCategory.id {l} {rawc {l} .C} (isc {l} .C)
                    {_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1)}}
                   (IdM.substeq {l} {l}
                    {Cat.Arrow {l} (rawc {l} .B)
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1)
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1)}
                    {Cat.Arrow {l} (rawc {l} .C)
                     (_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                      (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                      (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                       (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1))
                     (_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                      (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                      (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                       (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1))}
                    (fmapr {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1})
                    {fmapr {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o1} {.o1}
                     (IsCategory.id {l} {rawc {l} .A} (isc {l} .A) {.o1})}
                    {IsCategory.id {l} {rawc {l} .B} (isc {l} .B)
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}}
                    (IsFunctor.idF {l} {.A} {.B}
                     {rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)}
                     (isf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o1}))
                   (IsFunctor.idF {l} {.B} {.C}
                    {rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F)}
                    (isf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}))
                (λ {.o1} {.o2} {.o3} g f →
                   IdM.trans {l}
                   {Cat.Arrow {l} (rawc {l} .C)
                    (_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1))
                    (_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o3))}
                   {IsCategory.comp {l} {rawc {l} .C} (isc {l} .C)
                    {_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1)}
                    {_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o2)}
                    {_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o3)}
                    (fmapr {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o2}
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o3}
                     (fmapr {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o2} {.o3} g))
                    (fmapr {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o2}
                     (fmapr {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o1} {.o2} f))}
                   {fmapr {l} {rawc {l} .B} {rawc {l} .C}
                    (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o3}
                    (IsCategory.comp {l} {rawc {l} .B} (isc {l} .B)
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o2}
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o3}
                     (fmapr {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o2} {.o3} g)
                     (fmapr {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o1} {.o2} f))}
                   {fmapr {l} {rawc {l} .B} {rawc {l} .C}
                    (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o3}
                    (fmapr {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o1} {.o3}
                     (IsCategory.comp {l} {rawc {l} .A} (isc {l} .A) {.o1} {.o2} {.o3} g
                      f))}
                   (IsFunctor.compF {l} {.B} {.C}
                    {rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F)}
                    (isf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o2}
                    {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o3}
                    (fmapr {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o2} {.o3} g)
                    (fmapr {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o1} {.o2} f))
                   (IdM.substeq {l} {l}
                    {Cat.Arrow {l} (rawc {l} .B)
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1)
                     (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o3)}
                    {Cat.Arrow {l} (rawc {l} .C)
                     (_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                      (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                      (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                       (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1))
                     (_·r_ {l} {rawc {l} .B} {rawc {l} .C}
                      (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                      (_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                       (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o3))}
                    (fmapr {l} {rawc {l} .B} {rawc {l} .C}
                     (rawf {l} {.B} {.C} (⟱ {l} {Functor {l} .B .C} F))
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o3})
                    {IsCategory.comp {l} {rawc {l} .B} (isc {l} .B)
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o1}
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o2}
                     {_·r_ {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) .o3}
                     (fmapr {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o2} {.o3} g)
                     (fmapr {l} {rawc {l} .A} {rawc {l} .B}
                      (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o1} {.o2} f)}
                    {fmapr {l} {rawc {l} .A} {rawc {l} .B}
                     (rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o1} {.o3}
                     (IsCategory.comp {l} {rawc {l} .A} (isc {l} .A) {.o1} {.o2} {.o3} g
                      f)}
                    (IsFunctor.compF {l} {.A} {.B}
                     {rawf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)}
                     (isf {l} {.A} {.B} (⟱ {l} {Functor {l} .A .B} G)) {.o1} {.o2} {.o3}
                     g f))))})))
   (λ {.A} {.B} _ →
      record
        {⟱ =
           functor {_} {_} {_}
           (func {_} {_} {_} (λ A → A) (λ {.A'} {.B'} f → f))
           (isfunc {_} {_} {_} {_}
            (λ {.o1} →
               Refl {_} {_}
               {record
                  {⟱ =
                     functor {_} {_} {_}
                     (func {_} {_} {_} (λ A → A) (λ {.A'} {.B'} f → f))
                     (isfunc {_} {_} {_} {_}
                      (λ {.o2} →
                         Refl {_} {_}
                         {IsCategory.id {l} {rawc {l} .o1} (isc {l} .o1) {.o2}})
                      (λ {.o2} {.o3} {.o4} _ _ →
                         Refl {_} {_}
                         {IsCategory.comp {l} {rawc {l} .o1} (isc {l} .o1) {.o2} {.o3} {.o4}
                          _ _}))}})
            (λ {.o1} {.o2} {.o3} _ _ →
               Refl {_} {_}
               {record
                  {⟱ =
                     functor {_} {_} {_}
                     (func {_} {_} {_}
                      (λ A →
                         _·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                         (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                         (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                          (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) A))
                      (λ {.A'} {.B'} f →
                         fmapr {l} {rawc {l} .o2} {rawc {l} .o3}
                         (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                         {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                          (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .A'}
                         {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                          (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .B'}
                         (fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                          (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.A'} {.B'}
                          f)))
                     (isfunc {_} {_} {_} {_}
                      (λ {.o4} →
                         IdM.trans {l}
                         {Cat.Arrow {l} (rawc {l} .o3)
                          (_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4))
                          (_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4))}
                         {fmapr {l} {rawc {l} .o2} {rawc {l} .o3}
                          (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                          (fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o4} {.o4}
                           (IsCategory.id {l} {rawc {l} .o1} (isc {l} .o1) {.o4}))}
                         {fmapr {l} {rawc {l} .o2} {rawc {l} .o3}
                          (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                          (IsCategory.id {l} {rawc {l} .o2} (isc {l} .o2)
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4})}
                         {IsCategory.id {l} {rawc {l} .o3} (isc {l} .o3)
                          {_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4)}}
                         (IdM.substeq {l} {l}
                          {Cat.Arrow {l} (rawc {l} .o2)
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4)
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4)}
                          {Cat.Arrow {l} (rawc {l} .o3)
                           (_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                            (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                            (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                             (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4))
                           (_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                            (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                            (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                             (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4))}
                          (fmapr {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4})
                          {fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o4} {.o4}
                           (IsCategory.id {l} {rawc {l} .o1} (isc {l} .o1) {.o4})}
                          {IsCategory.id {l} {rawc {l} .o2} (isc {l} .o2)
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}}
                          (IsFunctor.idF {l} {.o1} {.o2}
                           {rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)}
                           (isf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o4}))
                         (IsFunctor.idF {l} {.o2} {.o3}
                          {rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _)}
                          (isf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}))
                      (λ {.o4} {.o5} {.o6} g f →
                         IdM.trans {l}
                         {Cat.Arrow {l} (rawc {l} .o3)
                          (_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4))
                          (_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o6))}
                         {IsCategory.comp {l} {rawc {l} .o3} (isc {l} .o3)
                          {_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4)}
                          {_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o5)}
                          {_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o6)}
                          (fmapr {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o5}
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o6}
                           (fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o5} {.o6}
                            g))
                          (fmapr {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o5}
                           (fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o4} {.o5}
                            f))}
                         {fmapr {l} {rawc {l} .o2} {rawc {l} .o3}
                          (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o6}
                          (IsCategory.comp {l} {rawc {l} .o2} (isc {l} .o2)
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o5}
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o6}
                           (fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o5} {.o6}
                            g)
                           (fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o4} {.o5}
                            f))}
                         {fmapr {l} {rawc {l} .o2} {rawc {l} .o3}
                          (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o6}
                          (fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o4} {.o6}
                           (IsCategory.comp {l} {rawc {l} .o1} (isc {l} .o1) {.o4} {.o5} {.o6}
                            g f))}
                         (IsFunctor.compF {l} {.o2} {.o3}
                          {rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _)}
                          (isf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o5}
                          {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o6}
                          (fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o5} {.o6}
                           g)
                          (fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o4} {.o5}
                           f))
                         (IdM.substeq {l} {l}
                          {Cat.Arrow {l} (rawc {l} .o2)
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4)
                           (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o6)}
                          {Cat.Arrow {l} (rawc {l} .o3)
                           (_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                            (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                            (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                             (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4))
                           (_·r_ {l} {rawc {l} .o2} {rawc {l} .o3}
                            (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                            (_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                             (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o6))}
                          (fmapr {l} {rawc {l} .o2} {rawc {l} .o3}
                           (rawf {l} {.o2} {.o3} (⟱ {l} {Functor {l} .o2 .o3} _))
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o6})
                          {IsCategory.comp {l} {rawc {l} .o2} (isc {l} .o2)
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o4}
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o5}
                           {_·r_ {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) .o6}
                           (fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o5} {.o6}
                            g)
                           (fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                            (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o4} {.o5}
                            f)}
                          {fmapr {l} {rawc {l} .o1} {rawc {l} .o2}
                           (rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o4} {.o6}
                           (IsCategory.comp {l} {rawc {l} .o1} (isc {l} .o1) {.o4} {.o5} {.o6}
                            g f)}
                          (IsFunctor.compF {l} {.o1} {.o2}
                           {rawf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)}
                           (isf {l} {.o1} {.o2} (⟱ {l} {Functor {l} .o1 .o2} _)) {.o4} {.o5}
                           {.o6} g f))))}}))})}
  Y o))


More information about the Agda mailing list