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

Classical realizability #14

Draft
wants to merge 26 commits into
base: master
Choose a base branch
from
Draft

Classical realizability #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
26 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
cfb6c59
Start working on classical realizability
rahulc29 Feb 28, 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
20 changes: 20 additions & 0 deletions docs/Cubical.Data.Bool.Properties.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -410,4 +410,24 @@

<a id="separatedBool"></a><a id="12070" href="Cubical.Data.Bool.Properties.html#12070" class="Function">separatedBool</a> <a id="12084" class="Symbol">:</a> <a id="12086" href="Cubical.Relation.Nullary.Base.html#1284" class="Function">Separated</a> <a id="12096" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a>
<a id="12101" href="Cubical.Data.Bool.Properties.html#12070" class="Function">separatedBool</a> <a id="12115" class="Symbol">=</a> <a id="12117" href="Cubical.Relation.Nullary.Properties.html#6859" class="Function">Discrete→Separated</a> <a id="12136" href="Cubical.Data.Bool.Base.html#756" class="Function Operator">_≟_</a>


<a id="Bool→Bool→∙Bool"></a><a id="12142" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12158" class="Symbol">:</a> <a id="12160" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="12165" class="Symbol">→</a> <a id="12167" class="Symbol">(</a><a id="12168" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="12173" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="12175" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a><a id="12179" class="Symbol">)</a> <a id="12181" href="Cubical.Foundations.Pointed.Base.html#638" class="Function Operator">→∙</a> <a id="12184" class="Symbol">(</a><a id="12185" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="12190" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="12192" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a><a id="12196" class="Symbol">)</a>
<a id="12198" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12214" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12220" class="Symbol">=</a> <a id="12222" href="Cubical.Foundations.Pointed.Base.html#893" class="Function">idfun∙</a> <a id="12229" class="Symbol">_</a>
<a id="12231" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12247" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="12252" class="Symbol">=</a> <a id="12254" href="Cubical.Foundations.Pointed.Properties.html#2394" class="Function">const∙</a> <a id="12261" class="Symbol">_</a> <a id="12263" class="Symbol">_</a>

<a id="Iso-Bool→∙Bool-Bool"></a><a id="12266" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12286" class="Symbol">:</a> <a id="12288" href="Cubical.Foundations.Isomorphism.html#773" class="Record">Iso</a> <a id="12292" class="Symbol">((</a><a id="12294" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="12299" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="12301" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a><a id="12305" class="Symbol">)</a> <a id="12307" href="Cubical.Foundations.Pointed.Base.html#638" class="Function Operator">→∙</a> <a id="12310" class="Symbol">(</a><a id="12311" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="12316" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="12318" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a><a id="12322" class="Symbol">))</a> <a id="12325" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a>
<a id="12330" href="Cubical.Foundations.Isomorphism.html#885" class="Field">Iso.fun</a> <a id="12338" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12358" href="Cubical.Data.Bool.Properties.html#12358" class="Bound">f</a> <a id="12360" class="Symbol">=</a> <a id="12362" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12366" href="Cubical.Data.Bool.Properties.html#12358" class="Bound">f</a> <a id="12368" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a>
<a id="12374" href="Cubical.Foundations.Isomorphism.html#901" class="Field">Iso.inv</a> <a id="12382" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12402" class="Symbol">=</a> <a id="12404" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a>
<a id="12420" href="Cubical.Foundations.Isomorphism.html#917" class="Field">Iso.rightInv</a> <a id="12433" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12453" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12459" class="Symbol">=</a> <a id="12461" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="12466" href="Cubical.Foundations.Isomorphism.html#917" class="Field">Iso.rightInv</a> <a id="12479" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12499" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="12504" class="Symbol">=</a> <a id="12506" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="12511" href="Cubical.Foundations.Isomorphism.html#948" class="Field">Iso.leftInv</a> <a id="12523" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12543" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a> <a id="12545" class="Symbol">=</a> <a id="12547" href="Cubical.Data.Sigma.Properties.html#13744" class="Function">Σ≡Prop</a> <a id="12554" class="Symbol">(λ</a> <a id="12557" href="Cubical.Data.Bool.Properties.html#12557" class="Bound">_</a> <a id="12559" class="Symbol">→</a> <a id="12561" href="Cubical.Data.Bool.Properties.html#1800" class="Function">isSetBool</a> <a id="12571" class="Symbol">_</a> <a id="12573" class="Symbol">_)</a> <a id="12576" class="Symbol">(</a><a id="12577" href="Cubical.Data.Bool.Properties.html#12600" class="Function">help</a> <a id="12582" class="Symbol">_</a> <a id="12584" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a><a id="12588" class="Symbol">)</a>
<a id="12592" class="Keyword">where</a>
<a id="12600" href="Cubical.Data.Bool.Properties.html#12600" class="Function">help</a> <a id="12605" class="Symbol">:</a> <a id="12607" class="Symbol">(</a><a id="12608" href="Cubical.Data.Bool.Properties.html#12608" class="Bound">x</a> <a id="12610" class="Symbol">:</a> <a id="12612" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a><a id="12616" class="Symbol">)</a> <a id="12618" class="Symbol">→</a> <a id="12620" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12624" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a> <a id="12626" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12632" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="12634" href="Cubical.Data.Bool.Properties.html#12608" class="Bound">x</a>
<a id="12640" class="Symbol">→</a> <a id="12642" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12658" class="Symbol">(</a><a id="12659" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12663" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a> <a id="12665" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a><a id="12670" class="Symbol">)</a> <a id="12672" class="Symbol">.</a><a id="12673" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12677" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="12679" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a> <a id="12681" class="Symbol">.</a><a id="12682" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a>
<a id="12688" href="Cubical.Data.Bool.Properties.html#12600" class="Function">help</a> <a id="12693" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12699" href="Cubical.Data.Bool.Properties.html#12699" class="Bound">p</a> <a id="12701" class="Symbol">=</a> <a id="12703" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a>
<a id="12714" class="Symbol">λ</a> <a id="12716" class="Symbol">{</a> <a id="12718" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12724" class="Symbol">→</a> <a id="12726" class="Symbol">(λ</a> <a id="12729" href="Cubical.Data.Bool.Properties.html#12729" class="Bound">j</a> <a id="12731" class="Symbol">→</a> <a id="12733" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12749" class="Symbol">(</a><a id="12750" href="Cubical.Data.Bool.Properties.html#12699" class="Bound">p</a> <a id="12752" href="Cubical.Data.Bool.Properties.html#12729" class="Bound">j</a><a id="12753" class="Symbol">)</a> <a id="12755" class="Symbol">.</a><a id="12756" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12760" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a><a id="12765" class="Symbol">)</a> <a id="12767" href="Cubical.Foundations.Prelude.html#4776" class="Function Operator">∙</a> <a id="12769" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="12773" href="Cubical.Data.Bool.Properties.html#12699" class="Bound">p</a>
<a id="12781" class="Symbol">;</a> <a id="12783" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="12788" class="Symbol">→</a> <a id="12790" class="Symbol">(λ</a> <a id="12793" href="Cubical.Data.Bool.Properties.html#12793" class="Bound">j</a> <a id="12795" class="Symbol">→</a> <a id="12797" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12813" class="Symbol">(</a><a id="12814" href="Cubical.Data.Bool.Properties.html#12699" class="Bound">p</a> <a id="12816" href="Cubical.Data.Bool.Properties.html#12793" class="Bound">j</a><a id="12817" class="Symbol">)</a> <a id="12819" class="Symbol">.</a><a id="12820" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12824" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a><a id="12828" class="Symbol">)</a> <a id="12830" href="Cubical.Foundations.Prelude.html#4776" class="Function Operator">∙</a> <a id="12832" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="12836" class="Symbol">(</a><a id="12837" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="12841" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a><a id="12842" class="Symbol">)}</a>
<a id="12847" href="Cubical.Data.Bool.Properties.html#12600" class="Function">help</a> <a id="12852" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="12857" href="Cubical.Data.Bool.Properties.html#12857" class="Bound">p</a> <a id="12859" class="Symbol">=</a> <a id="12861" class="Symbol">(λ</a> <a id="12864" href="Cubical.Data.Bool.Properties.html#12864" class="Bound">j</a> <a id="12866" class="Symbol">→</a> <a id="12868" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12884" class="Symbol">(</a><a id="12885" href="Cubical.Data.Bool.Properties.html#12857" class="Bound">p</a> <a id="12887" href="Cubical.Data.Bool.Properties.html#12864" class="Bound">j</a><a id="12888" class="Symbol">)</a> <a id="12890" class="Symbol">.</a><a id="12891" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a><a id="12894" class="Symbol">)</a>
<a id="12910" href="Cubical.Foundations.Prelude.html#4776" class="Function Operator">∙</a> <a id="12912" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="12919" class="Symbol">λ</a> <a id="12921" class="Symbol">{</a> <a id="12923" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12929" class="Symbol">→</a> <a id="12931" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="12935" href="Cubical.Data.Bool.Properties.html#12857" class="Bound">p</a> <a id="12937" class="Symbol">;</a> <a id="12939" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="12944" class="Symbol">→</a> <a id="12946" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="12950" class="Symbol">(</a><a id="12951" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="12955" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a><a id="12956" class="Symbol">)}</a>
</pre></body></html>
Loading
Loading