Update README.md

README.md

@@ -36,14 +36,28 @@ December 2023:
 - [ ] Exact completion
     - [x] Internal equivalence relations of a category
     - [ ] Functional relations
+- [ ] Tripos
+	- [x] Heyting-valued Predicates
+	- [x] $\forall$ and $\exists$ are adjoints
+	- [x] Beck-Chevalley condition
+	- [ ] Heyting prealgebra structure
+	- [ ] Interpret intuitionistic logic
+
+# Code Organisation
+
+- At the highest level, we have combinatory algebra machinery
+- Most modules are parameterised by a combinatory algebra `ca : CombinatoryAlgebra A`
+- There are modules on the category of assemblies in `Realizability.Assembly`
+- Lemmas and stuff relating to the regularity of $\mathsf{Asm}$ is found in `Realizability.Assembly.Regular`
+- Tripos modules are to be found in `Realizability.Tripos`
 
 # Writing
 
 There are some notes relating to the project on my [abstract non-sense](https://github.com/rahulc29/abstract-nonsense) repository.
 
 # Build Instructions
 
-You will need Agda >= 2.6.3 and a [custom fork](https://github.com/rahulc29/cubical/tree/rahulc29/realizability) of the Cubical library to build the code.
+You will need Agda >= 2.6.4 and a [custom fork](https://github.com/rahulc29/cubical/tree/rahulc29/realizability) of the Cubical library to build the code.
 
 The custom fork has a few additional definitions in the category theory modules. I will hopefully integrate them into the Cubical library.
 

src/Realizability/Assembly/Base.agda

@@ -1,7 +1,9 @@
 {-# OPTIONS --cubical #-}
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
 open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation
 open import Cubical.Reflection.RecordEquiv
 open import Realizability.CombinatoryAlgebra
 
@@ -18,9 +20,11 @@ module Realizability.Assembly.Base {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra
   AssemblyΣ : Type ℓ → Type _
   AssemblyΣ X =
     Σ[ isSetX ∈ isSet X ]
-    Σ[ _⊩_ ∈ (A → X → Type ℓ) ]
-    Σ[ ⊩isPropValued ∈ (∀ a x → isProp (a ⊩ x)) ]
-    (∀ x → ∃[ a ∈ A ] a ⊩ x)
+    Σ[ _⊩_ ∈ (A → X → hProp ℓ) ]
+    (∀ x → ∃[ a ∈ A ] ⟨ a ⊩ x ⟩)
+
+  isSetAssemblyΣ : ∀ X → isSet (AssemblyΣ X)
+  isSetAssemblyΣ X = isSetΣ (isProp→isSet isPropIsSet) λ isSetX → isSetΣ (isSetΠ (λ a → isSetΠ λ x → isSetHProp)) λ _⊩_ → isSetΠ λ x → isProp→isSet isPropPropTrunc
 
   unquoteDecl AssemblyIsoΣ = declareRecordIsoΣ AssemblyIsoΣ (quote Assembly)
 

src/Realizability/Assembly/Path.agda

@@ -14,6 +14,7 @@ open import Cubical.Categories.Category
 module Realizability.Assembly.Path {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
 open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a; P to PCombinator)
 open import Realizability.Assembly.Base ca
 open import Realizability.Assembly.Morphism ca
 

src/Realizability/Assembly/Regular/Cobase.agda

@@ -54,7 +54,7 @@ module
           (s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ b) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id))) ⨾ Id ,
           λ z zᵣ zᵣ⊩z →
             do
-              return ({!!} , {!!}))
+              return ({!!} , {!!} , {!!}))
 
 module _ (cl : CharLemma) where
   open ASMKernelPairs

src/Realizability/Assembly/SIP.agda

@@ -0,0 +1,17 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.SIP
+open import Realizability.CombinatoryAlgebra
+
+module Realizability.Assembly.SIP {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+
+open import Realizability.Assembly.Base ca
+open import Realizability.Assembly.Morphism ca
+
+
+AssemblyStr : (X : Type ℓ) → Type _
+AssemblyStr X = AssemblyΣ X
+
+AssemblyStrEquiv : StrEquiv AssemblyStr _
+AssemblyStrEquiv =
+  λ { (X , isSetX , _⊩X_ , ⊩Xsurjective) (Y , isSetY , _⊩Y_ , ⊩Ysurjective) e → {!!} }