Skip to content

Commit b220636

Browse files
JacquesCaretteJacquesCarette
committed
Deploying to gh-pages from @ 17cbcba 🚀
1 parent af601e8 commit b220636

6 files changed

+392
-269
lines changed

‎Categories.Bicategory.Bigroupoid.html‎

Lines changed: 14 additions & 14 deletions
Large diffs are not rendered by default.

‎Categories.Bicategory.Construction.LaxSlice.html‎

Lines changed: 19 additions & 19 deletions
Large diffs are not rendered by default.

‎Categories.Bicategory.Extras.html‎

Lines changed: 337 additions & 214 deletions
Large diffs are not rendered by default.

‎Categories.Bicategory.Opposite.html‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@
9696
<a id="3871" href="Categories.Bicategory.Opposite.html#3778" class="Bound">f</a> <a id="3873" href="Categories.Bicategory.html#2018" class="Function Operator">▷</a> <a id="3875" href="Categories.Bicategory.Extras.html#2341" class="Function">λ⇒</a> <a id="3886" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a>
9797
<a id="3892" class="Symbol">;</a> <a id="3894" href="Categories.Bicategory.html#2837" class="Field">pentagon</a> <a id="3903" class="Symbol">=</a> <a id="3905" class="Symbol">λ</a> <a id="3907" class="Symbol">{</a><a id="3908" href="Categories.Bicategory.Opposite.html#3908" class="Bound">_</a> <a id="3910" href="Categories.Bicategory.Opposite.html#3910" class="Bound">_</a> <a id="3912" href="Categories.Bicategory.Opposite.html#3912" class="Bound">_</a> <a id="3914" href="Categories.Bicategory.Opposite.html#3914" class="Bound">_</a> <a id="3916" href="Categories.Bicategory.Opposite.html#3916" class="Bound">_</a> <a id="3918" href="Categories.Bicategory.Opposite.html#3918" class="Bound">f</a> <a id="3920" href="Categories.Bicategory.Opposite.html#3920" class="Bound">g</a> <a id="3922" href="Categories.Bicategory.Opposite.html#3922" class="Bound">h</a> <a id="3924" href="Categories.Bicategory.Opposite.html#3924" class="Bound">i</a><a id="3925" class="Symbol">}</a> <a id="3927" class="Symbol">→</a> <a id="3929" href="Relation.Binary.Reasoning.Syntax.html#1572" class="Function Operator">begin</a>
9898
<a id="3943" href="Categories.Bicategory.Extras.html#2442" class="Function">α⇐</a> <a id="3946" href="Categories.Bicategory.html#1916" class="Function Operator">◁</a> <a id="3948" href="Categories.Bicategory.Opposite.html#3924" class="Bound">i</a> <a id="3950" href="Categories.Bicategory.html#1825" class="Function Operator">∘ᵥ</a> <a id="3953" href="Categories.Bicategory.Extras.html#2442" class="Function">α⇐</a> <a id="3956" href="Categories.Bicategory.html#1825" class="Function Operator">∘ᵥ</a> <a id="3959" href="Categories.Bicategory.Opposite.html#3918" class="Bound">f</a> <a id="3961" href="Categories.Bicategory.html#2018" class="Function Operator">▷</a> <a id="3963" href="Categories.Bicategory.Extras.html#2442" class="Function">α⇐</a> <a id="3970" href="Relation.Binary.Reasoning.Syntax.html#7462" class="Function">≈˘⟨</a> <a id="3974" href="Categories.Category.Core.html#715" class="Function">hom.assoc</a> <a id="3984" href="Relation.Binary.Reasoning.Syntax.html#7462" class="Function">⟩</a>
99-
<a id="3994" class="Symbol">(</a><a id="3995" href="Categories.Bicategory.Extras.html#2442" class="Function">α⇐</a> <a id="3998" href="Categories.Bicategory.html#1916" class="Function Operator">◁</a> <a id="4000" href="Categories.Bicategory.Opposite.html#3924" class="Bound">i</a> <a id="4002" href="Categories.Bicategory.html#1825" class="Function Operator">∘ᵥ</a> <a id="4005" href="Categories.Bicategory.Extras.html#2442" class="Function">α⇐</a><a id="4007" class="Symbol">)</a> <a id="4009" href="Categories.Bicategory.html#1825" class="Function Operator">∘ᵥ</a> <a id="4012" href="Categories.Bicategory.Opposite.html#3918" class="Bound">f</a> <a id="4014" href="Categories.Bicategory.html#2018" class="Function Operator">▷</a> <a id="4016" href="Categories.Bicategory.Extras.html#2442" class="Function">α⇐</a> <a id="4021" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="4024" href="Categories.Bicategory.Extras.html#6304" class="Function">pentagon-inv</a> <a id="4037" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
99+
<a id="3994" class="Symbol">(</a><a id="3995" href="Categories.Bicategory.Extras.html#2442" class="Function">α⇐</a> <a id="3998" href="Categories.Bicategory.html#1916" class="Function Operator">◁</a> <a id="4000" href="Categories.Bicategory.Opposite.html#3924" class="Bound">i</a> <a id="4002" href="Categories.Bicategory.html#1825" class="Function Operator">∘ᵥ</a> <a id="4005" href="Categories.Bicategory.Extras.html#2442" class="Function">α⇐</a><a id="4007" class="Symbol">)</a> <a id="4009" href="Categories.Bicategory.html#1825" class="Function Operator">∘ᵥ</a> <a id="4012" href="Categories.Bicategory.Opposite.html#3918" class="Bound">f</a> <a id="4014" href="Categories.Bicategory.html#2018" class="Function Operator">▷</a> <a id="4016" href="Categories.Bicategory.Extras.html#2442" class="Function">α⇐</a> <a id="4021" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="4024" href="Categories.Bicategory.Extras.html#7491" class="Function">pentagon-inv</a> <a id="4037" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
100100
<a id="4047" href="Categories.Bicategory.Extras.html#2442" class="Function">α⇐</a> <a id="4050" href="Categories.Bicategory.html#1825" class="Function Operator">∘ᵥ</a> <a id="4053" href="Categories.Bicategory.Extras.html#2442" class="Function">α⇐</a> <a id="4074" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a>
101101
<a id="4080" class="Symbol">}</a>
102102
<a id="4086" class="Keyword">where</a> <a id="4092" class="Keyword">open</a> <a id="4097" href="Categories.Category.Core.html#2462" class="Module">hom.HomReasoning</a>
@@ -114,8 +114,8 @@
114114
<a id="4395" class="Symbol">;</a> <a id="4397" href="Categories.Enriched.Category.html#1317" class="Field">unitˡ</a> <a id="4405" class="Symbol">=</a> <a id="4407" href="Categories.NaturalTransformation.NaturalIsomorphism.html#1442" class="Function">NaturalIsomorphism.op′</a> <a id="4430" href="Categories.Enriched.Category.html#1317" class="Function">unitˡ</a>
115115
<a id="4442" class="Symbol">;</a> <a id="4444" href="Categories.Enriched.Category.html#1469" class="Field">unitʳ</a> <a id="4452" class="Symbol">=</a> <a id="4454" href="Categories.NaturalTransformation.NaturalIsomorphism.html#1442" class="Function">NaturalIsomorphism.op′</a> <a id="4477" href="Categories.Enriched.Category.html#1469" class="Function">unitʳ</a>
116116
<a id="4489" class="Symbol">}</a>
117-
<a id="4495" class="Symbol">;</a> <a id="4497" href="Categories.Bicategory.html#2561" class="Field">triangle</a> <a id="4507" class="Symbol">=</a> <a id="4509" href="Categories.Bicategory.Extras.html#5969" class="Function">triangle-inv</a>
118-
<a id="4526" class="Symbol">;</a> <a id="4528" href="Categories.Bicategory.html#2837" class="Field">pentagon</a> <a id="4538" class="Symbol">=</a> <a id="4540" href="Categories.Bicategory.Extras.html#6304" class="Function">pentagon-inv</a>
117+
<a id="4495" class="Symbol">;</a> <a id="4497" href="Categories.Bicategory.html#2561" class="Field">triangle</a> <a id="4507" class="Symbol">=</a> <a id="4509" href="Categories.Bicategory.Extras.html#7156" class="Function">triangle-inv</a>
118+
<a id="4526" class="Symbol">;</a> <a id="4528" href="Categories.Bicategory.html#2837" class="Field">pentagon</a> <a id="4538" class="Symbol">=</a> <a id="4540" href="Categories.Bicategory.Extras.html#7491" class="Function">pentagon-inv</a>
119119
<a id="4557" class="Symbol">}</a>
120120

121121
<a id="4560" class="Comment">-- The combined 1- and 2-cell dual of C.</a>

0 commit comments

Comments
 (0)