I had a question for the great people of https://constructive-maths.zulipchat.com, but I think I'll ask here just in case...

I'm struggling with formalizing the normalization for STLC (really system T) in HA2, even on paper! The stumbling block is the definition of the interpretation of types $[\![ T ]\!]\subseteq {\cal SN}$.

In Coq I'd do this:

```
Fixpoint interp (t : type) : term -> Prop :=
match t with
| Nat => (* the set of terms that reduce to a numeral *)
| Arrow t1 t2 => (* the realizability arrow over the interpretation of t1 and t2 *)
end.
```

How do I code this with HA2? I'm suspecting "something something Tarski fixed-point theorem", but some clarification would be much appreciated.

Note that my "real" definition is mutually inductive, so any reference that handles that is appreciated (but not required).

AFAIK you can't really define internally a type by large dependent elimination in HA2 (this would require a form of choice) but if you present this intepretation inductively you can define it by the usual impredicative encoding.

That is, you encode instead

```
Inductive interp : type -> (term -> Prop) -> Prop :=
| nat_interp : interp nat (the set of terms that realize numerals)
| arr_interp : forall σ σi τ τi, interp σ σi -> interp τ τi -> interp (arr σ τ) (Fun σi τi)
```

Such inductive declarations can be systematically translated into HA2.

That mostly makes sense, thanks!

I'm a bit worried about that second argument of `interp`

, though, can you remind me what the encoding is (roughly)?

Last updated: Oct 13 2024 at 01:02 UTC