lagda trial

Trinitarianism/README.md

@@ -1 +1,39 @@
-Some text
+
+Trinitarianism
+==============
+By the end of this arc we will have 'a place to do maths'. 
+The following features will have three interpretations:
+ - Proof theoretic, with types as propositions
+ - Type theoretic, with types as programs
+ - Category theoretic, with types as objects in a category
+
+<!-- insert picture of trinitarianism -->
+
+## Terms and Types
+
+Here are some things that we could like to have in a 'place to do maths'
+  - objects to reason about (like ℕ)
+  - recipes for making things inside objects (like + 1)
+  - propositions to reason with (with the data of proofs) (like _ = 0)
+
+In proof theory, types are propositions and terms of a type are their proofs.
+In type theory, types are programs and terms are algorithms.
+In category theory, types are objects and terms are generalised elements.
+
+## Non-dependent Types
+
+- false / empty / initial object
+- true / unit / terminal object
+- or / sum / coproduct
+- and / pairs / product
+- implication / functions / internal hom
+
+# Dependent Types
+
+- predicate / type family / over category
+- substitution / substitution / pullback
+- existence / Σ type / left adjoint to pullback 
+- for all / Π type / right adjoint to pullback
+
+
+> Question: how do we talk about equality?