-
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.
Merge pull request #19 from rahulc29/polymorphism
Polymorphism
- Loading branch information
Showing
372 changed files
with
42,542 additions
and
9,281 deletions.
There are no files selected for viewing
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 |
|---|---|---|
| @@ -1,3 +1,4 @@ | ||
| *.agdai | ||
| *.agda~ | ||
| *.DS_Store | ||
| *.lagda.md~ |
This file was deleted.
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,16 @@ | ||
| # Experiments with Realizability in Univalent Type Theory | ||
|
|
||
| This project formalises categorical realizability from the ground up in Cubical Agda. | ||
|
|
||
| Notable results include : | ||
|
|
||
| * The category of assemblies having all finite limits and being cartesian closed | ||
| * Modest sets are equivalent to partial surjections from the combinatory algebra | ||
| * The construction of the subquotient embedding from PERs to modest sets and that it is split essentially surjective on objects | ||
| * The internal logic of the realizability tripos | ||
| * The construction of the realizability topos | ||
|
|
||
| Current formalisation targets include : | ||
|
|
||
| * Uniform families of PERs indexed by assemblies form a small and complete fibration | ||
| * The category of assemblies is exactly the category of double negation stable objects of the realizability topos |
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.