-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
51 changed files
with
4,354 additions
and
1,853 deletions.
There are no files selected for viewing
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,30 @@ | ||
| <!DOCTYPE HTML> | ||
| <html><head><meta charset="utf-8"><title>Categories.GenericObject</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Keyword">open</a> <a id="6" class="Keyword">import</a> <a id="13" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a> | ||
| <a id="41" class="Keyword">open</a> <a id="46" class="Keyword">import</a> <a id="53" href="Cubical.Categories.Category.html" class="Module">Cubical.Categories.Category</a> | ||
| <a id="81" class="Keyword">open</a> <a id="86" class="Keyword">import</a> <a id="93" href="Cubical.Categories.Displayed.Base.html" class="Module">Cubical.Categories.Displayed.Base</a> | ||
| <a id="127" class="Keyword">open</a> <a id="132" class="Keyword">import</a> <a id="139" href="Cubical.Foundations.Equiv.html" class="Module">Cubical.Foundations.Equiv</a> | ||
| <a id="165" class="Keyword">open</a> <a id="170" class="Keyword">import</a> <a id="177" href="Cubical.Foundations.HLevels.html" class="Module">Cubical.Foundations.HLevels</a> | ||
| <a id="205" class="Keyword">open</a> <a id="210" class="Keyword">import</a> <a id="217" href="Cubical.Data.Sigma.html" class="Module">Cubical.Data.Sigma</a> | ||
| <a id="236" class="Keyword">open</a> <a id="241" class="Keyword">import</a> <a id="248" href="Cubical.HITs.PropositionalTruncation.html" class="Module">Cubical.HITs.PropositionalTruncation</a> | ||
| <a id="285" class="Keyword">open</a> <a id="290" class="Keyword">import</a> <a id="297" href="Categories.CartesianMorphism.html" class="Module">Categories.CartesianMorphism</a> | ||
|
|
||
| <a id="327" class="Keyword">module</a> <a id="334" href="Categories.GenericObject.html" class="Module">Categories.GenericObject</a> <a id="359" class="Keyword">where</a> | ||
|
|
||
| <a id="366" class="Keyword">module</a> <a id="373" href="Categories.GenericObject.html#373" class="Module">_</a> | ||
| <a id="377" class="Symbol">{</a><a id="378" href="Categories.GenericObject.html#378" class="Bound">ℓB</a> <a id="381" href="Categories.GenericObject.html#381" class="Bound">ℓ'B</a> <a id="385" href="Categories.GenericObject.html#385" class="Bound">ℓE</a> <a id="388" href="Categories.GenericObject.html#388" class="Bound">ℓ'E</a><a id="391" class="Symbol">}</a> | ||
| <a id="395" class="Symbol">{</a><a id="396" href="Categories.GenericObject.html#396" class="Bound">B</a> <a id="398" class="Symbol">:</a> <a id="400" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="409" href="Categories.GenericObject.html#378" class="Bound">ℓB</a> <a id="412" href="Categories.GenericObject.html#381" class="Bound">ℓ'B</a><a id="415" class="Symbol">}</a> | ||
| <a id="419" class="Symbol">(</a><a id="420" href="Categories.GenericObject.html#420" class="Bound">E</a> <a id="422" class="Symbol">:</a> <a id="424" href="Cubical.Categories.Displayed.Base.html#457" class="Record">Categoryᴰ</a> <a id="434" href="Categories.GenericObject.html#396" class="Bound">B</a> <a id="436" href="Categories.GenericObject.html#385" class="Bound">ℓE</a> <a id="439" href="Categories.GenericObject.html#388" class="Bound">ℓ'E</a><a id="442" class="Symbol">)</a> <a id="444" class="Keyword">where</a> | ||
|
|
||
| <a id="453" class="Keyword">open</a> <a id="458" href="Cubical.Categories.Category.Base.html#334" class="Module">Category</a> <a id="467" href="Categories.GenericObject.html#396" class="Bound">B</a> | ||
| <a id="471" class="Keyword">open</a> <a id="476" href="Cubical.Categories.Displayed.Base.html#457" class="Module">Categoryᴰ</a> <a id="486" href="Categories.GenericObject.html#420" class="Bound">E</a> | ||
| <a id="490" class="Keyword">open</a> <a id="495" href="Categories.CartesianMorphism.html#336" class="Module">Contravariant</a> <a id="509" href="Categories.GenericObject.html#420" class="Bound">E</a> | ||
|
|
||
| <a id="514" class="Keyword">record</a> <a id="521" href="Categories.GenericObject.html#521" class="Record">GenericObject</a> <a id="535" class="Symbol">:</a> <a id="537" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="542" class="Symbol">(</a><a id="543" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="549" class="Symbol">(</a><a id="550" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="556" href="Categories.GenericObject.html#378" class="Bound">ℓB</a> <a id="559" href="Categories.GenericObject.html#381" class="Bound">ℓ'B</a><a id="562" class="Symbol">)</a> <a id="564" class="Symbol">(</a><a id="565" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="571" href="Categories.GenericObject.html#385" class="Bound">ℓE</a> <a id="574" href="Categories.GenericObject.html#388" class="Bound">ℓ'E</a><a id="577" class="Symbol">))</a> <a id="580" class="Keyword">where</a> | ||
| <a id="590" class="Keyword">constructor</a> <a id="602" href="Categories.GenericObject.html#602" class="InductiveConstructor">makeGenericObject</a> | ||
| <a id="624" class="Keyword">field</a> | ||
| <a id="636" href="Categories.GenericObject.html#636" class="Field">base</a> <a id="641" class="Symbol">:</a> <a id="643" href="Cubical.Categories.Category.Base.html#452" class="Function">ob</a> | ||
| <a id="652" href="Categories.GenericObject.html#652" class="Field">displayed</a> <a id="662" class="Symbol">:</a> <a id="664" href="Cubical.Categories.Displayed.Base.html#607" class="Field Operator">ob[</a> <a id="668" href="Categories.GenericObject.html#636" class="Field">base</a> <a id="673" href="Cubical.Categories.Displayed.Base.html#607" class="Field Operator">]</a> | ||
| <a id="681" href="Categories.GenericObject.html#681" class="Field">isGeneric</a> <a id="691" class="Symbol">:</a> | ||
| <a id="701" class="Symbol">∀</a> <a id="703" class="Symbol">{</a><a id="704" href="Categories.GenericObject.html#704" class="Bound">t</a> <a id="706" class="Symbol">:</a> <a id="708" href="Cubical.Categories.Category.Base.html#452" class="Function">ob</a><a id="710" class="Symbol">}</a> <a id="712" class="Symbol">(</a><a id="713" href="Categories.GenericObject.html#713" class="Bound">tᴰ</a> <a id="716" class="Symbol">:</a> <a id="718" href="Cubical.Categories.Displayed.Base.html#607" class="Field Operator">ob[</a> <a id="722" href="Categories.GenericObject.html#704" class="Bound">t</a> <a id="724" href="Cubical.Categories.Displayed.Base.html#607" class="Field Operator">]</a><a id="725" class="Symbol">)</a> | ||
| <a id="735" class="Symbol">→</a> <a id="737" href="Cubical.Core.Primitives.html#6268" class="Function">Σ[</a> <a id="740" href="Categories.GenericObject.html#740" class="Bound">f</a> <a id="742" href="Cubical.Core.Primitives.html#6268" class="Function">∈</a> <a id="744" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">Hom[</a> <a id="749" href="Categories.GenericObject.html#704" class="Bound">t</a> <a id="751" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">,</a> <a id="753" href="Categories.GenericObject.html#636" class="Field">base</a> <a id="758" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">]</a> <a id="760" href="Cubical.Core.Primitives.html#6268" class="Function">]</a> <a id="762" href="Cubical.Core.Primitives.html#6268" class="Function">Σ[</a> <a id="765" href="Categories.GenericObject.html#765" class="Bound">fᴰ</a> <a id="768" href="Cubical.Core.Primitives.html#6268" class="Function">∈</a> <a id="770" href="Cubical.Categories.Displayed.Base.html#633" class="Field Operator">Hom[</a> <a id="775" href="Categories.GenericObject.html#740" class="Bound">f</a> <a id="777" href="Cubical.Categories.Displayed.Base.html#633" class="Field Operator">][</a> <a id="780" href="Categories.GenericObject.html#713" class="Bound">tᴰ</a> <a id="783" href="Cubical.Categories.Displayed.Base.html#633" class="Field Operator">,</a> <a id="785" href="Categories.GenericObject.html#652" class="Field">displayed</a> <a id="795" href="Cubical.Categories.Displayed.Base.html#633" class="Field Operator">]</a> <a id="797" href="Cubical.Core.Primitives.html#6268" class="Function">]</a> <a id="799" href="Categories.CartesianMorphism.html#477" class="Function">isCartesian</a> <a id="811" href="Categories.GenericObject.html#740" class="Bound">f</a> <a id="813" href="Categories.GenericObject.html#765" class="Bound">fᴰ</a> | ||
| </pre></body></html> |
Oops, something went wrong.