Trebor

By the way, every untyped *normal* term can be typed in system F (for example λx. xx can be given the type Unit -> Unit where Unit = forall T. T -> T). And as a corollary, there exists an interpreter of system F in untyped lambda calculus operating on Godel encoded Church numerals, that can be given a type in system F itself.

@constantine@types.pl Can we also postulate fracture by saying every (A : Set) is isomorphic to the Sigma type over a pair of (A^○ : Tyᵇ, A^● : Tyᶠ A^○)? This should make inductive types a little easier to deal with.

@maxsnew More precisely, morphisms 1 -> Ω in a sheaf topos over a locale correspond bijectively to opens in the locale. So it's difficult to talk about which propositions are open. The effective topos is IMO very unsatisfactory in terms of its connection to topology. For example the Baire space (Nat -> Nat) and the Cantor space (Nat -> Bool) are homeomorphic in Eff. (As a corollary, the "seemingly impossible functional program" is invalid in Eff.) A better substitute would be the realizability topos over something like the relative pca of Kleene's second algebra over its computable part, but I haven't completely worked through this.

@hallasurvivor Suppose we define the algebra of quaternionic polynomials H as formal sums of terms like aqbqcqd... where a,b,c,d are quaternions and q is the variable. Real numbers commute with everything, so this forms an R-algebra. Recall that evaluation of real polynomials R[x] -> R^R is an injective homomorphism. It is however not true for quaternions H -> H^H. What kind of identities should we add to H to make it injective?

@ncf@types.pl There is the notion of a dominant functor, which is a functor i : A -> U such that for every object Y : U, there exists an object X : A such that we have a retract Y -> iX -> Y. There is no functoriality requirement on the r map though, and in fact A can be a discrete category.