Code

Classical realizability#14

Code

Draft

rahulc29 wants to merge 26 commits intomasterrahulc29/realizability:masterfrom 13-classical-realizabilityrahulc29/realizability:13-classical-realizabilityCopy head branch name to clipboard

+3,006-1,015

Commits

Commits on Jan 23, 2024

• Add soundness for propositional connectives

  rahulc29

  committed
  1dc4f0d

  Copy full SHA for 1dc4f0d

Commits on Jan 24, 2024

• Update case for existentials

  rahulc29

  committed
  51c7bfc

  Copy full SHA for 51c7bfc

Commits on Jan 25, 2024

• Prove soundness of substitution for existential

  rahulc29

  committed
  98df49c

  Copy full SHA for 98df49c

• Soundness of substitution and some combinators

  rahulc29

  committed
  c6a18ca

  Copy full SHA for c6a18ca

Commits on Jan 29, 2024

• Interpret quantifiers

  rahulc29

  committed
  eb9a962

  Copy full SHA for eb9a962

Commits on Jan 30, 2024

• Define topos objects

  rahulc29

  committed
  7223be4

  Copy full SHA for 7223be4

• Render HTML

  rahulc29

  committed
  940dcfe

  Copy full SHA for 940dcfe

• Define functional relations

  rahulc29

  committed
  f6af9d5

  Copy full SHA for f6af9d5

• Add introduction rules for natural deduction

  rahulc29

  committed
  83130e9

  Copy full SHA for 83130e9

• Add functional relation stuff

  rahulc29

  committed
  458d257

  Copy full SHA for 458d257

Commits on Feb 2, 2024

• Commit before refactor

  rahulc29

  committed
  3375b73

  Copy full SHA for 3375b73

Commits on Feb 6, 2024

• Start working on relational context structural operations

  rahulc29

  committed
  0a0ef50

  Copy full SHA for 0a0ef50

Commits on Feb 8, 2024

• Prove that weakening of relational context preserves realizers

  rahulc29

  committed
  1019d79

  Copy full SHA for 1019d79

• Update Topos Modules

  rahulc29

  committed
  bce456a

  Copy full SHA for bce456a

• Finish weakening boilerplate

  rahulc29

  committed
  b268c8e

  Copy full SHA for b268c8e

• Prove strictness of identity

  rahulc29

  committed
  452726a

  Copy full SHA for 452726a

• Add documentation

  rahulc29

  committed
  1ceb218

  Copy full SHA for 1ceb218

Commits on Feb 12, 2024

• Define topos object and morphisms

  rahulc29

  committed
  60e4c40

  Copy full SHA for 60e4c40

Commits on Feb 13, 2024

• Finish goals

  rahulc29

  committed
  8f196fc

  Copy full SHA for 8f196fc

Commits on Feb 16, 2024

• Add terminal object of RT

  rahulc29

  committed
  2e1ee97

  Copy full SHA for 2e1ee97

Commits on Feb 24, 2024

• Add algebraic realisability relatiobn

  rahulc29

  committed
  4d7bc8e

  Copy full SHA for 4d7bc8e

• Start using algebraic predicates

  rahulc29

  committed
  b35fcdb

  Copy full SHA for b35fcdb

Commits on Feb 26, 2024

• Archive commit

  rahulc29

  committed
  8d69eab

  Copy full SHA for 8d69eab

Commits on Feb 27, 2024

• Revert to preorder predicates

  rahulc29

  committed
  026a925

  Copy full SHA for 026a925

• Archive state

  rahulc29

  committed
  8029847

  Copy full SHA for 8029847

Commits on Feb 28, 2024

• Start working on classical realizability

  rahulc29

  committed
  cfb6c59

  Copy full SHA for cfb6c59