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

Realizability Topos of an Arbitrary Total Combinatory Algebra #11

Merged
merged 40 commits into from
May 2, 2024
Merged

Realizability Topos of an Arbitrary Total Combinatory Algebra #11

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
1dc4f0d
Add soundness for propositional connectives
rahulc29 Jan 23, 2024
51c7bfc
Update case for existentials
rahulc29 Jan 24, 2024
98df49c
Prove soundness of substitution for existential
rahulc29 Jan 25, 2024
c6a18ca
Soundness of substitution and some combinators
rahulc29 Jan 25, 2024
eb9a962
Interpret quantifiers
rahulc29 Jan 29, 2024
7223be4
Define topos objects
rahulc29 Jan 30, 2024
940dcfe
Render HTML
rahulc29 Jan 30, 2024
f6af9d5
Define functional relations
rahulc29 Jan 30, 2024
83130e9
Add introduction rules for natural deduction
rahulc29 Jan 30, 2024
458d257
Add functional relation stuff
rahulc29 Jan 30, 2024
3375b73
Commit before refactor
rahulc29 Feb 2, 2024
0a0ef50
Start working on relational context structural operations
rahulc29 Feb 6, 2024
1019d79
Prove that weakening of relational context preserves realizers
rahulc29 Feb 8, 2024
bce456a
Update Topos Modules
rahulc29 Feb 8, 2024
b268c8e
Finish weakening boilerplate
rahulc29 Feb 8, 2024
452726a
Prove strictness of identity
rahulc29 Feb 8, 2024
1ceb218
Add documentation
rahulc29 Feb 8, 2024
60e4c40
Define topos object and morphisms
rahulc29 Feb 12, 2024
8f196fc
Finish goals
rahulc29 Feb 13, 2024
2e1ee97
Add terminal object of RT
rahulc29 Feb 16, 2024
4d7bc8e
Add algebraic realisability relatiobn
rahulc29 Feb 24, 2024
b35fcdb
Start using algebraic predicates
rahulc29 Feb 24, 2024
8d69eab
Archive commit
rahulc29 Feb 26, 2024
026a925
Revert to preorder predicates
rahulc29 Feb 27, 2024
8029847
Archive state
rahulc29 Feb 27, 2024
48f8ce2
Switch to new definitions
rahulc29 Feb 29, 2024
6e6052f
Redo terminal object
rahulc29 Feb 29, 2024
5b2a98f
Refactor binary products
rahulc29 Mar 3, 2024
18b9d94
Universal property of equalisers
rahulc29 Mar 6, 2024
6a7058d
Show mere existence of equalisers
rahulc29 Mar 6, 2024
fde0671
Realizer for universal property of binary products
rahulc29 Mar 12, 2024
3fe30b9
Add equalisation of equalisers
rahulc29 Mar 13, 2024
adf534a
Functional relations that represent monics
rahulc29 Mar 14, 2024
73a0508
Characterise subobjects in terms of strict relations
rahulc29 Mar 26, 2024
a4b8679
Formulate propositional resizing
rahulc29 Mar 28, 2024
4f82984
Define resized predicates and subobject classifier
rahulc29 Apr 1, 2024
796a4d4
Complete refactor
rahulc29 Apr 2, 2024
9238eb7
Archival commit
rahulc29 Apr 8, 2024
3d55e7c
Change predicate
rahulc29 Apr 8, 2024
a16d85c
Add subobject classifier
rahulc29 Apr 15, 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
728 changes: 364 additions & 364 deletions docs/Cubical.Categories.Adjoint.html
View file
Open in desktop

Large diffs are not rendered by default.

238 changes: 123 additions & 115 deletions docs/Cubical.Categories.Category.Base.html
View file
Open in desktop

Large diffs are not rendered by default.

58 changes: 29 additions & 29 deletions docs/Cubical.Categories.Category.Properties.html
View file
Open in desktop

Large diffs are not rendered by default.

12 changes: 6 additions & 6 deletions docs/Cubical.Categories.Constructions.BinProduct.html
View file
Open in desktop

Large diffs are not rendered by default.

114 changes: 114 additions & 0 deletions docs/Cubical.Categories.Constructions.Elements.html
View file
Open in desktop

Large diffs are not rendered by default.

395 changes: 395 additions & 0 deletions docs/Cubical.Categories.Constructions.Slice.Base.html
View file
Open in desktop

Large diffs are not rendered by default.

66 changes: 66 additions & 0 deletions docs/Cubical.Categories.Constructions.Slice.Properties.html
View file
Open in desktop

Large diffs are not rendered by default.

18 changes: 18 additions & 0 deletions docs/Cubical.Categories.Constructions.Slice.html
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Categories.Constructions.Slice</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--safe</a> <a id="20" class="Symbol">#-}</a>

<a id="25" class="Keyword">open</a> <a id="30" class="Keyword">import</a> <a id="37" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a>

<a id="66" class="Keyword">open</a> <a id="71" class="Keyword">import</a> <a id="78" href="Cubical.Categories.Category.html" class="Module">Cubical.Categories.Category</a>

<a id="107" class="Keyword">open</a> <a id="112" href="Cubical.Categories.Category.Base.html#334" class="Module">Category</a>

<a id="122" class="Keyword">module</a> <a id="129" href="Cubical.Categories.Constructions.Slice.html" class="Module">Cubical.Categories.Constructions.Slice</a>
<a id="170" class="Symbol">{</a><a id="171" href="Cubical.Categories.Constructions.Slice.html#171" class="Bound">ℓ</a> <a id="173" href="Cubical.Categories.Constructions.Slice.html#173" class="Bound">ℓ&#39;</a> <a id="176" class="Symbol">:</a> <a id="178" href="Agda.Primitive.html#742" class="Postulate">Level</a><a id="183" class="Symbol">}</a>
<a id="187" class="Symbol">(</a><a id="188" href="Cubical.Categories.Constructions.Slice.html#188" class="Bound">C</a> <a id="190" class="Symbol">:</a> <a id="192" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="201" href="Cubical.Categories.Constructions.Slice.html#171" class="Bound">ℓ</a> <a id="203" href="Cubical.Categories.Constructions.Slice.html#173" class="Bound">ℓ&#39;</a><a id="205" class="Symbol">)</a>
<a id="209" class="Symbol">(</a><a id="210" href="Cubical.Categories.Constructions.Slice.html#210" class="Bound">c</a> <a id="212" class="Symbol">:</a> <a id="214" href="Cubical.Categories.Constructions.Slice.html#188" class="Bound">C</a> <a id="216" class="Symbol">.</a><a id="217" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a><a id="219" class="Symbol">)</a>
<a id="223" class="Keyword">where</a>

<a id="230" class="Keyword">open</a> <a id="235" class="Keyword">import</a> <a id="242" href="Cubical.Categories.Constructions.Slice.Base.html" class="Module">Cubical.Categories.Constructions.Slice.Base</a> <a id="286" href="Cubical.Categories.Constructions.Slice.html#188" class="Bound">C</a> <a id="288" href="Cubical.Categories.Constructions.Slice.html#210" class="Bound">c</a> <a id="290" class="Keyword">public</a>
<a id="297" class="Keyword">open</a> <a id="302" class="Keyword">import</a> <a id="309" href="Cubical.Categories.Constructions.Slice.Properties.html" class="Module">Cubical.Categories.Constructions.Slice.Properties</a> <a id="359" href="Cubical.Categories.Constructions.Slice.html#188" class="Bound">C</a> <a id="361" href="Cubical.Categories.Constructions.Slice.html#210" class="Bound">c</a> <a id="363" class="Keyword">public</a>
</pre></body></html>
93 changes: 93 additions & 0 deletions docs/Cubical.Categories.Constructions.SubObject.html
View file
Open in desktop

Large diffs are not rendered by default.

41 changes: 41 additions & 0 deletions docs/Cubical.Categories.Equivalence.Base.html
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Categories.Equivalence.Base</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--safe</a> <a id="20" class="Symbol">#-}</a>
<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.Categories.Equivalence.Base.html" class="Module">Cubical.Categories.Equivalence.Base</a> <a id="67" class="Keyword">where</a>

<a id="74" class="Keyword">open</a> <a id="79" class="Keyword">import</a> <a id="86" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a>

<a id="115" class="Keyword">open</a> <a id="120" class="Keyword">import</a> <a id="127" href="Cubical.HITs.PropositionalTruncation.html" class="Module">Cubical.HITs.PropositionalTruncation</a>

<a id="165" class="Keyword">open</a> <a id="170" class="Keyword">import</a> <a id="177" href="Cubical.Categories.Category.html" class="Module">Cubical.Categories.Category</a>
<a id="205" class="Keyword">open</a> <a id="210" class="Keyword">import</a> <a id="217" href="Cubical.Categories.Functor.html" class="Module">Cubical.Categories.Functor</a>
<a id="244" class="Keyword">open</a> <a id="249" class="Keyword">import</a> <a id="256" href="Cubical.Categories.NaturalTransformation.html" class="Module">Cubical.Categories.NaturalTransformation</a>

<a id="298" class="Keyword">open</a> <a id="303" href="Cubical.Categories.Category.Base.html#334" class="Module">Category</a>
<a id="312" class="Keyword">open</a> <a id="317" href="Cubical.Categories.Functor.Base.html#441" class="Module">Functor</a>

<a id="326" class="Keyword">private</a>
<a id="336" class="Keyword">variable</a>
<a id="349" href="Cubical.Categories.Equivalence.Base.html#349" class="Generalizable">ℓC</a> <a id="352" href="Cubical.Categories.Equivalence.Base.html#352" class="Generalizable">ℓC&#39;</a> <a id="356" href="Cubical.Categories.Equivalence.Base.html#356" class="Generalizable">ℓD</a> <a id="359" href="Cubical.Categories.Equivalence.Base.html#359" class="Generalizable">ℓD&#39;</a> <a id="363" class="Symbol">:</a> <a id="365" href="Agda.Primitive.html#742" class="Postulate">Level</a>

<a id="372" class="Keyword">record</a> <a id="WeakInverse"></a><a id="379" href="Cubical.Categories.Equivalence.Base.html#379" class="Record">WeakInverse</a> <a id="391" class="Symbol">{</a><a id="392" href="Cubical.Categories.Equivalence.Base.html#392" class="Bound">C</a> <a id="394" class="Symbol">:</a> <a id="396" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="405" href="Cubical.Categories.Equivalence.Base.html#349" class="Generalizable">ℓC</a> <a id="408" href="Cubical.Categories.Equivalence.Base.html#352" class="Generalizable">ℓC&#39;</a><a id="411" class="Symbol">}</a> <a id="413" class="Symbol">{</a><a id="414" href="Cubical.Categories.Equivalence.Base.html#414" class="Bound">D</a> <a id="416" class="Symbol">:</a> <a id="418" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="427" href="Cubical.Categories.Equivalence.Base.html#356" class="Generalizable">ℓD</a> <a id="430" href="Cubical.Categories.Equivalence.Base.html#359" class="Generalizable">ℓD&#39;</a><a id="433" class="Symbol">}</a>
<a id="456" class="Symbol">(</a><a id="457" href="Cubical.Categories.Equivalence.Base.html#457" class="Bound">func</a> <a id="462" class="Symbol">:</a> <a id="464" href="Cubical.Categories.Functor.Base.html#441" class="Record">Functor</a> <a id="472" href="Cubical.Categories.Equivalence.Base.html#392" class="Bound">C</a> <a id="474" href="Cubical.Categories.Equivalence.Base.html#414" class="Bound">D</a><a id="475" class="Symbol">)</a> <a id="477" class="Symbol">:</a> <a id="479" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="484" class="Symbol">(</a><a id="485" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="491" class="Symbol">(</a><a id="492" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="498" href="Cubical.Categories.Equivalence.Base.html#405" class="Bound">ℓC</a> <a id="501" href="Cubical.Categories.Equivalence.Base.html#408" class="Bound">ℓC&#39;</a><a id="504" class="Symbol">)</a> <a id="506" class="Symbol">(</a><a id="507" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="513" href="Cubical.Categories.Equivalence.Base.html#427" class="Bound">ℓD</a> <a id="516" href="Cubical.Categories.Equivalence.Base.html#430" class="Bound">ℓD&#39;</a><a id="519" class="Symbol">))</a> <a id="522" class="Keyword">where</a>
<a id="530" class="Keyword">field</a>
<a id="WeakInverse.invFunc"></a><a id="540" href="Cubical.Categories.Equivalence.Base.html#540" class="Field">invFunc</a> <a id="548" class="Symbol">:</a> <a id="550" href="Cubical.Categories.Functor.Base.html#441" class="Record">Functor</a> <a id="558" href="Cubical.Categories.Equivalence.Base.html#414" class="Bound">D</a> <a id="560" href="Cubical.Categories.Equivalence.Base.html#392" class="Bound">C</a>

<a id="WeakInverse.η"></a><a id="567" href="Cubical.Categories.Equivalence.Base.html#567" class="Field">η</a> <a id="569" class="Symbol">:</a> <a id="571" href="Cubical.Categories.Functor.Base.html#4025" class="Function Operator">𝟙⟨</a> <a id="574" href="Cubical.Categories.Equivalence.Base.html#392" class="Bound">C</a> <a id="576" href="Cubical.Categories.Functor.Base.html#4025" class="Function Operator">⟩</a> <a id="578" href="Cubical.Categories.NaturalTransformation.Base.html#2633" class="Function Operator">≅ᶜ</a> <a id="581" href="Cubical.Categories.Equivalence.Base.html#540" class="Field">invFunc</a> <a id="589" href="Cubical.Categories.Functor.Base.html#4767" class="Function Operator">∘F</a> <a id="592" href="Cubical.Categories.Equivalence.Base.html#457" class="Bound">func</a>
<a id="WeakInverse.ε"></a><a id="601" href="Cubical.Categories.Equivalence.Base.html#601" class="Field">ε</a> <a id="603" class="Symbol">:</a> <a id="605" href="Cubical.Categories.Equivalence.Base.html#457" class="Bound">func</a> <a id="610" href="Cubical.Categories.Functor.Base.html#4767" class="Function Operator">∘F</a> <a id="613" href="Cubical.Categories.Equivalence.Base.html#540" class="Field">invFunc</a> <a id="621" href="Cubical.Categories.NaturalTransformation.Base.html#2633" class="Function Operator">≅ᶜ</a> <a id="624" href="Cubical.Categories.Functor.Base.html#4025" class="Function Operator">𝟙⟨</a> <a id="627" href="Cubical.Categories.Equivalence.Base.html#414" class="Bound">D</a> <a id="629" href="Cubical.Categories.Functor.Base.html#4025" class="Function Operator">⟩</a>

<a id="632" class="Comment">-- I don&#39;t know of a good alternative representation of isEquivalence that</a>
<a id="707" class="Comment">-- avoids truncation in the general case. If the categories are univalent, then</a>
<a id="788" class="Comment">-- an adjoint equivalence might be enough.</a>
<a id="isEquivalence"></a><a id="831" href="Cubical.Categories.Equivalence.Base.html#831" class="Function">isEquivalence</a> <a id="845" class="Symbol">:</a> <a id="847" class="Symbol">{</a><a id="848" href="Cubical.Categories.Equivalence.Base.html#848" class="Bound">C</a> <a id="850" class="Symbol">:</a> <a id="852" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="861" href="Cubical.Categories.Equivalence.Base.html#349" class="Generalizable">ℓC</a> <a id="864" href="Cubical.Categories.Equivalence.Base.html#352" class="Generalizable">ℓC&#39;</a><a id="867" class="Symbol">}</a> <a id="869" class="Symbol">{</a><a id="870" href="Cubical.Categories.Equivalence.Base.html#870" class="Bound">D</a> <a id="872" class="Symbol">:</a> <a id="874" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="883" href="Cubical.Categories.Equivalence.Base.html#356" class="Generalizable">ℓD</a> <a id="886" href="Cubical.Categories.Equivalence.Base.html#359" class="Generalizable">ℓD&#39;</a><a id="889" class="Symbol">}</a>
<a id="905" class="Symbol">→</a> <a id="907" class="Symbol">(</a><a id="908" href="Cubical.Categories.Equivalence.Base.html#908" class="Bound">func</a> <a id="913" class="Symbol">:</a> <a id="915" href="Cubical.Categories.Functor.Base.html#441" class="Record">Functor</a> <a id="923" href="Cubical.Categories.Equivalence.Base.html#848" class="Bound">C</a> <a id="925" href="Cubical.Categories.Equivalence.Base.html#870" class="Bound">D</a><a id="926" class="Symbol">)</a> <a id="928" class="Symbol">→</a> <a id="930" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="935" class="Symbol">(</a><a id="936" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="942" class="Symbol">(</a><a id="943" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="949" href="Cubical.Categories.Equivalence.Base.html#349" class="Generalizable">ℓC</a> <a id="952" href="Cubical.Categories.Equivalence.Base.html#352" class="Generalizable">ℓC&#39;</a><a id="955" class="Symbol">)</a> <a id="957" class="Symbol">(</a><a id="958" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="964" href="Cubical.Categories.Equivalence.Base.html#356" class="Generalizable">ℓD</a> <a id="967" href="Cubical.Categories.Equivalence.Base.html#359" class="Generalizable">ℓD&#39;</a><a id="970" class="Symbol">))</a>
<a id="973" href="Cubical.Categories.Equivalence.Base.html#831" class="Function">isEquivalence</a> <a id="987" href="Cubical.Categories.Equivalence.Base.html#987" class="Bound">func</a> <a id="992" class="Symbol">=</a> <a id="994" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥</a> <a id="996" href="Cubical.Categories.Equivalence.Base.html#379" class="Record">WeakInverse</a> <a id="1008" href="Cubical.Categories.Equivalence.Base.html#987" class="Bound">func</a> <a id="1013" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥₁</a>

<a id="1017" class="Keyword">record</a> <a id="_≃ᶜ_"></a><a id="1024" href="Cubical.Categories.Equivalence.Base.html#1024" class="Record Operator">_≃ᶜ_</a> <a id="1029" class="Symbol">(</a><a id="1030" href="Cubical.Categories.Equivalence.Base.html#1030" class="Bound">C</a> <a id="1032" class="Symbol">:</a> <a id="1034" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="1043" href="Cubical.Categories.Equivalence.Base.html#349" class="Generalizable">ℓC</a> <a id="1046" href="Cubical.Categories.Equivalence.Base.html#352" class="Generalizable">ℓC&#39;</a><a id="1049" class="Symbol">)</a> <a id="1051" class="Symbol">(</a><a id="1052" href="Cubical.Categories.Equivalence.Base.html#1052" class="Bound">D</a> <a id="1054" class="Symbol">:</a> <a id="1056" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="1065" href="Cubical.Categories.Equivalence.Base.html#356" class="Generalizable">ℓD</a> <a id="1068" href="Cubical.Categories.Equivalence.Base.html#359" class="Generalizable">ℓD&#39;</a><a id="1071" class="Symbol">)</a> <a id="1073" class="Symbol">:</a>
<a id="1090" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="1095" class="Symbol">(</a><a id="1096" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="1102" class="Symbol">(</a><a id="1103" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="1109" href="Cubical.Categories.Equivalence.Base.html#1043" class="Bound">ℓC</a> <a id="1112" href="Cubical.Categories.Equivalence.Base.html#1046" class="Bound">ℓC&#39;</a><a id="1115" class="Symbol">)</a> <a id="1117" class="Symbol">(</a><a id="1118" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="1124" href="Cubical.Categories.Equivalence.Base.html#1065" class="Bound">ℓD</a> <a id="1127" href="Cubical.Categories.Equivalence.Base.html#1068" class="Bound">ℓD&#39;</a><a id="1130" class="Symbol">))</a> <a id="1133" class="Keyword">where</a>
<a id="1141" class="Keyword">constructor</a> <a id="equivᶜ"></a><a id="1153" href="Cubical.Categories.Equivalence.Base.html#1153" class="InductiveConstructor">equivᶜ</a>
<a id="1162" class="Keyword">field</a>
<a id="_≃ᶜ_.func"></a><a id="1172" href="Cubical.Categories.Equivalence.Base.html#1172" class="Field">func</a> <a id="1177" class="Symbol">:</a> <a id="1179" href="Cubical.Categories.Functor.Base.html#441" class="Record">Functor</a> <a id="1187" href="Cubical.Categories.Equivalence.Base.html#1030" class="Bound">C</a> <a id="1189" href="Cubical.Categories.Equivalence.Base.html#1052" class="Bound">D</a>
<a id="_≃ᶜ_.isEquiv"></a><a id="1195" href="Cubical.Categories.Equivalence.Base.html#1195" class="Field">isEquiv</a> <a id="1203" class="Symbol">:</a> <a id="1205" href="Cubical.Categories.Equivalence.Base.html#831" class="Function">isEquivalence</a> <a id="1219" href="Cubical.Categories.Equivalence.Base.html#1172" class="Field">func</a>
</pre></body></html>
Loading
Loading