1+ <!DOCTYPE HTML>
2+ < html > < head > < meta charset ="utf-8 "> < title > Categories.Diagram.Pushout.Colimit</ title > < link rel ="stylesheet " href ="Agda.css "> </ head > < body > < pre class ="Agda "> < a id ="1 " class ="Symbol "> {-#</ a > < a id ="5 " class ="Keyword "> OPTIONS</ a > < a id ="13 " class ="Pragma "> --without-K</ a > < a id ="25 " class ="Pragma "> --safe</ a > < a id ="32 " class ="Symbol "> #-}</ a >
3+
4+ < a id ="37 " class ="Keyword "> open</ a > < a id ="42 " class ="Keyword "> import</ a > < a id ="49 " href ="Categories.Category.Core.html " class ="Module "> Categories.Category.Core</ a > < a id ="74 " class ="Keyword "> using</ a > < a id ="80 " class ="Symbol "> (</ a > < a id ="81 " href ="Categories.Category.Core.html#442 " class ="Record "> Category</ a > < a id ="89 " class ="Symbol "> )</ a >
5+
6+ < a id ="92 " class ="Keyword "> module</ a > < a id ="99 " href ="Categories.Diagram.Pushout.Colimit.html " class ="Module "> Categories.Diagram.Pushout.Colimit</ a > < a id ="134 " class ="Symbol "> {</ a > < a id ="135 " href ="Categories.Diagram.Pushout.Colimit.html#135 " class ="Bound "> o</ a > < a id ="137 " href ="Categories.Diagram.Pushout.Colimit.html#137 " class ="Bound "> ℓ</ a > < a id ="139 " href ="Categories.Diagram.Pushout.Colimit.html#139 " class ="Bound "> e</ a > < a id ="140 " class ="Symbol "> }</ a > < a id ="142 " class ="Symbol "> (</ a > < a id ="143 " href ="Categories.Diagram.Pushout.Colimit.html#143 " class ="Bound "> C</ a > < a id ="145 " class ="Symbol "> :</ a > < a id ="147 " href ="Categories.Category.Core.html#442 " class ="Record "> Category</ a > < a id ="156 " href ="Categories.Diagram.Pushout.Colimit.html#135 " class ="Bound "> o</ a > < a id ="158 " href ="Categories.Diagram.Pushout.Colimit.html#137 " class ="Bound "> ℓ</ a > < a id ="160 " href ="Categories.Diagram.Pushout.Colimit.html#139 " class ="Bound "> e</ a > < a id ="161 " class ="Symbol "> )</ a > < a id ="163 " class ="Keyword "> where</ a >
7+
8+ < a id ="170 " class ="Keyword "> open</ a > < a id ="175 " class ="Keyword "> import</ a > < a id ="182 " href ="Categories.Functor.Core.html " class ="Module "> Categories.Functor.Core</ a > < a id ="206 " class ="Keyword "> using</ a > < a id ="212 " class ="Symbol "> (</ a > < a id ="213 " href ="Categories.Functor.Core.html#248 " class ="Record "> Functor</ a > < a id ="220 " class ="Symbol "> )</ a >
9+ < a id ="222 " class ="Keyword "> open</ a > < a id ="227 " class ="Keyword "> import</ a > < a id ="234 " href ="Categories.Diagram.Pushout.html " class ="Module "> Categories.Diagram.Pushout</ a > < a id ="261 " href ="Categories.Diagram.Pushout.Colimit.html#143 " class ="Bound "> C</ a > < a id ="263 " class ="Keyword "> using</ a > < a id ="269 " class ="Symbol "> (</ a > < a id ="270 " href ="Categories.Diagram.Pushout.html#1051 " class ="Record "> Pushout</ a > < a id ="277 " class ="Symbol "> )</ a >
10+ < a id ="279 " class ="Keyword "> open</ a > < a id ="284 " class ="Keyword "> import</ a > < a id ="291 " href ="Categories.Category.Instance.Span.html " class ="Module "> Categories.Category.Instance.Span</ a > < a id ="325 " class ="Keyword "> using</ a > < a id ="331 " class ="Symbol "> (</ a > < a id ="332 " href ="Categories.Category.Instance.Span.html#821 " class ="Function "> Span</ a > < a id ="336 " class ="Symbol "> ;</ a > < a id ="338 " href ="Categories.Category.Instance.Span.html#313 " class ="Datatype "> SpanObj</ a > < a id ="345 " class ="Symbol "> ;</ a > < a id ="347 " href ="Categories.Category.Instance.Span.html#396 " class ="Datatype "> SpanArr</ a > < a id ="354 " class ="Symbol "> )</ a >
11+
12+ < a id ="357 " class ="Keyword "> import</ a > < a id ="364 " href ="Categories.Diagram.Colimit.html " class ="Module "> Categories.Diagram.Colimit</ a > < a id ="391 " class ="Symbol "> as</ a > < a id ="394 " class ="Module "> Colim</ a >
13+ < a id ="400 " class ="Keyword "> import</ a > < a id ="407 " href ="Categories.Diagram.Duality.html " class ="Module "> Categories.Diagram.Duality</ a > < a id ="434 " class ="Symbol "> as</ a > < a id ="437 " class ="Module "> Dual</ a >
14+ < a id ="442 " class ="Keyword "> import</ a > < a id ="449 " href ="Categories.Diagram.Pullback.Limit.html " class ="Module "> Categories.Diagram.Pullback.Limit</ a > < a id ="483 " class ="Symbol "> as</ a > < a id ="486 " class ="Module "> PBLim</ a >
15+
16+ < a id ="493 " class ="Keyword "> private</ a >
17+ < a id ="503 " class ="Keyword "> module</ a > < a id ="C "> </ a > < a id ="510 " href ="Categories.Diagram.Pushout.Colimit.html#510 " class ="Module "> C</ a > < a id ="512 " class ="Symbol "> =</ a > < a id ="514 " href ="Categories.Category.Core.html#442 " class ="Module "> Category</ a > < a id ="523 " href ="Categories.Diagram.Pushout.Colimit.html#143 " class ="Bound "> C</ a >
18+ < a id ="527 " class ="Keyword "> open</ a > < a id ="532 " href ="Categories.Category.Core.html#442 " class ="Module "> Category</ a > < a id ="541 " href ="Categories.Diagram.Pushout.Colimit.html#143 " class ="Bound "> C</ a > < a id ="543 " class ="Keyword "> using</ a > < a id ="549 " class ="Symbol "> (</ a > < a id ="550 " href ="Categories.Category.Core.html#575 " class ="Field Operator "> _⇒_</ a > < a id ="553 " class ="Symbol "> ;</ a > < a id ="555 " href ="Categories.Category.Core.html#559 " class ="Field "> Obj</ a > < a id ="558 " class ="Symbol "> )</ a >
19+
20+ < a id ="561 " class ="Keyword "> module</ a > < a id ="568 " href ="Categories.Diagram.Pushout.Colimit.html#568 " class ="Module "> _</ a > < a id ="570 " class ="Symbol "> {</ a > < a id ="571 " href ="Categories.Diagram.Pushout.Colimit.html#571 " class ="Bound "> F</ a > < a id ="573 " class ="Symbol "> :</ a > < a id ="575 " href ="Categories.Functor.Core.html#248 " class ="Record "> Functor</ a > < a id ="583 " href ="Categories.Category.Instance.Span.html#821 " class ="Function "> Span</ a > < a id ="588 " href ="Categories.Diagram.Pushout.Colimit.html#143 " class ="Bound "> C</ a > < a id ="589 " class ="Symbol "> }</ a > < a id ="591 " class ="Keyword "> where</ a >
21+ < a id ="599 " class ="Keyword "> open</ a > < a id ="604 " href ="Categories.Functor.Core.html#248 " class ="Module "> Functor</ a > < a id ="612 " href ="Categories.Diagram.Pushout.Colimit.html#571 " class ="Bound "> F</ a > < a id ="614 " class ="Keyword "> using</ a > < a id ="620 " class ="Symbol "> (</ a > < a id ="621 " href ="Categories.Functor.Core.html#432 " class ="Field "> F₀</ a > < a id ="623 " class ="Symbol "> ;</ a > < a id ="625 " href ="Categories.Functor.Core.html#455 " class ="Field "> F₁</ a > < a id ="627 " class ="Symbol "> )</ a >
22+ < a id ="631 " class ="Keyword "> open</ a > < a id ="636 " href ="Categories.Diagram.Colimit.html " class ="Module "> Colim</ a > < a id ="642 " href ="Categories.Diagram.Pushout.Colimit.html#571 " class ="Bound "> F</ a > < a id ="644 " class ="Keyword "> using</ a > < a id ="650 " class ="Symbol "> (</ a > < a id ="651 " href ="Categories.Diagram.Colimit.html#961 " class ="Record "> Colimit</ a > < a id ="658 " class ="Symbol "> )</ a >
23+ < a id ="662 " class ="Keyword "> open</ a > < a id ="667 " href ="Categories.Diagram.Duality.html " class ="Module "> Dual</ a > < a id ="672 " href ="Categories.Diagram.Pushout.Colimit.html#143 " class ="Bound "> C</ a > < a id ="674 " class ="Keyword "> using</ a > < a id ="680 " class ="Symbol "> (</ a > < a id ="681 " href ="Categories.Diagram.Duality.html#2259 " class ="Function "> coPullback⇒Pushout</ a > < a id ="699 " class ="Symbol "> ;</ a > < a id ="701 " href ="Categories.Diagram.Duality.html#4444 " class ="Function "> Colimit⇒coLimit</ a > < a id ="716 " class ="Symbol "> )</ a >
24+ < a id ="720 " class ="Keyword "> open</ a > < a id ="725 " href ="Categories.Diagram.Pullback.Limit.html " class ="Module "> PBLim</ a > < a id ="731 " href ="Categories.Category.Core.html#3132 " class ="Function "> C.op</ a > < a id ="736 " class ="Keyword "> using</ a > < a id ="742 " class ="Symbol "> (</ a > < a id ="743 " href ="Categories.Diagram.Pullback.Limit.html#1010 " class ="Function "> limit⇒pullback</ a > < a id ="757 " class ="Symbol "> )</ a >
25+
26+ < a id ="762 " class ="Keyword "> private</ a >
27+ < a id ="774 " class ="Keyword "> open</ a > < a id ="779 " href ="Categories.Category.Instance.Span.html#313 " class ="Module "> SpanObj</ a >
28+ < a id ="791 " class ="Keyword "> open</ a > < a id ="796 " href ="Categories.Category.Instance.Span.html#396 " class ="Module "> SpanArr</ a >
29+
30+ < a id ="809 " href ="Categories.Diagram.Pushout.Colimit.html#809 " class ="Function "> W</ a > < a id ="811 " class ="Symbol "> =</ a > < a id ="813 " href ="Categories.Functor.Core.html#432 " class ="Field "> F₀</ a > < a id ="816 " href ="Categories.Category.Instance.Span.html#335 " class ="InductiveConstructor "> center</ a >
31+ < a id ="827 " href ="Categories.Diagram.Pushout.Colimit.html#827 " class ="Function "> A</ a > < a id ="829 " class ="Symbol "> =</ a > < a id ="831 " href ="Categories.Functor.Core.html#432 " class ="Field "> F₀</ a > < a id ="834 " href ="Categories.Category.Instance.Span.html#354 " class ="InductiveConstructor "> left</ a >
32+ < a id ="843 " href ="Categories.Diagram.Pushout.Colimit.html#843 " class ="Function "> B</ a > < a id ="845 " class ="Symbol "> =</ a > < a id ="847 " href ="Categories.Functor.Core.html#432 " class ="Field "> F₀</ a > < a id ="850 " href ="Categories.Category.Instance.Span.html#373 " class ="InductiveConstructor "> right</ a >
33+
34+ < a id ="861 " href ="Categories.Diagram.Pushout.Colimit.html#861 " class ="Function "> W⇒A</ a > < a id ="865 " class ="Symbol "> :</ a > < a id ="867 " href ="Categories.Diagram.Pushout.Colimit.html#809 " class ="Function "> W</ a > < a id ="869 " href ="Categories.Category.Core.html#575 " class ="Field Operator "> ⇒</ a > < a id ="871 " href ="Categories.Diagram.Pushout.Colimit.html#827 " class ="Function "> A</ a >
35+ < a id ="877 " href ="Categories.Diagram.Pushout.Colimit.html#861 " class ="Function "> W⇒A</ a > < a id ="881 " class ="Symbol "> =</ a > < a id ="883 " href ="Categories.Functor.Core.html#455 " class ="Field "> F₁</ a > < a id ="886 " href ="Categories.Category.Instance.Span.html#472 " class ="InductiveConstructor "> span-arrˡ</ a >
36+
37+ < a id ="901 " href ="Categories.Diagram.Pushout.Colimit.html#901 " class ="Function "> W⇒B</ a > < a id ="905 " class ="Symbol "> :</ a > < a id ="907 " href ="Categories.Diagram.Pushout.Colimit.html#809 " class ="Function "> W</ a > < a id ="909 " href ="Categories.Category.Core.html#575 " class ="Field Operator "> ⇒</ a > < a id ="911 " href ="Categories.Diagram.Pushout.Colimit.html#843 " class ="Function "> B</ a >
38+ < a id ="917 " href ="Categories.Diagram.Pushout.Colimit.html#901 " class ="Function "> W⇒B</ a > < a id ="921 " class ="Symbol "> =</ a > < a id ="923 " href ="Categories.Functor.Core.html#455 " class ="Field "> F₁</ a > < a id ="926 " href ="Categories.Category.Instance.Span.html#506 " class ="InductiveConstructor "> span-arrʳ</ a >
39+
40+ < a id ="939 " href ="Categories.Diagram.Pushout.Colimit.html#939 " class ="Function "> colimit⇒pushout</ a > < a id ="955 " class ="Symbol "> :</ a > < a id ="957 " href ="Categories.Diagram.Colimit.html#961 " class ="Record "> Colimit</ a > < a id ="965 " class ="Symbol "> →</ a > < a id ="967 " href ="Categories.Diagram.Pushout.html#1051 " class ="Record "> Pushout</ a > < a id ="975 " href ="Categories.Diagram.Pushout.Colimit.html#861 " class ="Function "> W⇒A</ a > < a id ="979 " href ="Categories.Diagram.Pushout.Colimit.html#901 " class ="Function "> W⇒B</ a >
41+ < a id ="985 " href ="Categories.Diagram.Pushout.Colimit.html#939 " class ="Function "> colimit⇒pushout</ a > < a id ="1001 " href ="Categories.Diagram.Pushout.Colimit.html#1001 " class ="Bound "> colim</ a > < a id ="1007 " class ="Symbol "> =</ a > < a id ="1009 " href ="Categories.Diagram.Duality.html#2259 " class ="Function "> coPullback⇒Pushout</ a > < a id ="1028 " class ="Symbol "> (</ a > < a id ="1029 " href ="Categories.Diagram.Pullback.Limit.html#1010 " class ="Function "> limit⇒pullback</ a > < a id ="1044 " class ="Symbol "> (</ a > < a id ="1045 " href ="Categories.Diagram.Duality.html#4444 " class ="Function "> Colimit⇒coLimit</ a > < a id ="1061 " href ="Categories.Diagram.Pushout.Colimit.html#1001 " class ="Bound "> colim</ a > < a id ="1066 " class ="Symbol "> ))</ a >
42+
43+ < a id ="1070 " class ="Keyword "> module</ a > < a id ="1077 " href ="Categories.Diagram.Pushout.Colimit.html#1077 " class ="Module "> _</ a > < a id ="1079 " class ="Symbol "> {</ a > < a id ="1080 " href ="Categories.Diagram.Pushout.Colimit.html#1080 " class ="Bound "> fA</ a > < a id ="1083 " href ="Categories.Diagram.Pushout.Colimit.html#1083 " class ="Bound "> fB</ a > < a id ="1086 " href ="Categories.Diagram.Pushout.Colimit.html#1086 " class ="Bound "> gA</ a > < a id ="1089 " class ="Symbol "> :</ a > < a id ="1091 " href ="Categories.Category.Core.html#559 " class ="Field "> Obj</ a > < a id ="1094 " class ="Symbol "> }</ a > < a id ="1096 " class ="Symbol "> {</ a > < a id ="1097 " href ="Categories.Diagram.Pushout.Colimit.html#1097 " class ="Bound "> f</ a > < a id ="1099 " class ="Symbol "> :</ a > < a id ="1101 " href ="Categories.Diagram.Pushout.Colimit.html#1083 " class ="Bound "> fB</ a > < a id ="1104 " href ="Categories.Category.Core.html#575 " class ="Field Operator "> ⇒</ a > < a id ="1106 " href ="Categories.Diagram.Pushout.Colimit.html#1080 " class ="Bound "> fA</ a > < a id ="1108 " class ="Symbol "> }</ a > < a id ="1110 " class ="Symbol "> {</ a > < a id ="1111 " href ="Categories.Diagram.Pushout.Colimit.html#1111 " class ="Bound "> g</ a > < a id ="1113 " class ="Symbol "> :</ a > < a id ="1115 " href ="Categories.Diagram.Pushout.Colimit.html#1083 " class ="Bound "> fB</ a > < a id ="1118 " href ="Categories.Category.Core.html#575 " class ="Field Operator "> ⇒</ a > < a id ="1120 " href ="Categories.Diagram.Pushout.Colimit.html#1086 " class ="Bound "> gA</ a > < a id ="1122 " class ="Symbol "> }</ a > < a id ="1124 " class ="Symbol "> (</ a > < a id ="1125 " href ="Categories.Diagram.Pushout.Colimit.html#1125 " class ="Bound "> p</ a > < a id ="1127 " class ="Symbol "> :</ a > < a id ="1129 " href ="Categories.Diagram.Pushout.html#1051 " class ="Record "> Pushout</ a > < a id ="1137 " href ="Categories.Diagram.Pushout.Colimit.html#1097 " class ="Bound "> f</ a > < a id ="1139 " href ="Categories.Diagram.Pushout.Colimit.html#1111 " class ="Bound "> g</ a > < a id ="1140 " class ="Symbol "> )</ a > < a id ="1142 " class ="Keyword "> where</ a >
44+ < a id ="1150 " class ="Keyword "> open</ a > < a id ="1155 " href ="Categories.Diagram.Pullback.Limit.html " class ="Module "> PBLim</ a > < a id ="1161 " href ="Categories.Category.Core.html#3132 " class ="Function "> C.op</ a > < a id ="1166 " class ="Keyword "> using</ a > < a id ="1172 " class ="Symbol "> (</ a > < a id ="1173 " href ="Categories.Diagram.Pullback.Limit.html#4005 " class ="Function "> pullback⇒limit-F</ a > < a id ="1189 " class ="Symbol "> ;</ a > < a id ="1191 " href ="Categories.Diagram.Pullback.Limit.html#5885 " class ="Function "> pullback⇒limit</ a > < a id ="1205 " class ="Symbol "> )</ a >
45+ < a id ="1209 " class ="Keyword "> open</ a > < a id ="1214 " href ="Categories.Diagram.Duality.html " class ="Module "> Dual</ a > < a id ="1219 " href ="Categories.Diagram.Pushout.Colimit.html#143 " class ="Bound "> C</ a > < a id ="1221 " class ="Keyword "> using</ a > < a id ="1227 " class ="Symbol "> (</ a > < a id ="1228 " href ="Categories.Diagram.Duality.html#4073 " class ="Function "> coLimit⇒Colimit</ a > < a id ="1243 " class ="Symbol "> ;</ a > < a id ="1245 " href ="Categories.Diagram.Duality.html#2618 " class ="Function "> Pushout⇒coPullback</ a > < a id ="1263 " class ="Symbol "> )</ a >
46+
47+ < a id ="1268 " href ="Categories.Diagram.Pushout.Colimit.html#1268 " class ="Function "> pushout⇒colimit-F</ a > < a id ="1286 " class ="Symbol "> :</ a > < a id ="1288 " href ="Categories.Functor.Core.html#248 " class ="Record "> Functor</ a > < a id ="1296 " href ="Categories.Category.Instance.Span.html#821 " class ="Function "> Span</ a > < a id ="1301 " href ="Categories.Diagram.Pushout.Colimit.html#143 " class ="Bound "> C</ a >
48+ < a id ="1305 " href ="Categories.Diagram.Pushout.Colimit.html#1268 " class ="Function "> pushout⇒colimit-F</ a > < a id ="1323 " class ="Symbol "> =</ a > < a id ="1325 " href ="Categories.Functor.Core.html#816 " class ="Function "> Functor.op</ a > < a id ="1336 " class ="Symbol "> (</ a > < a id ="1337 " href ="Categories.Diagram.Pullback.Limit.html#4005 " class ="Function "> pullback⇒limit-F</ a > < a id ="1354 " class ="Symbol "> (</ a > < a id ="1355 " href ="Categories.Diagram.Duality.html#2618 " class ="Function "> Pushout⇒coPullback</ a > < a id ="1374 " href ="Categories.Diagram.Pushout.Colimit.html#1125 " class ="Bound "> p</ a > < a id ="1375 " class ="Symbol "> ))</ a >
49+
50+ < a id ="1381 " class ="Keyword "> open</ a > < a id ="1386 " href ="Categories.Diagram.Colimit.html " class ="Module "> Colim</ a > < a id ="1392 " href ="Categories.Diagram.Pushout.Colimit.html#1268 " class ="Function "> pushout⇒colimit-F</ a > < a id ="1410 " class ="Keyword "> using</ a > < a id ="1416 " class ="Symbol "> (</ a > < a id ="1417 " href ="Categories.Diagram.Colimit.html#961 " class ="Record "> Colimit</ a > < a id ="1424 " class ="Symbol "> )</ a >
51+
52+ < a id ="1429 " href ="Categories.Diagram.Pushout.Colimit.html#1429 " class ="Function "> pushout⇒colimit</ a > < a id ="1445 " class ="Symbol "> :</ a > < a id ="1447 " href ="Categories.Diagram.Colimit.html#961 " class ="Record "> Colimit</ a >
53+ < a id ="1457 " href ="Categories.Diagram.Pushout.Colimit.html#1429 " class ="Function "> pushout⇒colimit</ a > < a id ="1473 " class ="Symbol "> =</ a > < a id ="1475 " href ="Categories.Diagram.Duality.html#4073 " class ="Function "> coLimit⇒Colimit</ a > < a id ="1491 " class ="Symbol "> (</ a > < a id ="1492 " href ="Categories.Diagram.Pullback.Limit.html#5885 " class ="Function "> pullback⇒limit</ a > < a id ="1507 " class ="Symbol "> (</ a > < a id ="1508 " href ="Categories.Diagram.Duality.html#2618 " class ="Function "> Pushout⇒coPullback</ a > < a id ="1527 " href ="Categories.Diagram.Pushout.Colimit.html#1125 " class ="Bound "> p</ a > < a id ="1528 " class ="Symbol "> ))</ a >
54+ </ pre > </ body > </ html >
0 commit comments