Slides of a (very) informal lecture of mine on the Curry-Howard correspondence
1 variables (p' p : ℝ≥0) 2 [fact (0 < p')] [fact (p' < p)] [fact (p ≤ 1)] 3 4 theorem liquid_tensor_experiment 5 (S : Profinite) (V : pBanach p) : 6 ∀ i > 0, Ext i (M_{p'} S) V ≅ 0 :=