Show that the Isomorphism satisfied by L^gl is an isomorhism of predomains
We defined the type L^gl X = (∀ k . L k X). We can show that this satisfies the following isomorphism:
L^gl X ≅ (∀ k . X) + 1 + L^gl X
We can define a predomain structure on L^gl X by taking the relation to be
x ≤ y iff ∀ k . (x k) ≤ (y k) in L k X
The goal of this Issue is to show in Agda that L^gl defined as above satisfies the above isomorphism at the level of predomains. This involves the following:
-
Show that L^gl satisfies the isomorphism at the level of types -
Define the predomain structure on L^gl -
Show that the predomain satisfies the above isomorphism
Edited by ericgio