[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