Interoperability between proofs: A problem with universes

In STTFA, the the fact there is som subtyping and impredicativity makes proofs incompatible in Agda a priori. Hence the question: Can we get rid off the subtyping and impredicativity in those proofs?

Mainly, the problem of cumulativity (or subtyping) as it is in STTFA is a matter of code duplication. For impredicativity, it is a bit different: An impredicative proof cannot always turned into a predicative proof. And at the time of writing there is no static check to know whether an impredicative proof can be turned into a predicative one (notice that I do not really define impredicative/predicative in this setting).

Going from STTFA into Agda requires some tricks to do on the universes. We know that Universo can already be used to check whether an impredicative proof can be turned into a predicative one.

Given that Universo already exists, the question is whether we could avoid the code duplication and let Universo does that for us by using universe polymorphism? This would have two benefits:

• Agda already knows universe polymorphism, so it would be a lighter translation than code duplication which would also make the library more idiomatic
• This would allow us to reuse Universo as a tool and would avoid us to write new machinery

The plan

Here is a scheme of a plan to do that:

1. Turn the library written in the sttfa encoding into the cts encoding with the sttfa specification

2. Run Universo to translate this library into the cts specification

3. If it works, you are done

4. If it does not work, bisect to find the smallest part of the library which fails and identify the problem. Likely, it is either because of impredicativity or cumulativity.

5. Step 4 should allow to identify a problematic constant. Make this constant universe polymorphic (as discussed during the last meeting). (try to do the minimal changes, not all sorts need to be generalised). For example: foo : cts.univ cts.star cts.box cts.I can be turned into foo: s1 : cts.Sort -> s2 : cts.Sort -> p : cts.eps cts.true -> cts.univ s1 s2 p.

6. Now, you need to instrument all the proofs using foo. Likely, to do that automatically, I suggest the following:

   a. Add into the context ?1 : cts.Sort. before the proof you need to instrument. You can do that several times to get several "buffers".
   b. Then, you can replace foo by foo ?1 ?2 cts.I
   c. Now, ask Dedukti to type check. Probably, you will get an error such as: foo ?1 ?2 cts.I is ill-typed. I expected cts.?1 and inferred cts.star. So what you need to do is just rewrite foo ?1 ?2 cts.I by foo cts.start ?2 cts.I.
   d. Do that again, and Dedukti will tell you to replace ?2 by cts.box
   e. Notice that in this case, all the inhabitant of cts.eps cts.true should be cts.I hence, this is why the third argument of foo is cts.I directly.

7. Repeat step 6 for every usage of foo

8. Go back to step 2.

Algorithm for generating universe polymorphic version of types

This is psuedocode

let dsu = ref DSU.t (* Disjoint Set Union *)

let rec join x y = match x, y with
| (A x), (A y) 			-> join x y
| (A -> B), (U -> V) 		-> join A U; join B V
| (x : A => B), (y : U => V) 	-> join A U; join B V
| x, y 				-> dsu := DSU.join !dsu x y


(* infer returns type of term *)
let rec infer ctx term = match term with
| (f t1 t2 ... tn) -> 
	let [A1, A2, ..., An, An+1] = infer ctx f in (* f : A1 -> A2 -> .. -> An+1 *)
	for i=1..n
		join (normalize Ai) (normalize (infer ti));
	An+1
| (x : A => y) ->
	let B = infer (ctx::(x : A)) y in
	A -> B
| ((x : A) -> y) ->
	let B = infer (ctx::(x : A)) y in
	TYPE
| t ->
	ctx[t] (* Type of t as per context *)

addvar typ =
(* 
	replace cts.box, cts.diamond, cts.I ... and their types with
	variables x1, x2, ...

	So for example (this is leibniz's type in CTS encoding)

	  cts.Term
	    cts.diamond
	    (cts.prod
	       cts.triangle
	       cts.diamond
	       cts.diamond
	       cts.I
	       (cts.univ cts.box cts.triangle cts.I)
	       (t => 
	          cts.prod ctx.box ctx.box cts.box cts.I x
		           (t1 => cts.prod ...
	
	Becomes:
	(x1 : x31) -> (x2 : x32) -> (x3 : x33) -> ... -> (x30 : x60) ->
	  cts.Term
	    x1
	    (cts.prod
	       x2
	       x3
	       x4
	       x5
	       (cts.univ x6 x7 x8)
	       (t : x9 => 
	          cts.prod x10 x11 x12 x13 t
		           (t1 => cts.prod ...
*)

let replWithPar term =
(*
	Replace all variables xi with DSU.parent !dsu xi
*)

let rec polymorphirise typ =
	dsu := DSU.empty
	let typ = addvar typ in 
	let _ = infer typ in
	replWithPar typ