Skip to content

Commit

Permalink
Deploying to gh-pages from @ 5fe4366 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@felixwellen
felixwellen committed Aug 22, 2023
1 parent 544f301 commit 0f84518
Show file tree
Hide file tree
Showing 77 changed files with 4,208 additions and 3,923 deletions.
24 changes: 12 additions & 12 deletions Cubical.Algebra.CommRing.Localisation.Limit.html
View file

Large diffs are not rendered by default.

42 changes: 21 additions & 21 deletions Cubical.Algebra.ZariskiLattice.StructureSheaf.html
View file

Large diffs are not rendered by default.

16 changes: 8 additions & 8 deletions Cubical.Algebra.ZariskiLattice.StructureSheafPullback.html
View file

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions Cubical.Categories.Abelian.Base.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,10 +87,10 @@
<a id="2348" href="Cubical.Categories.Abelian.Base.html#2348" class="Bound">e</a> <a id="2350" href="Cubical.Categories.Abelian.Base.html#2273" class="Function Operator">=coker</a> <a id="2357" href="Cubical.Categories.Abelian.Base.html#2357" class="Bound">f</a> <a id="2359" class="Symbol">=</a> <a id="2361" href="Cubical.Categories.Abelian.Base.html#930" class="Record">IsCokernel</a> <a id="2372" href="Cubical.Categories.Additive.Base.html#2552" class="Function">preaddcat</a> <a id="2382" href="Cubical.Categories.Abelian.Base.html#2357" class="Bound">f</a> <a id="2384" href="Cubical.Categories.Abelian.Base.html#2348" class="Bound">e</a>

<a id="2389" class="Keyword">field</a>
<a id="AbelianCategoryStr.monNormal"></a><a id="2399" href="Cubical.Categories.Abelian.Base.html#2399" class="Field">monNormal</a> <a id="2409" class="Symbol">:</a> <a id="2411" class="Symbol">{</a><a id="2412" href="Cubical.Categories.Abelian.Base.html#2412" class="Bound">x</a> <a id="2414" href="Cubical.Categories.Abelian.Base.html#2414" class="Bound">y</a> <a id="2416" class="Symbol">:</a> <a id="2418" href="Cubical.Categories.Category.Base.html#452" class="Function">ob</a><a id="2420" class="Symbol">}</a> <a id="2422" class="Symbol">→</a> <a id="2424" class="Symbol">(</a><a id="2425" href="Cubical.Categories.Abelian.Base.html#2425" class="Bound">m</a> <a id="2427" class="Symbol">:</a> <a id="2429" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">Hom[</a> <a id="2434" href="Cubical.Categories.Abelian.Base.html#2412" class="Bound">x</a> <a id="2436" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">,</a> <a id="2438" href="Cubical.Categories.Abelian.Base.html#2414" class="Bound">y</a> <a id="2440" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">]</a><a id="2441" class="Symbol">)</a> <a id="2443" class="Symbol">→</a> <a id="2445" href="Cubical.Categories.Morphism.html#388" class="Function">isMonic</a> <a id="2453" href="Cubical.Categories.Additive.Base.html#1232" class="Function">cat</a> <a id="2457" href="Cubical.Categories.Abelian.Base.html#2425" class="Bound">m</a>
<a id="AbelianCategoryStr.monNormal"></a><a id="2399" href="Cubical.Categories.Abelian.Base.html#2399" class="Field">monNormal</a> <a id="2409" class="Symbol">:</a> <a id="2411" class="Symbol">{</a><a id="2412" href="Cubical.Categories.Abelian.Base.html#2412" class="Bound">x</a> <a id="2414" href="Cubical.Categories.Abelian.Base.html#2414" class="Bound">y</a> <a id="2416" class="Symbol">:</a> <a id="2418" href="Cubical.Categories.Category.Base.html#452" class="Function">ob</a><a id="2420" class="Symbol">}</a> <a id="2422" class="Symbol">→</a> <a id="2424" class="Symbol">(</a><a id="2425" href="Cubical.Categories.Abelian.Base.html#2425" class="Bound">m</a> <a id="2427" class="Symbol">:</a> <a id="2429" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">Hom[</a> <a id="2434" href="Cubical.Categories.Abelian.Base.html#2412" class="Bound">x</a> <a id="2436" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">,</a> <a id="2438" href="Cubical.Categories.Abelian.Base.html#2414" class="Bound">y</a> <a id="2440" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">]</a><a id="2441" class="Symbol">)</a> <a id="2443" class="Symbol">→</a> <a id="2445" href="Cubical.Categories.Morphism.html#428" class="Function">isMonic</a> <a id="2453" href="Cubical.Categories.Additive.Base.html#1232" class="Function">cat</a> <a id="2457" href="Cubical.Categories.Abelian.Base.html#2425" class="Bound">m</a>
<a id="2465" class="Symbol">→</a> <a id="2467" href="Cubical.Core.Primitives.html#6268" class="Function">Σ[</a> <a id="2470" href="Cubical.Categories.Abelian.Base.html#2470" class="Bound">z</a> <a id="2472" href="Cubical.Core.Primitives.html#6268" class="Function">∈</a> <a id="2474" href="Cubical.Categories.Category.Base.html#452" class="Function">ob</a> <a id="2477" href="Cubical.Core.Primitives.html#6268" class="Function">]</a> <a id="2479" href="Cubical.Core.Primitives.html#6268" class="Function">Σ[</a> <a id="2482" href="Cubical.Categories.Abelian.Base.html#2482" class="Bound">f</a> <a id="2484" href="Cubical.Core.Primitives.html#6268" class="Function">∈</a> <a id="2486" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">Hom[</a> <a id="2491" href="Cubical.Categories.Abelian.Base.html#2414" class="Bound">y</a> <a id="2493" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">,</a> <a id="2495" href="Cubical.Categories.Abelian.Base.html#2470" class="Bound">z</a> <a id="2497" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">]</a> <a id="2499" href="Cubical.Core.Primitives.html#6268" class="Function">]</a> <a id="2501" class="Symbol">(</a><a id="2502" href="Cubical.Categories.Abelian.Base.html#2425" class="Bound">m</a> <a id="2504" href="Cubical.Categories.Abelian.Base.html#2161" class="Function Operator">=ker</a> <a id="2509" href="Cubical.Categories.Abelian.Base.html#2482" class="Bound">f</a><a id="2510" class="Symbol">)</a>

<a id="AbelianCategoryStr.epiNormal"></a><a id="2517" href="Cubical.Categories.Abelian.Base.html#2517" class="Field">epiNormal</a> <a id="2527" class="Symbol">:</a> <a id="2529" class="Symbol">{</a><a id="2530" href="Cubical.Categories.Abelian.Base.html#2530" class="Bound">x</a> <a id="2532" href="Cubical.Categories.Abelian.Base.html#2532" class="Bound">y</a> <a id="2534" class="Symbol">:</a> <a id="2536" href="Cubical.Categories.Category.Base.html#452" class="Function">ob</a><a id="2538" class="Symbol">}</a> <a id="2540" class="Symbol">→</a> <a id="2542" class="Symbol">(</a><a id="2543" href="Cubical.Categories.Abelian.Base.html#2543" class="Bound">e</a> <a id="2545" class="Symbol">:</a> <a id="2547" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">Hom[</a> <a id="2552" href="Cubical.Categories.Abelian.Base.html#2530" class="Bound">x</a> <a id="2554" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">,</a> <a id="2556" href="Cubical.Categories.Abelian.Base.html#2532" class="Bound">y</a> <a id="2558" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">]</a><a id="2559" class="Symbol">)</a> <a id="2561" class="Symbol">→</a> <a id="2563" href="Cubical.Categories.Morphism.html#514" class="Function">isEpic</a> <a id="2570" href="Cubical.Categories.Additive.Base.html#1232" class="Function">cat</a> <a id="2574" href="Cubical.Categories.Abelian.Base.html#2543" class="Bound">e</a>
<a id="AbelianCategoryStr.epiNormal"></a><a id="2517" href="Cubical.Categories.Abelian.Base.html#2517" class="Field">epiNormal</a> <a id="2527" class="Symbol">:</a> <a id="2529" class="Symbol">{</a><a id="2530" href="Cubical.Categories.Abelian.Base.html#2530" class="Bound">x</a> <a id="2532" href="Cubical.Categories.Abelian.Base.html#2532" class="Bound">y</a> <a id="2534" class="Symbol">:</a> <a id="2536" href="Cubical.Categories.Category.Base.html#452" class="Function">ob</a><a id="2538" class="Symbol">}</a> <a id="2540" class="Symbol">→</a> <a id="2542" class="Symbol">(</a><a id="2543" href="Cubical.Categories.Abelian.Base.html#2543" class="Bound">e</a> <a id="2545" class="Symbol">:</a> <a id="2547" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">Hom[</a> <a id="2552" href="Cubical.Categories.Abelian.Base.html#2530" class="Bound">x</a> <a id="2554" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">,</a> <a id="2556" href="Cubical.Categories.Abelian.Base.html#2532" class="Bound">y</a> <a id="2558" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">]</a><a id="2559" class="Symbol">)</a> <a id="2561" class="Symbol">→</a> <a id="2563" href="Cubical.Categories.Morphism.html#1466" class="Function">isEpic</a> <a id="2570" href="Cubical.Categories.Additive.Base.html#1232" class="Function">cat</a> <a id="2574" href="Cubical.Categories.Abelian.Base.html#2543" class="Bound">e</a>
<a id="2582" class="Symbol">→</a> <a id="2584" href="Cubical.Core.Primitives.html#6268" class="Function">Σ[</a> <a id="2587" href="Cubical.Categories.Abelian.Base.html#2587" class="Bound">w</a> <a id="2589" href="Cubical.Core.Primitives.html#6268" class="Function">∈</a> <a id="2591" href="Cubical.Categories.Category.Base.html#452" class="Function">ob</a> <a id="2594" href="Cubical.Core.Primitives.html#6268" class="Function">]</a> <a id="2596" href="Cubical.Core.Primitives.html#6268" class="Function">Σ[</a> <a id="2599" href="Cubical.Categories.Abelian.Base.html#2599" class="Bound">f</a> <a id="2601" href="Cubical.Core.Primitives.html#6268" class="Function">∈</a> <a id="2603" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">Hom[</a> <a id="2608" href="Cubical.Categories.Abelian.Base.html#2587" class="Bound">w</a> <a id="2610" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">,</a> <a id="2612" href="Cubical.Categories.Abelian.Base.html#2530" class="Bound">x</a> <a id="2614" href="Cubical.Categories.Category.Base.html#468" class="Function Operator">]</a> <a id="2616" href="Cubical.Core.Primitives.html#6268" class="Function">]</a> <a id="2618" class="Symbol">(</a><a id="2619" href="Cubical.Categories.Abelian.Base.html#2543" class="Bound">e</a> <a id="2621" href="Cubical.Categories.Abelian.Base.html#2273" class="Function Operator">=coker</a> <a id="2628" href="Cubical.Categories.Abelian.Base.html#2599" class="Bound">f</a><a id="2629" class="Symbol">)</a>


Expand Down
Loading

0 comments on commit 0f84518

Please sign in to comment.