proposition: Lemma transportable_GL: transportable GL.
proof: Proof. move => E F s g [[[fg gi] [_ gs]] sg tg] /setP_P sp. rewrite sg in gi gs; rewrite tg in gs. split; move =>[ha hb]; split. - move => a b aF bF; move: (gs a aF) (gs b bF) => [a' a'E av] [b' b'E bv]. move:(ha _ _ a'E b'E) => [c' h]. by exists (Vf g c'); apply/funI_P; ex_tac; aw; rewrite - av - bv. - move => a b /funI_P [u us ->] /funI_P [v vs ->]; aw => eq. move/setX_P: (sp _ us) => [pz /setX_P[pp pp1 pp2] qz]. move/setX_P: (sp _ vs) => [pz' /setX_P[pp' pp1' pp2'] qz']. move: (gi _ _ pp1 pp1' (pr1_def eq)) => eq1. move: (gi _ _ pp2 pp2' (pr2_def eq)) => eq2. have eq3: P u = P v by rewrite - pp - pp' eq1 eq2. by rewrite (hb _ _ us vs eq3). - move => a b aE bE. move: (Vf_target fg); rewrite sg tg => H. move: (ha _ _ (H _ aE) (H _ bE)) => [c /funI_P [z zs zv]]. exists (Q z). move/setX_P: (sp _ zs) => [pz /setX_P[pp pp1 pp2] qz]. rewrite (gi _ _ aE pp1 (pr1_def (pr1_def zv))). by rewrite (gi _ _ bE pp2 (pr2_def (pr1_def zv))) pp pz. - move => a b ias ibs spab. set u := (J (J (Vf g (P (P a))) (Vf g (Q (P a)))) (Vf g (Q a))). set v := (J (J (Vf g (P (P b))) (Vf g (Q (P b)))) (Vf g (Q b))). have r1: inc u (transport s g) by apply/funI_P; exists a. have r2: inc v (transport s g) by apply/funI_P; exists b. have puv: P u = P v by rewrite /u/v spab; aw. move:(hb _ _ r1 r2 puv); rewrite /u/v => /pr2_def eq. move/setX_P: (sp _ ias) => [pz /setX_P[pp pp1 pp2] qz]. move/setX_P: (sp _ ibs) => [pz' /setX_P[pp' pp1' pp2'] qz']. apply: pair_exten => //; apply:(gi _ _ qz qz' eq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)