diff --git a/README.org~ b/README.org~
deleted file mode 100644
index 8f2c425..0000000
--- a/README.org~
+++ /dev/null
@@ -1,73 +0,0 @@
-# Experiments with Realizability in Univalent Type Theory
-
-This repository contains accompanying code for my (upcoming) Bachelor's thesis. I am studying categorical realisability through the lens of univalent type theory. 
-
-This formalisation loosely follows my study (see the timeline below). Much of the development has been done inside Agda first, so it is convenient
-for me to think using a cubical viewpoint, but most of the results should directly translate over to their Book HoTT analogues. 
-
-This project is very much a work-in-progress, so the code is not very pretty - it is littered with `{!!}` and `--allow-unsolved-metas`. 
-Most of the holes have comments alongside them that explain how to fill that hole.
-
-I periodically clean and reorganise the code.
-
-
-# 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.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.
-
-# Timeline
-
-Weak timeline :
-
-Upto November 2023:
-
-- [x] Combinatory Algebras
-  - [x] Applicative Structures
-  - [x] Feferman structure on an AS
-  - [x] Combinatorial completeness
-  - [ ] Computation rule for $\lambda*$
-  - Combinators
-    - [x] Identity, booleans, if-then-else, pairs, projections, B combinator, some Curry numerals
-    - [x] Computation rule for pairs 
-    - [ ] Fixpoint combinators and primitive recursion combinator
-- [x] Category of Assemblies
-  - [x] Define assemblies
-  - [x] Define the category $\mathsf{Asm}$
-  - [x] Cartesian closure and similar structure
-    - [x] Binary products
-    - [x] Binary coproducts
-      - [x] Universal property
-    - [x] Equalisers
-    - [x] Exponentials
-    - [x] Initial and terminal objects
-    - [x] Coequalisers (December 2023)
-
-December 2023:
-
-- [ ] $\mathsf{Asm}$ is regular
-    - [x] Kernel pairs of morphisms exist
-    - [x] Kernel pairs have coequalisers
-    - [ ] Regular epics stable under pullback
-- [ ] 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