Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Polymorphism #17

Merged
merged 19 commits into from
Sep 19, 2024
Merged

Polymorphism #17

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
05772cc
Start working on general case for subobject classifiers
rahulc29 Apr 16, 2024
4e956d4
Define PERs
rahulc29 May 2, 2024
26be6f0
Define PERs and refactor assembly modules
rahulc29 May 6, 2024
bd065f5
Start working towards LCCC on Mod
rahulc29 May 15, 2024
56dbf84
Remove files not caught in gitignore
rahulc29 May 15, 2024
a5d8149
Partial Surjections stuff
rahulc29 May 20, 2024
b40f374
Show modest set morphisms are equivalent to partial surjection morphisms
rahulc29 May 20, 2024
f06f4a1
Right adjoint to pullback functor ASM
rahulc29 May 25, 2024
d644d36
Archive
rahulc29 May 30, 2024
827bf93
Archive
rahulc29 Jun 5, 2024
41d4f18
Finite Limits for PERs
rahulc29 Jun 25, 2024
73d04b5
Families of modest sets as displayed category
rahulc29 Jun 26, 2024
1c1ecc3
Define Small PERs and Equivalence to ordinary PERs
rahulc29 Jun 27, 2024
2d33f50
Subquotient modest set and canonical PER of a modest set
rahulc29 Jul 4, 2024
0c8e626
Subquotient and Canonical PER Operations
rahulc29 Jul 5, 2024
75c6f59
Fix performance issues
rahulc29 Jul 7, 2024
1b95e78
Isomorphism of PERs and Modest Sets
rahulc29 Aug 16, 2024
a84a79b
Subquotient functor
rahulc29 Aug 25, 2024
02fc360
Render HTML
rahulc29 Sep 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
*.agdai
*.agda~
*.DS_Store
*.lagda.md~
62 changes: 0 additions & 62 deletions Dockerfile
View file
Open in desktop

This file was deleted.

104 changes: 104 additions & 0 deletions docs/Categories.CartesianMorphism.html
View file
Open in desktop

Large diffs are not rendered by default.

30 changes: 30 additions & 0 deletions docs/Categories.GenericObject.html
View file
Open in desktop
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">ℓ&#39;B</a> <a id="385" href="Categories.GenericObject.html#385" class="Bound">ℓE</a> <a id="388" href="Categories.GenericObject.html#388" class="Bound">ℓ&#39;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">ℓ&#39;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">ℓ&#39;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">ℓ&#39;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">ℓ&#39;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>
Loading
Loading