%%%%% Map into the singleton language %%%%% map : con -> eterm -> type. tmap : kind -> etp -> type. tmap/t : tmap t et. tmap/sing : tmap (sing C) (esing M) <- map C M. tmap/pi : tmap (pi K1 K2) (epi A1 A2) <- tmap K1 A1 <- ({a} {x} map a x -> tmap (K2 a) (A2 x)). tmap/sigma : tmap (sigma K1 K2) (esigma A1 A2) <- tmap K1 A1 <- ({a} {x} map a x -> tmap (K2 a) (A2 x)). tmap/one : tmap one eone. map/pair : map (pair C1 C2) (epair M1 M2) <- map C1 M1 <- map C2 M2. map/pi1 : map (pi1 C) (epi1 M) <- map C M. map/pi2 : map (pi2 C) (epi2 M) <- map C M. map/lam : map (lam K C) (elam A M) <- tmap K A <- ({a} {x} map a x -> map (C a) (M x)). map/app : map (app C1 C2) (eapp M1 M2) <- map C1 M1 <- map C2 M2. map/star : map star estar. map/unit : map unit (econst const/unit). map/void : map void (econst const/void). map/prod : map (prod C1 C2) (eapp (eapp (econst const/prod) M1) M2) <- map C1 M1 <- map C2 M2. map/arrow : map (arrow C1 C2) (eapp (eapp (econst const/arrow) M1) M2) <- map C1 M1 <- map C2 M2. map/plus : map (plus C1 C2) (eapp (eapp (econst const/plus) M1) M2) <- map C1 M1 <- map C2 M2. map/ref : map (ref C) (eapp (econst const/ref) M) <- map C M. map/tag : map (tag C) (eapp (econst const/tag) M) <- map C M. map/tagged : map tagged (econst const/tagged). map/rec : map (rec K C1 C2) (eapp (econst (const/rec SK)) (epair MA (epair (elam (epi A ([_] et)) ([x] elam A ([y] M1 x y))) M2))) <- tmap K A <- ({a} {x} map a x -> {b} {y} map b y -> map (C1 a b) (M1 x y)) <- map C2 M2 <- flay A SK MA. map/labeled : map (labeled I C) (eapp (econst (const/labeled I)) M) <- map C M. %%%%% Map from the singleton language %%%%% unmap : eterm -> con -> type. tunmap : etp -> kind -> type. tunmap/t : tunmap et t. tunmap/sing : tunmap (esing M) (sing C) <- unmap M C. tunmap/pi : tunmap (epi A1 A2) (pi K1 K2) <- tunmap A1 K1 <- ({x} {a} unmap x a -> tunmap (A2 x) (K2 a)). tunmap/sigma : tunmap (esigma A1 A2) (sigma K1 K2) <- tunmap A1 K1 <- ({x} {a} unmap x a -> tunmap (A2 x) (K2 a)). tunmap/one : tunmap eone one. unmap/app : unmap (eapp M1 M2) (app C1 C2) <- unmap M1 C1 <- unmap M2 C2. unmap/pi1 : unmap (epi1 M) (pi1 C) <- unmap M C. unmap/pi2 : unmap (epi2 M) (pi2 C) <- unmap M C. unmap/lam : unmap (elam A M) (lam K C) <- tunmap A K <- ({x} {a} unmap x a -> unmap (M x) (C a)). unmap/pair : unmap (epair M1 M2) (pair C1 C2) <- unmap M1 C1 <- unmap M2 C2. unmap/star : unmap estar star. unmap/unit : unmap (econst const/unit) unit. unmap/void : unmap (econst const/void) void. unmap/prod : unmap (econst const/prod) (lam t ([a] lam t ([b] prod a b))). unmap/arrow : unmap (econst const/arrow) (lam t ([a] lam t ([b] arrow a b))). unmap/plus : unmap (econst const/plus) (lam t ([a] lam t ([b] plus a b))). unmap/ref : unmap (econst const/ref) (lam t ([a] ref a)). unmap/tag : unmap (econst const/tag) (lam t ([a] tag a)). unmap/tagged : unmap (econst const/tagged) tagged. unmap/rec : unmap (econst (const/rec SK)) (lam (sigma K ([a] kprod (karrow (karrow (L a) t) (karrow (L a) t)) (L a))) ([b] rec (L (pi1 b)) ([c] [d] app (app (pi1 (pi2 b)) c) d) (pi2 (pi2 b)))) <- skof-il SK K L. unmap/labeled : unmap (econst (const/labeled I)) (lam t ([a] labeled I a)). %block unmap-block : some {a:con} block {x:eterm} {xt:unmap x a}. %%%%% Equality %%%%% unmap-resp : eterm-eq M M' -> con-eq C C' -> unmap M C -> unmap M' C' -> type. %mode unmap-resp +X1 +X2 +X3 -X4. - : unmap-resp _ _ D D. %worlds (conblock | unmap-block) (unmap-resp _ _ _ _). %total {} (unmap-resp _ _ _ _). tunmap-resp : etp-eq A A' -> kind-eq K K' -> tunmap A K -> tunmap A' K' -> type. %mode tunmap-resp +X1 +X2 +X3 -X4. - : tunmap-resp _ _ D D. %worlds (conblock | unmap-block) (tunmap-resp _ _ _ _). %total {} (tunmap-resp _ _ _ _). %%%%% Map Effectiveness %%%%% can-map : {C} map C M -> type. %mode can-map +X1 -X2. can-tmap : {K} tmap K A -> type. %mode can-tmap +X1 -X2. %block can-map-bind : some {m:eterm} block {a:con} {at:map a m} {thm:can-map a at}. %block map-bind-for-can-map : some {b:etp} {k:kind} block {x:eterm} {d:evof x b} {a:con} {e:cn-of a k} {at:map a x} {thm:can-map a at}. %block invert-bind-for-can-map : some {K:kind} {K':kind} {B:etp} {DmapK:tmap K B} {DmapB:tunmap B K'} {DwfK:kd-wf K} {DwfB:ewf B} {DequivK:kd-equiv K K'} block {a:con} {da:cn-of a K} {das:cn-assm da} {_:mcn-assm da das} {_:cn-of-reg da DwfK} {x:eterm} {dx:evof x B} {at:map a x} {xt:unmap x a} {_:can-map a at}. - : can-map _ (map/app D2 D1) <- can-map _ D1 <- can-map _ D2. - : can-map _ (map/pi1 D) <- can-map _ D. - : can-map _ (map/pi2 D) <- can-map _ D. - : can-map _ (map/lam D2 D1) <- can-tmap _ D1 <- ({x} {a} {d:map a x} can-map a d -> can-map _ (D2 a x d)). - : can-map _ (map/pair D2 D1) <- can-map _ D1 <- can-map _ D2. - : can-map _ map/star. - : can-map _ map/unit. - : can-map _ map/void. - : can-map _ map/tagged. - : can-map _ (map/ref D) <- can-map _ D. - : can-map _ (map/tag D) <- can-map _ D. - : can-map _ (map/labeled D) <- can-map _ D. - : can-map _ (map/arrow D2 D1) <- can-map _ D1 <- can-map _ D2. - : can-map _ (map/prod D2 D1) <- can-map _ D1 <- can-map _ D2. - : can-map _ (map/plus D2 D1) <- can-map _ D1 <- can-map _ D2. - : can-map _ (map/rec Dflay D3 D2 D1) <- can-tmap _ D1 <- ({x} {a} {d:map a x} can-map a d -> {y} {b} {e:map b y} can-map b e -> can-map _ (D2 a x d b y e)) <- can-map _ D3 <- can-flay _ Dflay. - : can-tmap _ tmap/t. - : can-tmap _ (tmap/sing D) <- can-map _ D. - : can-tmap _ (tmap/pi D2 D1) <- can-tmap _ D1 <- ({a} {x} {xt} can-map x xt -> can-tmap _ (D2 x a xt)). - : can-tmap _ (tmap/sigma D2 D1) <- can-tmap _ D1 <- ({a} {x} {xt} can-map x xt -> can-tmap _ (D2 x a xt)). - : can-tmap _ tmap/one. %worlds (evar | can-map-bind | map-bind-for-can-map | invert-bind-for-can-map) (can-map _ _) (can-tmap _ _). %total (D1 D2) (can-map D1 _) (can-tmap D2 _). %%%%% Map functionality %%%%% map-fun : map C M -> map C M' -> eterm-eq M M' -> type. %mode map-fun +X1 +X2 -X3. tmap-fun : tmap K A -> tmap K A' -> etp-eq A A' -> type. %mode tmap-fun +X1 +X2 -X3. %block map-fun-bind : some {x:eterm} block {a:con} {at:map a x}. %block map-bind-for-map-fun : some {b:etp} {k:kind} block {x:eterm} {d:evof x b} {a:con} {e:cn-of a k} {at:map a x}. %block invert-bind-for-map-fun : some {K:kind} {B:etp} {DwfK:kd-wf K} block {a:con} {da:cn-of a K} {das:cn-assm da} {_:mcn-assm da das} {_:cn-of-reg da DwfK} {x:eterm} {dx:evof x B} {at:map a x}. - : map-fun D D eterm-eq/i. - : map-fun (map/app D2 D1) (map/app D2' D1') Deq <- map-fun D1 D1' Deq1 <- map-fun D2 D2' Deq2 <- eterm-resp-eterm2 eapp Deq1 Deq2 Deq. - : map-fun (map/pi1 D) (map/pi1 D') Deq <- map-fun D D' Deq1 <- eterm-resp-eterm epi1 Deq1 Deq. - : map-fun (map/pi2 D) (map/pi2 D') Deq <- map-fun D D' Deq1 <- eterm-resp-eterm epi2 Deq1 Deq. - : map-fun (map/lam D2 D1) (map/lam D2' D1') Deq <- tmap-fun D1 D1' Deq1 <- ({x} {a} {d:map a x} map-fun (D2 a x d) (D2' a x d) (Deq2 x)) <- elam-resp Deq1 Deq2 Deq. - : map-fun (map/pair D2 D1) (map/pair D2' D1') Deq <- map-fun D1 D1' Deq1 <- map-fun D2 D2' Deq2 <- eterm-resp-eterm2 epair Deq1 Deq2 Deq. - : map-fun (map/ref D) (map/ref D') Deq <- map-fun D D' Deq1 <- eterm-resp-eterm ([m] eapp (econst const/ref) m) Deq1 Deq. - : map-fun (map/tag D) (map/tag D') Deq <- map-fun D D' Deq1 <- eterm-resp-eterm ([m] eapp (econst const/tag) m) Deq1 Deq. - : map-fun (map/labeled D) (map/labeled D') Deq <- map-fun D D' Deq1 <- eterm-resp-eterm ([m] eapp (econst (const/labeled I)) m) Deq1 Deq. - : map-fun (map/arrow D2 D1) (map/arrow D2' D1') Deq <- map-fun D1 D1' Deq1 <- map-fun D2 D2' Deq2 <- eterm-resp-eterm2 ([m] [n] eapp (eapp (econst const/arrow) m) n) Deq1 Deq2 Deq. - : map-fun (map/prod D2 D1) (map/prod D2' D1') Deq <- map-fun D1 D1' Deq1 <- map-fun D2 D2' Deq2 <- eterm-resp-eterm2 ([m] [n] eapp (eapp (econst const/prod) m) n) Deq1 Deq2 Deq. - : map-fun (map/plus D2 D1) (map/plus D2' D1') Deq <- map-fun D1 D1' Deq1 <- map-fun D2 D2' Deq2 <- eterm-resp-eterm2 ([m] [n] eapp (eapp (econst const/plus) m) n) Deq1 Deq2 Deq. map-fun-rec : skel-eq As As' -> eterm-eq M M' -> etp-eq A A' -> ({x} {y} eterm-eq (M1 x y) (M1' x y)) -> eterm-eq M2 M2' -> eterm-eq (eapp (econst (const/rec As)) (epair M (epair (elam (epi A ([_] et)) ([x] elam A ([y] M1 x y))) M2))) (eapp (econst (const/rec As')) (epair M' (epair (elam (epi A' ([_] et)) ([x] elam A' ([y] M1' x y))) M2'))) -> type. %mode map-fun-rec +X1 +X2 +X3 +X4 +X5 -X6. - : map-fun-rec _ _ _ _ _ eterm-eq/i. %worlds (evar) (map-fun-rec _ _ _ _ _ _). %total {} (map-fun-rec _ _ _ _ _ _). - : map-fun (map/rec Dflay Dmap2 Dmap1 Dtmap) (map/rec Dflay' Dmap2' Dmap1' Dtmap') Deq <- tmap-fun Dtmap Dtmap' DeqA <- ({x} {a} {da:map a x} {y} {b} {db:map b y} map-fun (Dmap1 a x da b y db) (Dmap1' a x da b y db) (DeqM1 x y)) <- map-fun Dmap2 Dmap2' DeqM2 <- flay-resp DeqA skel-eq/i eterm-eq/i Dflay Dflay'' <- flay-fun Dflay'' Dflay' DeqSK DeqMA <- map-fun-rec DeqSK DeqMA DeqA DeqM1 DeqM2 Deq. - : tmap-fun tmap/t tmap/t etp-eq/i. - : tmap-fun (tmap/sing D) (tmap/sing D') Deq <- map-fun D D' Deq1 <- etp-resp-eterm esing Deq1 Deq. - : tmap-fun (tmap/pi D2 D1) (tmap/pi D2' D1') Deq <- tmap-fun D1 D1' Deq1 <- ({a} {x} {xt} tmap-fun (D2 x a xt) (D2' x a xt) (Deq2 a)) <- etp-resp-bind epi Deq1 Deq2 Deq. - : tmap-fun (tmap/sigma D2 D1) (tmap/sigma D2' D1') Deq <- tmap-fun D1 D1' Deq1 <- ({a} {x} {xt} tmap-fun (D2 x a xt) (D2' x a xt) (Deq2 a)) <- etp-resp-bind esigma Deq1 Deq2 Deq. - : tmap-fun tmap/one tmap/one etp-eq/i. %worlds (evar | map-fun-bind | map-bind-for-map-fun | invert-bind-for-map-fun) (map-fun _ _ _) (tmap-fun _ _ _). %total (D1 D2) (map-fun _ D1 _) (tmap-fun _ D2 _). %%%%% Map preserves typing %%%%% map-of : cn-of C K -> map C M %% -> tmap K A -> eof M A -> type. %mode map-of +X1 +X2 -X3 -X4. map-of' : cn-of C K -> map C M -> tmap K A %% -> eof M A -> type. %mode map-of' +X1 +X2 +X3 -X4. map-wf : kd-wf K %% -> tmap K A -> ewf A -> type. %mode map-wf +X1 -X2 -X3. map-wf' : kd-wf K -> tmap K A %% -> ewf A -> type. %mode map-wf' +X1 +X2 -X3. map-subtp : kd-sub K L -> tmap K A -> tmap L B %% -> subtp A B -> type. %mode map-subtp +X1 +X2 +X3 -X4. map-tequiv : kd-equiv K L -> tmap K A -> tmap L B %% -> tequiv A B -> type. %mode map-tequiv +X1 +X2 +X3 -X4. map-equiv' : map C M -> map D N -> cn-equiv C D K %% -> tmap K A -> equiv M N A -> type. %mode map-equiv' +X1 +X2 +X3 -X4 -X5. map-equiv'' : map C M -> map D N -> cn-equiv C D K -> tmap K A %% -> equiv M N A -> type. %mode map-equiv'' +X1 +X2 +X3 +X4 -X5. %block map-bind : some {B:etp} {K:kind} {Dmap:tmap K B} {Dwf:ewf B} block {x:eterm} {dx:evof x B} {a:con} {da:cn-of a K} {at:map a x} {thm:can-map a at} {thm:map-of da at Dmap (eof/var Dwf dx)}. %block invert-bind-for-map-of : some {K:kind} {K':kind} {B:etp} {DmapK:tmap K B} {DmapB:tunmap B K'} {DwfK:kd-wf K} {DwfB:ewf B} {DequivK:kd-equiv K K'} block {a:con} {da:cn-of a K} {das:cn-assm da} {_:mcn-assm da das} {_:cn-of-reg da DwfK} {x:eterm} {dx:evof x B} {at:map a x} {xt:unmap x a} {_:can-map a at} {_:map-of da at DmapK (eof/var DwfB dx)}. - : map-of (cn-of/app Dof2 Dof1) (map/app Dmap2 Dmap1) (DmapB _ _ Dmap2) (eof/app Dof2' Dof1') <- map-of Dof1 Dmap1 (tmap/pi DmapB DmapA) Dof1' <- map-of' Dof2 Dmap2 DmapA Dof2'. - : map-of (cn-of/pi1 Dof) (map/pi1 Dmap) DmapA (eof/pi1 Dof') <- map-of Dof Dmap (tmap/sigma DmapB DmapA) Dof'. - : map-of (cn-of/pi2 Dof) (map/pi2 Dmap) (DmapB _ _ (map/pi1 Dmap)) (eof/pi2 Dof') <- map-of Dof Dmap (tmap/sigma DmapB DmapA) Dof'. - : map-of (cn-of/lam Dof Dwf) (map/lam Dmap DmapA) (tmap/pi DmapB DmapA) (eof/lam Dof' Dwf') <- map-wf' Dwf DmapA Dwf' <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at DmapA (eof/var Dwf' d) -> map-of (Dof a e) (Dmap a x at) (DmapB a x at) (Dof' x d)). - : map-of (cn-of/pair Dwf2 Dof2 Dof1) (map/pair Dmap2 Dmap1) (tmap/sigma DmapB DmapA) (eof/pair Dwf2' Dof2' Dof1') <- map-of Dof1 Dmap1 DmapA Dof1' <- eof-reg Dof1' Dwf1' <- ({x} {d:evof x A} {a} {e:cn-of a K} {at:map a x} can-map a at -> map-of e at DmapA (eof/var Dwf1' d) -> map-wf (Dwf2 a e) (DmapB a x at) (Dwf2' x d)) <- map-of' Dof2 Dmap2 (DmapB _ _ Dmap1) Dof2'. - : map-of cn-of/star map/star tmap/one eof/star. - : map-of (cn-of/sing Dof) Dmap (tmap/sing Dmap) (eof/sing Dof') <- map-of' Dof Dmap tmap/t Dof'. - : map-of (cn-of/extsigma Dwf2 Dof2 Dof1) Dmap (tmap/sigma DmapB DmapA) (eof/extsigma Dwf2' Dof2' Dof1') <- map-of Dof1 (map/pi1 Dmap) DmapA Dof1' <- eof-reg Dof1' Dwf1' <- ({x} {d:evof x A} {a} {e:cn-of a K} {at:map a x} can-map a at -> map-of e at DmapA (eof/var Dwf1' d) -> map-wf (Dwf2 a e) (DmapB a x at) (Dwf2' x d)) <- map-of' Dof2 (map/pi2 Dmap) (DmapB _ _ (map/pi1 Dmap)) Dof2'. - : map-of (cn-of/extpi Dof DofPre) Dmap (tmap/pi DmapB DmapA) (eof/extpi Dof' DofPre') <- map-of DofPre Dmap (tmap/pi _ DmapA) DofPre' <- eof-reg DofPre' (ewf/pi _ Dwf') <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at DmapA (eof/var Dwf' d) -> map-of (Dof a e) (map/app at Dmap) (DmapB a x at) (Dof' x d)). - : map-of (cn-of/subsume Dsub Dof) Dmap DmapB (eof/subsume Dsub' Dof') <- map-of Dof Dmap DmapA Dof' <- can-tmap _ DmapB <- map-subtp Dsub DmapA DmapB Dsub'. - : map-of cn-of/unit map/unit tmap/t (eof/const ewf/t (ekof/i etopen/t ckof/unit)). - : map-of cn-of/void map/void tmap/t (eof/const ewf/t (ekof/i etopen/t ckof/void)). - : map-of cn-of/tagged map/tagged tmap/t (eof/const ewf/t (ekof/i etopen/t ckof/tagged)). - : map-of (cn-of/ref Dof) (map/ref Dmap) tmap/t (eof/app Dof' (eof/const (ewf/pi ([_] [_] ewf/t) ewf/t) (ekof/i (etopen/arrow etopen/t etp-skel/t etopen/t) ckof/ref))) <- map-of' Dof Dmap tmap/t Dof'. - : map-of (cn-of/tag Dof) (map/tag Dmap) tmap/t (eof/app Dof' (eof/const (ewf/pi ([_] [_] ewf/t) ewf/t) (ekof/i (etopen/arrow etopen/t etp-skel/t etopen/t) ckof/tag))) <- map-of' Dof Dmap tmap/t Dof'. - : map-of (cn-of/labeled Dof) (map/labeled Dmap) tmap/t (eof/app Dof' (eof/const (ewf/pi ([_] [_] ewf/t) ewf/t) (ekof/i (etopen/arrow etopen/t etp-skel/t etopen/t) ckof/labeled))) <- map-of' Dof Dmap tmap/t Dof'. - : map-of (cn-of/arrow Dof2 Dof1) (map/arrow Dmap2 Dmap1) tmap/t (eof/app Dof2' (eof/app Dof1' (eof/const (ewf/pi ([_] [_] ewf/pi ([_] [_] ewf/t) ewf/t) ewf/t) (ekof/i (etopen/arrow (etopen/arrow etopen/t etp-skel/t etopen/t) etp-skel/t etopen/t) ckof/arrow)))) <- map-of' Dof1 Dmap1 tmap/t Dof1' <- map-of' Dof2 Dmap2 tmap/t Dof2'. - : map-of (cn-of/prod Dof2 Dof1) (map/prod Dmap2 Dmap1) tmap/t (eof/app Dof2' (eof/app Dof1' (eof/const (ewf/pi ([_] [_] ewf/pi ([_] [_] ewf/t) ewf/t) ewf/t) (ekof/i (etopen/arrow (etopen/arrow etopen/t etp-skel/t etopen/t) etp-skel/t etopen/t) ckof/prod)))) <- map-of' Dof1 Dmap1 tmap/t Dof1' <- map-of' Dof2 Dmap2 tmap/t Dof2'. - : map-of (cn-of/plus Dof2 Dof1) (map/plus Dmap2 Dmap1) tmap/t (eof/app Dof2' (eof/app Dof1' (eof/const (ewf/pi ([_] [_] ewf/pi ([_] [_] ewf/t) ewf/t) ewf/t) (ekof/i (etopen/arrow (etopen/arrow etopen/t etp-skel/t etopen/t) etp-skel/t etopen/t) ckof/plus)))) <- map-of' Dof1 Dmap1 tmap/t Dof1' <- map-of' Dof2 Dmap2 tmap/t Dof2'. - : map-of (cn-of/rec DofC2 DofC1 DwfK) (map/rec Dflay DmapC2 DmapC1 (DmapK : tmap K A)) tmap/t (eof/app (eof/pair ([z] [dz] ewf/sigma ([_] [_] DwfA' z dz) (ewf/pi ([_] [_] ewf/pi ([_] [_] ewf/t) (DwfA' z dz)) (ewf/pi ([_] [_] ewf/t) (DwfA' z dz)))) (eof/equiv (tequiv/sigma ([_] [_] Dtequiv) (tequiv/pi ([_] [_] tequiv/pi ([_] [_] tequiv/t) Dtequiv) (tequiv/pi ([_] [_] tequiv/t) Dtequiv))) (eof/pair ([_] [_] DwfA) DofM2 (eof/lam ([x] [dx] eof/lam ([y] [dy] DofM1 x dx y dy) DwfA) (ewf/pi ([_] [_] ewf/t) DwfA)))) DofMA) DeofConst) <- map-wf' DwfK DmapK (DwfA : ewf A) <- ({x} {dx} {a} {da} {at} can-map a at -> map-of da at (tmap/pi ([_] [_] [_] tmap/t) DmapK) (eof/var (ewf/pi ([_] [_] ewf/t) DwfA) dx) -> {y} {dy} {b} {db} {bt} can-map b bt -> map-of db bt DmapK (eof/var DwfA dy) -> map-of' (DofC1 a da b db) (DmapC1 a x at b y bt) tmap/t (DofM1 x dx y dy)) <- map-of' DofC2 DmapC2 DmapK (DofM2 : eof M2 A) <- can-skof _ Dskof <- flay-sound DwfA Dflay Dskof DofMA Dtequiv <- skof-reg Dskof DwfD DwfA' <- skof-implies-eof-rec Dskof DeofConst. %%% - : map-of' Dof Dmap DmapA Dof'' <- map-of Dof Dmap DmapA' Dof' <- tmap-fun DmapA' DmapA Deq <- eof-resp eterm-eq/i Deq Dof' Dof''. %%% - : map-wf kd-wf/t tmap/t ewf/t. - : map-wf (kd-wf/sing Dof) (tmap/sing Dmap) (ewf/sing Dof') <- can-map _ Dmap <- map-of' Dof Dmap tmap/t Dof'. - : map-wf (kd-wf/pi Dwf2 Dwf1) (tmap/pi Dmap2 Dmap1) (ewf/pi Dwf2' Dwf1') <- map-wf Dwf1 Dmap1 Dwf1' <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at Dmap1 (eof/var Dwf1' d) -> map-wf (Dwf2 a e) (Dmap2 a x at) (Dwf2' x d)). - : map-wf (kd-wf/sigma Dwf2 Dwf1) (tmap/sigma Dmap2 Dmap1) (ewf/sigma Dwf2' Dwf1') <- map-wf Dwf1 Dmap1 Dwf1' <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at Dmap1 (eof/var Dwf1' d) -> map-wf (Dwf2 a e) (Dmap2 a x at) (Dwf2' x d)). - : map-wf kd-wf/one tmap/one ewf/one. %%% - : map-wf' Dwf Dmap Dwf'' <- map-wf Dwf Dmap' Dwf' <- tmap-fun Dmap' Dmap Deq <- ewf-resp Deq Dwf' Dwf''. %%% - : map-subtp (kd-sub/refl Dequiv) DmapA DmapB (subtp/reflex Dequiv') <- map-tequiv Dequiv DmapA DmapB Dequiv'. - : map-subtp (kd-sub/trans DsubBC DsubAB) DmapA DmapC (subtp/trans DsubBC' DsubAB') <- can-tmap _ DmapB <- map-subtp DsubAB DmapA DmapB DsubAB' <- map-subtp DsubBC DmapB DmapC DsubBC'. - : map-subtp (kd-sub/sing-t Dof) (tmap/sing Dmap) tmap/t (subtp/sing_t Dof') <- map-of' Dof Dmap tmap/t Dof'. - : map-subtp (kd-sub/sigma Dwf2 Dsub2 Dsub1) (tmap/sigma Dmap2 Dmap1) (tmap/sigma Dmap2' Dmap1') (subtp/sigma Dwf2' Dsub2' Dsub1') <- map-subtp Dsub1 Dmap1 Dmap1' Dsub1' <- subtp-reg Dsub1' Dwf1 Dwf1' <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at Dmap1 (eof/var Dwf1 d) -> map-subtp (Dsub2 a e) (Dmap2 a x at) (Dmap2' a x at) (Dsub2' x d)) <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at Dmap1' (eof/var Dwf1' d) -> map-wf' (Dwf2 a e) (Dmap2' a x at) (Dwf2' x d)). - : map-subtp (kd-sub/pi Dwf2 Dsub2 Dsub1) (tmap/pi Dmap2 Dmap1) (tmap/pi Dmap2' Dmap1') (subtp/pi Dwf2' Dsub2' Dsub1') <- map-subtp Dsub1 Dmap1' Dmap1 Dsub1' <- subtp-reg Dsub1' Dwf1' Dwf1 <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at Dmap1' (eof/var Dwf1' d) -> map-subtp (Dsub2 a e) (Dmap2 a x at) (Dmap2' a x at) (Dsub2' x d)) <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at Dmap1 (eof/var Dwf1 d) -> map-wf' (Dwf2 a e) (Dmap2 a x at) (Dwf2' x d)). %%% - : map-tequiv (kd-equiv/refl Dwf) Dmap Dmap' Dequiv' <- map-wf' Dwf Dmap Dwf' <- tmap-fun Dmap Dmap' Deq <- tequiv-resp etp-eq/i Deq (tequiv/reflex Dwf') Dequiv'. - : map-tequiv (kd-equiv/symm Dequiv) Dmap Dmap' (tequiv/symm Dequiv') <- map-tequiv Dequiv Dmap' Dmap Dequiv'. - : map-tequiv (kd-equiv/trans DequivBC DequivAB) DmapA DmapC (tequiv/trans DequivBC' DequivAB') <- can-tmap _ DmapB <- map-tequiv DequivAB DmapA DmapB DequivAB' <- map-tequiv DequivBC DmapB DmapC DequivBC'. - : map-tequiv (kd-equiv/sing Dequiv) (tmap/sing Dmap) (tmap/sing Dmap') (tequiv/sing Dequiv') <- map-equiv'' Dmap Dmap' Dequiv tmap/t Dequiv'. - : map-tequiv (kd-equiv/sigma Dequiv2 Dequiv1) (tmap/sigma Dmap2 Dmap1) (tmap/sigma Dmap2' Dmap1') (tequiv/sigma Dequiv2' Dequiv1') <- map-tequiv Dequiv1 Dmap1 Dmap1' Dequiv1' <- tequiv-reg Dequiv1' Dwf1' _ <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at Dmap1 (eof/var Dwf1' d) -> map-tequiv (Dequiv2 a e) (Dmap2 a x at) (Dmap2' a x at) (Dequiv2' x d)). - : map-tequiv (kd-equiv/pi Dequiv2 Dequiv1) (tmap/pi Dmap2 Dmap1) (tmap/pi Dmap2' Dmap1') (tequiv/pi Dequiv2' Dequiv1') <- map-tequiv Dequiv1 Dmap1 Dmap1' Dequiv1' <- tequiv-reg Dequiv1' Dwf1' _ <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at Dmap1 (eof/var Dwf1' d) -> map-tequiv (Dequiv2 a e) (Dmap2 a x at) (Dmap2' a x at) (Dequiv2' x d)). %%% - : map-equiv' Dmap Dmap' (cn-equiv/refl Dof) DmapA Dequiv' <- map-fun Dmap Dmap' Deq <- map-of Dof Dmap DmapA Dof' <- equiv-resp eterm-eq/i Deq etp-eq/i (equiv/reflex Dof') Dequiv'. - : map-equiv' Dmap Dmap' (cn-equiv/symm Dequiv) DmapA (equiv/symm Dequiv') <- map-equiv' Dmap' Dmap Dequiv DmapA Dequiv'. - : map-equiv' Dmap1 Dmap3 (cn-equiv/trans D23 D12) DmapA (equiv/trans D23' D12') <- can-map _ Dmap2 <- map-equiv' Dmap1 Dmap2 D12 DmapA D12' <- map-equiv'' Dmap2 Dmap3 D23 DmapA D23'. - : map-equiv' (map/app Dmap2 Dmap1) (map/app Dmap2' Dmap1') (cn-equiv/app Dequiv2 Dequiv1) (DmapB _ _ Dmap2) (equiv/app Dequiv2' Dequiv1') <- map-equiv' Dmap1 Dmap1' Dequiv1 (tmap/pi DmapB DmapA) Dequiv1' <- map-equiv'' Dmap2 Dmap2' Dequiv2 DmapA Dequiv2'. - : map-equiv' (map/pi1 Dmap) (map/pi1 Dmap') (cn-equiv/pi1 Dequiv) DmapA (equiv/pi1 Dequiv') <- map-equiv' Dmap Dmap' Dequiv (tmap/sigma DmapB DmapA) Dequiv'. - : map-equiv' (map/pi2 Dmap) (map/pi2 Dmap') (cn-equiv/pi2 Dequiv) (DmapB _ _ (map/pi1 Dmap)) (equiv/pi2 Dequiv') <- map-equiv' Dmap Dmap' Dequiv (tmap/sigma DmapB DmapA) Dequiv'. - : map-equiv' (map/lam Dmap DmapA) (map/lam Dmap' DmapA') (cn-equiv/lam Dequiv2 Dequiv1) (tmap/pi DmapB DmapA) (equiv/lam Dequiv2' Dequiv1') <- map-tequiv Dequiv1 DmapA DmapA' Dequiv1' <- tequiv-reg Dequiv1' Dwf' _ <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at DmapA (eof/var Dwf' d) -> map-equiv' (Dmap a x at) (Dmap' a x at) (Dequiv2 a e) (DmapB a x at) (Dequiv2' x d)). - : map-equiv' (map/pair Dmap2 Dmap1) (map/pair Dmap2' Dmap1') (cn-equiv/pair Dwf2 Dequiv2 Dequiv1) (tmap/sigma DmapB DmapA) (equiv/pair Dwf2' Dequiv2' Dequiv1') <- map-equiv' Dmap1 Dmap1' Dequiv1 DmapA Dequiv1' <- equiv-reg Dequiv1' _ _ Dwf1' <- ({x} {d:evof x A} {a} {e:cn-of a K} {at:map a x} can-map a at -> map-of e at DmapA (eof/var Dwf1' d) -> map-wf (Dwf2 a e) (DmapB a x at) (Dwf2' x d)) <- map-equiv'' Dmap2 Dmap2' Dequiv2 (DmapB _ _ Dmap1) Dequiv2'. - : map-equiv' Dmap1 Dmap2 (cn-equiv/sing Dequiv) (tmap/sing Dmap1) (equiv/sing Dequiv') <- map-equiv'' Dmap1 Dmap2 Dequiv tmap/t Dequiv'. - : map-equiv' Dmap1 Dmap2 (cn-equiv/singelim Dof) tmap/t (equiv/singelim Dof') <- map-of' Dof Dmap1 (tmap/sing Dmap2) Dof'. - : map-equiv' Dmap Dmap' (cn-equiv/extsigma Dwf2 Dequiv2 Dequiv1) (tmap/sigma DmapB DmapA) (equiv/extsigma Dwf2' Dequiv2' Dequiv1') <- map-equiv' (map/pi1 Dmap) (map/pi1 Dmap') Dequiv1 DmapA Dequiv1' <- equiv-reg Dequiv1' _ _ Dwf1' <- ({x} {d:evof x A} {a} {e:cn-of a K} {at:map a x} can-map a at -> map-of e at DmapA (eof/var Dwf1' d) -> map-wf (Dwf2 a e) (DmapB a x at) (Dwf2' x d)) <- map-equiv'' (map/pi2 Dmap) (map/pi2 Dmap') Dequiv2 (DmapB _ _ (map/pi1 Dmap)) Dequiv2'. - : map-equiv' Dmap Dmap' (cn-equiv/extpi Dequiv DofPre2 DofPre1) (tmap/pi DmapB DmapA) (equiv/extpi Dequiv' DofPre2' DofPre1') <- map-of DofPre1 Dmap (tmap/pi _ DmapA) DofPre1' <- ({x} {a} {at} can-map a at -> can-tmap _ (DmapB2 a x at)) <- map-of' DofPre2 Dmap' (tmap/pi DmapB2 DmapA) DofPre2' <- eof-reg DofPre1' (ewf/pi _ Dwf') <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at DmapA (eof/var Dwf' d) -> map-equiv' (map/app at Dmap) (map/app at Dmap') (Dequiv a e) (DmapB a x at) (Dequiv' x d)). - : map-equiv' Dmap Dmap' (cn-equiv/extpiw Dequiv DequivPre) (tmap/pi DmapB DmapA) (equiv/extpiw Dequiv' DequivPre') <- map-equiv' Dmap Dmap' DequivPre (tmap/pi _ DmapA) DequivPre' <- equiv-reg DequivPre' _ _ (ewf/pi _ Dwf') <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at DmapA (eof/var Dwf' d) -> map-equiv' (map/app at Dmap) (map/app at Dmap') (Dequiv a e) (DmapB a x at) (Dequiv' x d)). - : map-equiv' Dmap1 Dmap2 (cn-equiv/one Dof2 Dof1) tmap/one (equiv/one Dof2' Dof1') <- map-of' Dof1 Dmap1 tmap/one Dof1' <- map-of' Dof2 Dmap2 tmap/one Dof2'. - : map-equiv' Dmap Dmap' (cn-equiv/subsume Dsub Dequiv) DmapB (equiv/subsume Dsub' Dequiv') <- map-equiv' Dmap Dmap' Dequiv DmapA Dequiv' <- can-tmap _ DmapB <- map-subtp Dsub DmapA DmapB Dsub'. - : map-equiv' (map/app DmapN (map/lam DmapM DmapA)) DmapMN (cn-equiv/beta DofN DofM) (DmapB _ _ DmapN) Dequiv' <- map-of' DofN DmapN DmapA DofN' <- eof-reg DofN' DwfA <- ({x} {d} {a} {e} {at} can-map a at -> map-of e at DmapA (eof/var DwfA d) -> map-of (DofM a e) (DmapM a x at) (DmapB a x at) (DofM' x d)) <- map-fun (DmapM _ _ DmapN) DmapMN Deq <- equiv-resp eterm-eq/i Deq etp-eq/i (equiv/beta DofN' DofM') Dequiv'. - : map-equiv' (map/pi1 (map/pair Dmap2 Dmap1)) Dmap1' (cn-equiv/beta1 Dof2 Dof1) DwfA Dequiv' <- map-of Dof1 Dmap1 DwfA Dof1' <- map-of Dof2 Dmap2 DwfB Dof2' <- map-fun Dmap1 Dmap1' Deq <- equiv-resp eterm-eq/i Deq etp-eq/i (equiv/beta1 Dof2' Dof1') Dequiv'. - : map-equiv' (map/pi2 (map/pair Dmap2 Dmap1)) Dmap2' (cn-equiv/beta2 Dof2 Dof1) DwfB Dequiv' <- map-of Dof1 Dmap1 DwfA Dof1' <- map-of Dof2 Dmap2 DwfB Dof2' <- map-fun Dmap2 Dmap2' Deq <- equiv-resp eterm-eq/i Deq etp-eq/i (equiv/beta2 Dof2' Dof1') Dequiv'. - : map-equiv' map/unit map/unit cn-equiv/unit tmap/t (equiv/reflex (eof/const ewf/t (ekof/i etopen/t ckof/unit))). - : map-equiv' map/void map/void cn-equiv/void tmap/t (equiv/reflex (eof/const ewf/t (ekof/i etopen/t ckof/void))). - : map-equiv' map/tagged map/tagged cn-equiv/tagged tmap/t (equiv/reflex (eof/const ewf/t (ekof/i etopen/t ckof/tagged))). - : map-equiv' (map/ref Dmap) (map/ref Dmap') (cn-equiv/ref Dequiv) tmap/t (equiv/app Dequiv' (equiv/reflex (eof/const (ewf/pi ([_] [_] ewf/t) ewf/t) (ekof/i (etopen/arrow etopen/t etp-skel/t etopen/t) ckof/ref)))) <- map-equiv'' Dmap Dmap' Dequiv tmap/t Dequiv'. - : map-equiv' (map/tag Dmap) (map/tag Dmap') (cn-equiv/tag Dequiv) tmap/t (equiv/app Dequiv' (equiv/reflex (eof/const (ewf/pi ([_] [_] ewf/t) ewf/t) (ekof/i (etopen/arrow etopen/t etp-skel/t etopen/t) ckof/tag)))) <- map-equiv'' Dmap Dmap' Dequiv tmap/t Dequiv'. - : map-equiv' (map/labeled Dmap) (map/labeled Dmap') (cn-equiv/labeled Dequiv) tmap/t (equiv/app Dequiv' (equiv/reflex (eof/const (ewf/pi ([_] [_] ewf/t) ewf/t) (ekof/i (etopen/arrow etopen/t etp-skel/t etopen/t) ckof/labeled)))) <- map-equiv'' Dmap Dmap' Dequiv tmap/t Dequiv'. - : map-equiv' (map/arrow Dmap2 Dmap1) (map/arrow Dmap2' Dmap1') (cn-equiv/arrow Dequiv2 Dequiv1) tmap/t (equiv/app Dequiv2' (equiv/app Dequiv1' (equiv/reflex (eof/const (ewf/pi ([_] [_] ewf/pi ([_] [_] ewf/t) ewf/t) ewf/t) (ekof/i (etopen/arrow (etopen/arrow etopen/t etp-skel/t etopen/t) etp-skel/t etopen/t) ckof/arrow))))) <- map-equiv'' Dmap1 Dmap1' Dequiv1 tmap/t Dequiv1' <- map-equiv'' Dmap2 Dmap2' Dequiv2 tmap/t Dequiv2'. - : map-equiv' (map/prod Dmap2 Dmap1) (map/prod Dmap2' Dmap1') (cn-equiv/prod Dequiv2 Dequiv1) tmap/t (equiv/app Dequiv2' (equiv/app Dequiv1' (equiv/reflex (eof/const (ewf/pi ([_] [_] ewf/pi ([_] [_] ewf/t) ewf/t) ewf/t) (ekof/i (etopen/arrow (etopen/arrow etopen/t etp-skel/t etopen/t) etp-skel/t etopen/t) ckof/prod))))) <- map-equiv'' Dmap1 Dmap1' Dequiv1 tmap/t Dequiv1' <- map-equiv'' Dmap2 Dmap2' Dequiv2 tmap/t Dequiv2'. - : map-equiv' (map/plus Dmap2 Dmap1) (map/plus Dmap2' Dmap1') (cn-equiv/plus Dequiv2 Dequiv1) tmap/t (equiv/app Dequiv2' (equiv/app Dequiv1' (equiv/reflex (eof/const (ewf/pi ([_] [_] ewf/pi ([_] [_] ewf/t) ewf/t) ewf/t) (ekof/i (etopen/arrow (etopen/arrow etopen/t etp-skel/t etopen/t) etp-skel/t etopen/t) ckof/plus))))) <- map-equiv'' Dmap1 Dmap1' Dequiv1 tmap/t Dequiv1' <- map-equiv'' Dmap2 Dmap2' Dequiv2 tmap/t Dequiv2'. - : map-equiv' (map/rec Dflay DmapC2 DmapC1 DmapK) (map/rec Dflay' DmapC2' DmapC1' DmapK') (cn-equiv/rec DequivC2 DequivC1 DequivK) %% tmap/t (equiv/app (equiv/pair ([z] [dz] ewf/sigma ([_] [_] DwfA' z dz) (ewf/pi ([_] [_] ewf/pi ([_] [_] ewf/t) (DwfA' z dz)) (ewf/pi ([_] [_] ewf/t) (DwfA' z dz)))) (equiv/equiv (tequiv/sigma ([_] [_] Dtequiv) (tequiv/pi ([_] [_] tequiv/pi ([_] [_] tequiv/t) Dtequiv) (tequiv/pi ([_] [_] tequiv/t) Dtequiv))) (equiv/pair ([_] [_] DwfA) DequivM2 (equiv/lam ([x] [d] equiv/lam ([y] [e] DequivM1 x d y e) DequivA) (tequiv/pi ([_] [_] tequiv/t) DequivA)))) DequivMA) DequivConst) <- map-tequiv DequivK DmapK DmapK' DequivA <- tequiv-reg DequivA DwfA _ <- ({x} {dx:evof x (epi A ([_] et))} {a} {da:cn-of a (pi K ([_] t))} {at:map a x} can-map a at -> map-of da at (tmap/pi ([_] [_] [_] tmap/t) DmapK) (eof/var (ewf/pi ([_] [_] ewf/t) DwfA) dx) -> {y} {dy:evof y A} {b} {db:cn-of b K} {bt:map b y} can-map b bt -> map-of db bt DmapK (eof/var DwfA dy) -> map-equiv'' (DmapC1 a x at b y bt) (DmapC1' a x at b y bt) (DequivC1 a da b db) tmap/t (DequivM1 x dx y dy)) <- map-equiv'' DmapC2 DmapC2' DequivC2 DmapK DequivM2 <- can-skof _ Dskof <- flay-sound DwfA Dflay Dskof DofMA Dtequiv <- flay-equiv DequivA Dflay Dflay' Dskof DeqSK DequivMA <- skof-implies-eof-rec Dskof DeofConst <- eterm-resp-skel ([sk] econst (const/rec sk)) DeqSK DeqConst <- equiv-resp eterm-eq/i DeqConst etp-eq/i (equiv/reflex DeofConst) DequivConst <- skof-reg Dskof DwfD DwfA'. %%% - : map-equiv'' Dmap Dmap' Dequiv DmapA Dequiv'' <- map-equiv' Dmap Dmap' Dequiv DmapA' Dequiv' <- tmap-fun DmapA' DmapA Deq <- equiv-resp eterm-eq/i eterm-eq/i Deq Dequiv' Dequiv''. %worlds (map-bind | invert-bind-for-map-of) (map-of _ _ _ _) (map-of' _ _ _ _) (map-wf _ _ _) (map-wf' _ _ _) (map-subtp _ _ _ _) (map-tequiv _ _ _ _) (map-equiv' _ _ _ _ _) (map-equiv'' _ _ _ _ _). %total (D1 D2 D3 D4 D5 D6 D7 D8) (map-of D1 _ _ _) (map-of' D2 _ _ _) (map-wf D3 _ _) (map-wf' D4 _ _) (map-subtp D5 _ _ _) (map-tequiv D6 _ _ _) (map-equiv' _ _ D7 _ _) (map-equiv'' _ _ D8 _ _). map-equiv : cn-equiv C D K %% -> map C M -> map D N -> tmap K A -> equiv M N A -> type. %mode map-equiv +X1 -X2 -X3 -X4 -X5. - : map-equiv Dequiv Dmap1 Dmap2 DmapA Dequiv' <- can-map _ Dmap1 <- can-map _ Dmap2 <- map-equiv' Dmap1 Dmap2 Dequiv DmapA Dequiv'. %worlds (map-bind) (map-equiv _ _ _ _ _). %total {} (map-equiv _ _ _ _ _). %% strange modes to overcome some output freeness issues in consistency map-equiv-i1 : cn-equiv C D K -> map C M %% -> map D N -> tmap K A -> equiv M N A -> type. %mode map-equiv-i1 +X1 +X2 -X3 -X4 -X5. - : map-equiv-i1 Dequiv Dmap1 Dmap2 DmapA Dequiv' <- can-map _ Dmap2 <- map-equiv' Dmap1 Dmap2 Dequiv DmapA Dequiv'. %worlds (map-bind) (map-equiv-i1 _ _ _ _ _). %total {} (map-equiv-i1 _ _ _ _ _). map-equiv-i2 : cn-equiv C D K -> map C M -> map D N -> tmap K A -> equiv M N A -> type. %mode map-equiv-i2 +X1 -X2 +X3 -X4 -X5. - : map-equiv-i2 Dequiv Dmap1 Dmap2 DmapA Dequiv' <- can-map _ Dmap1 <- map-equiv' Dmap1 Dmap2 Dequiv DmapA Dequiv'. %worlds (map-bind) (map-equiv-i2 _ _ _ _ _). %total {} (map-equiv-i2 _ _ _ _ _). %%%%% Unmap effectiveness %%%%% can-unmap : {M} unmap M C -> type. %mode can-unmap +X1 -X2. can-tunmap : {A} tunmap A K -> type. %mode can-tunmap +X1 -X2. %block can-unmap-bind : some {a:con} block {x:eterm} {xt:unmap x a} {thm:can-unmap x xt}. %block unmap-bind-for-can-unmap : some {k:kind} {b:etp} {d_map:tunmap b k} block {a:con} {d:cn-of a k} {x:eterm} {e:evof x b} {xt:unmap x a} {thm:can-unmap x xt}. - : can-unmap _ (unmap/app D2 D1) <- can-unmap _ D1 <- can-unmap _ D2. - : can-unmap _ (unmap/pi1 D) <- can-unmap _ D. - : can-unmap _ (unmap/pi2 D) <- can-unmap _ D. - : can-unmap _ (unmap/lam D2 D1) <- can-tunmap _ D1 <- ({a} {x} {xt} can-unmap x xt -> can-unmap _ (D2 x a xt)). - : can-unmap _ (unmap/pair D2 D1) <- can-unmap _ D1 <- can-unmap _ D2. - : can-unmap _ unmap/star. - : can-unmap _ unmap/ref. - : can-unmap _ unmap/tag. - : can-unmap _ unmap/labeled. - : can-unmap _ unmap/unit. - : can-unmap _ unmap/void. - : can-unmap _ unmap/tagged. - : can-unmap _ unmap/arrow. - : can-unmap _ unmap/prod. - : can-unmap _ unmap/plus. - : can-unmap _ (unmap/rec Dskof) <- can-skof-il _ Dskof. - : can-tunmap _ tunmap/t. - : can-tunmap _ (tunmap/sing D) <- can-unmap _ D. - : can-tunmap _ (tunmap/pi D2 D1) <- can-tunmap _ D1 <- ({a} {x} {xt} can-unmap x xt -> can-tunmap _ (D2 x a xt)). - : can-tunmap _ (tunmap/sigma D2 D1) <- can-tunmap _ D1 <- ({a} {x} {xt} can-unmap x xt -> can-tunmap _ (D2 x a xt)). - : can-tunmap _ tunmap/one. %worlds (conblock | can-unmap-bind | unmap-bind-for-can-unmap) (can-unmap _ _) (can-tunmap _ _). %total (D1 D2) (can-unmap D1 _) (can-tunmap D2 _). %%%%% Unmap functionality %%%%% unmap-fun : unmap M C -> unmap M C' -> con-eq C C' -> type. %mode unmap-fun +X1 +X2 -X3. tunmap-fun : tunmap A K -> tunmap A K' -> kind-eq K K' -> type. %mode tunmap-fun +X1 +X2 -X3. %block unmap-fun-bind : some {a:con} block {x:eterm} {xt:unmap x a}. %block unmap-bind-for-unmap-fun : some {k:kind} {b:etp} block {a:con} {d:cn-of a k} {x:eterm} {e:evof x b} {xt:unmap x a}. %block invert-bind-for-unmap-fun : some {K:kind} {B:etp} {DmapK:tmap K B} {DwfK:kd-wf K} block {a:con} {da:cn-of a K} {das:cn-assm da} {_:mcn-assm da das} {_:cn-of-reg da DwfK} {x:eterm} {dx:evof x B} {at:map a x} {xt:unmap x a}. - : unmap-fun D D con-eq/i. - : unmap-fun (unmap/app D2 D1) (unmap/app D2' D1') Deq <- unmap-fun D1 D1' Deq1 <- unmap-fun D2 D2' Deq2 <- con-resp-con2 app Deq1 Deq2 Deq. - : unmap-fun (unmap/pi1 D) (unmap/pi1 D') Deq <- unmap-fun D D' Deq1 <- con-resp-con pi1 Deq1 Deq. - : unmap-fun (unmap/pi2 D) (unmap/pi2 D') Deq <- unmap-fun D D' Deq1 <- con-resp-con pi2 Deq1 Deq. - : unmap-fun (unmap/lam D2 D1) (unmap/lam D2' D1') Deq <- tunmap-fun D1 D1' Deq1 <- ({a} {x} {xt} unmap-fun (D2 x a xt) (D2' x a xt) (Deq2 a)) <- lam-resp Deq1 Deq2 Deq. - : unmap-fun (unmap/pair D2 D1) (unmap/pair D2' D1') Deq <- unmap-fun D1 D1' Deq1 <- unmap-fun D2 D2' Deq2 <- con-resp-con2 pair Deq1 Deq2 Deq. - : unmap-fun (unmap/rec D) (unmap/rec D') Deq <- skof-il-fun D D' DeqA DeqB <- con-resp-kind2-bind ([K] [L] lam (sigma K ([a] kprod (karrow (karrow (L a) t) (karrow (L a) t)) (L a))) ([b] rec (L (pi1 b)) ([c] [d] app (app (pi1 (pi2 b)) c) d) (pi2 (pi2 b)))) DeqA DeqB Deq. - : tunmap-fun D D kind-eq/i. - : tunmap-fun (tunmap/sing D) (tunmap/sing D') Deq <- unmap-fun D D' Deq1 <- kind-resp-con sing Deq1 Deq. - : tunmap-fun (tunmap/pi D2 D1) (tunmap/pi D2' D1') Deq <- tunmap-fun D1 D1' Deq1 <- ({a} {x} {xt} tunmap-fun (D2 x a xt) (D2' x a xt) (Deq2 a)) <- pi-resp Deq1 Deq2 Deq. - : tunmap-fun (tunmap/sigma D2 D1) (tunmap/sigma D2' D1') Deq <- tunmap-fun D1 D1' Deq1 <- ({a} {x} {xt} tunmap-fun (D2 x a xt) (D2' x a xt) (Deq2 a)) <- sigma-resp Deq1 Deq2 Deq. %worlds (conblock | unmap-fun-bind | unmap-bind-for-unmap-fun | invert-bind-for-unmap-fun) (unmap-fun _ _ _) (tunmap-fun _ _ _). %total (D1 D2) (unmap-fun _ D1 _) (tunmap-fun _ D2 _). %%%%% Unmap preserves typing %%%%% unmap-expand : eexpand R A M -> unmap R C -> tunmap A K %% -> unmap M D -> expand-il C K D -> type. %mode unmap-expand +X1 +X2 +X3 -X4 -X5. - : unmap-expand eexpand/t D tunmap/t D expand-il/t. - : unmap-expand (eexpand/pi Dexp2 Dexp1) DmapR (tunmap/pi DmapB DmapA) (unmap/lam DmapM DmapA) (expand-il/pi Dexp2' Dexp1') <- ({a} {x} {xt:unmap x a} unmap-expand (Dexp1 x) xt DmapA (DmapX x a xt) (Dexp1' a)) <- ({a} {x} {xt:unmap x a} unmap-expand (Dexp2 x) (unmap/app (DmapX x a xt) DmapR) (DmapB x a xt) (DmapM x a xt) (Dexp2' a)). - : unmap-expand (eexpand/sigma Dexp2 Dexp1) DmapR (tunmap/sigma (DmapB : {x} {a} unmap x a -> tunmap (B x) (L a)) DmapA) (unmap/pair DmapM2 DmapM1) (expand-il/sigma Dexp2' Dexp1') <- unmap-expand Dexp1 (unmap/pi1 DmapR) DmapA DmapM1 Dexp1' <- unmap-expand Dexp2 (unmap/pi2 DmapR) (DmapB _ _ (unmap/pi1 DmapR)) DmapM2 Dexp2'. - : unmap-expand eexpand/sing _ (tunmap/sing D) D expand-il/sing. - : unmap-expand eexpand/one _ tunmap/one unmap/star expand-il/one. %worlds (conblock | unmap-block) (unmap-expand _ _ _ _ _). %total D (unmap-expand D _ _ _ _). unmap-skof : skof SK A B %% -> tunmap A K -> ({x} {a} unmap x a -> tunmap (B x) (L a)) -> skof-il SK K L -> type. %mode unmap-skof +X1 -X2 -X3 -X4. - : unmap-skof skof/t tunmap/one ([_] [_] [_] tunmap/t) skof-il/t. - : unmap-skof (skof/pi Dexpand Dskof2 Dskof1) (tunmap/sigma ([y] [b] [yt] tunmap/pi ([_] [_] [_] DmapD) (DmapA y b yt)) DmapC) ([w] [c] [wt] tunmap/pi ([x] [a] [xt] DmapB _ _ (unmap/app (DmapX _ _ (unmap/pi1 wt) _ _ xt) (unmap/pi2 wt))) (DmapA _ _ (unmap/pi1 wt))) (skof-il/pi Dexpand' Dskof2' Dskof1') <- unmap-skof Dskof1 DmapC DmapA Dskof1' <- unmap-skof Dskof2 DmapD DmapB Dskof2' <- ({b} {y} {yt:unmap y b} {a} {x} {xt:unmap x a} unmap-expand (Dexpand y x) xt (DmapA y b yt) (DmapX y b yt x a xt) (Dexpand' b a)). - : unmap-skof (skof/sigma Dexpand Dskof2 Dskof1) (tunmap/sigma ([y] [b] [yt] tunmap/pi ([_] [_] [_] DmapD) (DmapA y b yt)) DmapC) ([w] [c] [wt] tunmap/sigma ([x] [a] [xt] DmapB _ _ (unmap/app (DmapX _ _ (unmap/pi1 wt) _ _ xt) (unmap/pi2 wt))) (DmapA _ _ (unmap/pi1 wt))) (skof-il/sigma Dexpand' Dskof2' Dskof1') <- unmap-skof Dskof1 DmapC DmapA Dskof1' <- unmap-skof Dskof2 DmapD DmapB Dskof2' <- ({b} {y} {yt:unmap y b} {a} {x} {xt:unmap x a} unmap-expand (Dexpand y x) xt (DmapA y b yt) (DmapX y b yt x a xt) (Dexpand' b a)). - : unmap-skof skof/sing tunmap/t ([x] [a] [xt] tunmap/sing xt) skof-il/sing. - : unmap-skof skof/one tunmap/one ([_] [_] [_] tunmap/one) skof-il/one. %worlds (conblock | unmap-block) (unmap-skof _ _ _ _). %total D (unmap-skof D _ _ _). unmap-vof : evof X A -> unmap X C %% -> tunmap A K -> cn-of C K -> type. %mode unmap-vof +X1 +X2 -X3 -X4. unmap-of : eof M A -> unmap M C %% -> tunmap A K -> cn-of C K -> type. %mode unmap-of +X1 +X2 -X3 -X4. unmap-of' : eof M A -> unmap M C -> tunmap A K %% -> cn-of C K -> type. %mode unmap-of' +X1 +X2 +X3 -X4. unmap-wf : ewf A %% -> tunmap A K -> kd-wf K -> type. %mode unmap-wf +X1 -X2 -X3. unmap-wf' : ewf A -> tunmap A K %% -> kd-wf K -> type. %mode unmap-wf' +X1 +X2 -X3. unmap-subtp : subtp A B -> tunmap A K -> tunmap B L %% -> kd-sub K L -> type. %mode unmap-subtp +X1 +X2 +X3 -X4. unmap-tequiv : tequiv A B -> tunmap A K -> tunmap B L %% -> kd-equiv K L -> type. %mode unmap-tequiv +X1 +X2 +X3 -X4. unmap-equiv : unmap M C -> unmap N D -> equiv M N A %% -> tunmap A K -> cn-equiv C D K -> type. %mode unmap-equiv +X1 +X2 +X3 -X4 -X5. unmap-equiv' : unmap M C -> unmap N D -> equiv M N A -> tunmap A K %% -> cn-equiv C D K -> type. %mode unmap-equiv' +X1 +X2 +X3 +X4 -X5. - : (map-of _ _ _ _ -> unmap-of _ _ _ _) -> type. %block unmap-bind : some {K:kind} {B:etp} {Dmap:tunmap B K} {Dwf:kd-wf K} block {a:con} {da:cn-of a K} {das:cn-assm da} {_:mcn-assm da das} {_:cn-of-reg da Dwf} {x:eterm} {dx:evof x B} {xt:unmap x a} {_:can-unmap x xt} {_:unmap-vof dx xt Dmap da}. %block invert-bind-for-unmap-of : some {K:kind} {K':kind} {B:etp} {DmapK:tmap K B} {DmapB:tunmap B K'} {DwfK:kd-wf K} {DwfB:ewf B} {DequivK:kd-equiv K K'} block {a:con} {da:cn-of a K} {das:cn-assm da} {_:mcn-assm da das} {_:cn-of-reg da DwfK} {x:eterm} {dx:evof x B} {at:map a x} {xt:unmap x a} {_:can-map a at} {_:map-of da at DmapK (eof/var DwfB dx)} {_:can-unmap x xt} {_:unmap-vof dx xt DmapB (cn-of/equiv DequivK da)}. %%% Hack to get coverage checker to split - : unmap-vof _ unmap/unit tunmap/t cn-of/unit. - : unmap-of (eof/var _ Dvof) D Dt Dof <- unmap-vof Dvof D Dt Dof. - : unmap-of (eof/app Dof2 Dof1) (unmap/app Dmap2 Dmap1) (DmapB _ _ Dmap2) (cn-of/app Dof2' Dof1') <- unmap-of Dof1 Dmap1 (tunmap/pi DmapB DmapA) Dof1' <- unmap-of' Dof2 Dmap2 DmapA Dof2'. - : unmap-of (eof/pi1 Dof) (unmap/pi1 Dmap) DmapA (cn-of/pi1 Dof') <- unmap-of Dof Dmap (tunmap/sigma DmapB DmapA) Dof'. - : unmap-of (eof/pi2 Dof) (unmap/pi2 Dmap) (DmapB _ _ (unmap/pi1 Dmap)) (cn-of/pi2 Dof') <- unmap-of Dof Dmap (tunmap/sigma DmapB DmapA) Dof'. - : unmap-of (eof/lam Dof Dwf) (unmap/lam Dmap DmapA) (tunmap/pi DmapB DmapA) (cn-of/lam Dof' Dwf') <- unmap-wf' Dwf DmapA Dwf' <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e Dwf' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA e -> unmap-of (Dof x d) (Dmap x a xt) (DmapB x a xt) (Dof' a e)). - : unmap-of (eof/pair Dwf2 Dof2 Dof1) (unmap/pair Dmap2 Dmap1) (tunmap/sigma DmapB DmapA) (cn-of/pair Dwf2' Dof2' Dof1') <- unmap-of Dof1 Dmap1 DmapA Dof1' <- cn-of-reg Dof1' Dwf1' <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e Dwf1' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA e -> unmap-wf (Dwf2 x d) (DmapB x a xt) (Dwf2' a e)) <- unmap-of' Dof2 Dmap2 (DmapB _ _ Dmap1) Dof2'. - : unmap-of eof/star unmap/star tunmap/one cn-of/star. - : unmap-of (eof/sing Dof) Dmap (tunmap/sing Dmap) (cn-of/sing Dof') <- unmap-of' Dof Dmap tunmap/t Dof'. - : unmap-of (eof/subsume Dsub Dof) Dmap DmapB (cn-of/subsume Dsub' Dof') <- unmap-of Dof Dmap DmapA Dof' <- can-tunmap _ DmapB <- unmap-subtp Dsub DmapA DmapB Dsub'. - : unmap-of (eof/extpi Dof2 Dof1) Dmap (tunmap/pi DmapB DmapA) (cn-of/extpi Dof2' Dof1') <- unmap-of Dof1 Dmap (tunmap/pi _ DmapA) Dof1' <- cn-of-reg Dof1' (kd-wf/pi _ DwfK) <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfK -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA e -> unmap-of (Dof2 x d) (unmap/app xt Dmap) (DmapB x a xt) (Dof2' a e)). - : unmap-of (eof/extsigma Dwf2 Dof2 Dof1) Dmap (tunmap/sigma DmapB DmapA) (cn-of/extsigma Dwf2' Dof2' Dof1') <- unmap-of Dof1 (unmap/pi1 Dmap) DmapA Dof1' <- cn-of-reg Dof1' DwfA <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA e -> unmap-wf (Dwf2 x d) (DmapB x a xt) (Dwf2' a e)) <- unmap-of' Dof2 (unmap/pi2 Dmap) (DmapB _ _ (unmap/pi1 Dmap)) Dof2'. - : unmap-of (eof/const _ (ekof/i etopen/t ckof/unit)) unmap/unit tunmap/t cn-of/unit. - : unmap-of (eof/const _ (ekof/i etopen/t ckof/void)) unmap/void tunmap/t cn-of/void. - : unmap-of (eof/const _ (ekof/i etopen/t ckof/tagged)) unmap/tagged tunmap/t cn-of/tagged. - : unmap-of (eof/const _ (ekof/i (etopen/arrow etopen/t etp-skel/t etopen/t) ckof/ref)) unmap/ref (tunmap/pi ([_] [_] [_] tunmap/t) tunmap/t) (cn-of/lam ([a] [e] cn-of/ref e) kd-wf/t). - : unmap-of (eof/const _ (ekof/i (etopen/arrow etopen/t etp-skel/t etopen/t) ckof/tag)) unmap/tag (tunmap/pi ([_] [_] [_] tunmap/t) tunmap/t) (cn-of/lam ([a] [e] cn-of/tag e) kd-wf/t). - : unmap-of (eof/const _ (ekof/i (etopen/arrow etopen/t etp-skel/t etopen/t) ckof/labeled)) unmap/labeled (tunmap/pi ([_] [_] [_] tunmap/t) tunmap/t) (cn-of/lam ([a] [e] cn-of/labeled e) kd-wf/t). - : unmap-of (eof/const _ (ekof/i (etopen/arrow (etopen/arrow etopen/t etp-skel/t etopen/t) etp-skel/t etopen/t) ckof/arrow)) unmap/arrow (tunmap/pi ([_] [_] [_] tunmap/pi ([_] [_] [_] tunmap/t) tunmap/t) tunmap/t) (cn-of/lam ([a] [e] cn-of/lam ([b] [f] cn-of/arrow f e) kd-wf/t) kd-wf/t). - : unmap-of (eof/const _ (ekof/i (etopen/arrow (etopen/arrow etopen/t etp-skel/t etopen/t) etp-skel/t etopen/t) ckof/prod)) unmap/prod (tunmap/pi ([_] [_] [_] tunmap/pi ([_] [_] [_] tunmap/t) tunmap/t) tunmap/t) (cn-of/lam ([a] [e] cn-of/lam ([b] [f] cn-of/prod f e) kd-wf/t) kd-wf/t). - : unmap-of (eof/const _ (ekof/i (etopen/arrow (etopen/arrow etopen/t etp-skel/t etopen/t) etp-skel/t etopen/t) ckof/plus)) unmap/plus (tunmap/pi ([_] [_] [_] tunmap/pi ([_] [_] [_] tunmap/t) tunmap/t) tunmap/t) (cn-of/lam ([a] [e] cn-of/lam ([b] [f] cn-of/plus f e) kd-wf/t) kd-wf/t). - : unmap-of (eof/const _ (ekof/i (Dopen : etopen _ Q) (ckof/rec (Dcskof : cskof SK Dc Ac)))) (unmap/rec (Dskof-il : skof-il SK K L)) %% Dtunmap (cn-of/lam ([b] [e] cn-of/rec (cn-of/pi2 (cn-of/pi2 e)) ([a1] [d1] [a2] [d2] cn-of/app d2 (cn-of/app d1 (cn-of/pi1 (cn-of/pi2 e)))) (DwfL _ (cn-of/pi1 e))) (kd-wf/sigma ([a] [d] kd-wf/sigma ([_] [_] DwfL a d) (kd-wf/pi ([_] [_] kd-wf/pi ([_] [_] kd-wf/t) (DwfL a d)) (kd-wf/pi ([_] [_] kd-wf/t) (DwfL a d)))) DwfK)) <- cskof-implies-skof Dcskof DopenA DskelA DopenB (Dskof : skof SK D A) <- ({x} can-etp-skel _ (DskelB x)) <- etopen-fun (etopen-rec _ _ _ _ _ _ DopenA DskelA DopenB DskelB) Dopen DeqQ <- unmap-skof Dskof DunmapD DunmapA Dskof-il' <- skof-il-fun Dskof-il' Dskof-il DeqK DeqL <- tunmap-resp etp-eq/i DeqK DunmapD DunmapD' <- ({a} {x} {xt} tunmap-resp etp-eq/i (DeqL a) (DunmapA x a xt) (DunmapA' x a xt)) <- tunmap-resp DeqQ kind-eq/i (tunmap/pi ([_] [_] [_] tunmap/t) (tunmap/sigma ([y] [b] [yt] tunmap/sigma ([_] [_] [_] DunmapA' y b yt : tunmap (A y) (L b)) (tunmap/pi ([_] [_] [_] tunmap/pi ([_] [_] [_] tunmap/t) (DunmapA' y b yt)) (tunmap/pi ([_] [_] [_] tunmap/t) (DunmapA' y b yt)))) (DunmapD' : tunmap D K))) Dtunmap <- skof-il-reg Dskof-il (DwfK : kd-wf K) (DwfL : {b} cn-of b K -> kd-wf (L b)). %%% - : unmap-of' Dof Dmap DmapA Dof'' <- unmap-of Dof Dmap DmapA' Dof' <- tunmap-fun DmapA' DmapA Deq <- cn-of-resp con-eq/i Deq Dof' Dof''. %%% - : unmap-wf ewf/t tunmap/t kd-wf/t. - : unmap-wf (ewf/pi Dwf2 Dwf1) (tunmap/pi Dmap2 Dmap1) (kd-wf/pi Dwf2' Dwf1') <- unmap-wf Dwf1 Dmap1 Dwf1' <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e Dwf1' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt Dmap1 e -> unmap-wf (Dwf2 x d) (Dmap2 x a xt) (Dwf2' a e)). - : unmap-wf (ewf/sigma Dwf2 Dwf1) (tunmap/sigma Dmap2 Dmap1) (kd-wf/sigma Dwf2' Dwf1') <- unmap-wf Dwf1 Dmap1 Dwf1' <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e Dwf1' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt Dmap1 e -> unmap-wf (Dwf2 x d) (Dmap2 x a xt) (Dwf2' a e)). - : unmap-wf (ewf/sing Dof) (tunmap/sing Dmap) (kd-wf/sing Dof') <- can-unmap _ Dmap <- unmap-of Dof Dmap tunmap/t Dof'. - : unmap-wf ewf/one tunmap/one kd-wf/one. %%% - : unmap-wf' Dwf Dmap Dwf'' <- unmap-wf Dwf Dmap' Dwf' <- tunmap-fun Dmap' Dmap Deq <- kd-wf-resp Deq Dwf' Dwf''. %%% - : unmap-subtp (subtp/reflex Dequiv) Dmap1 Dmap2 (kd-sub/refl Dequiv') <- unmap-tequiv Dequiv Dmap1 Dmap2 Dequiv'. - : unmap-subtp (subtp/trans Dsub23 Dsub12) Dmap1 Dmap3 (kd-sub/trans Dsub23' Dsub12') <- can-tunmap _ Dmap2 <- unmap-subtp Dsub12 Dmap1 Dmap2 Dsub12' <- unmap-subtp Dsub23 Dmap2 Dmap3 Dsub23'. - : unmap-subtp (subtp/sing_t Dof) (tunmap/sing Dmap) tunmap/t (kd-sub/sing-t Dof') <- unmap-of' Dof Dmap tunmap/t Dof'. - : unmap-subtp (subtp/pi DwfB1 DsubB DsubA) (tunmap/pi DmapB1 DmapA1) (tunmap/pi DmapB2 DmapA2) (kd-sub/pi DwfB1' DsubB' DsubA') <- unmap-subtp DsubA DmapA2 DmapA1 DsubA' <- kd-sub-reg DsubA' DwfA2' DwfA1' <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA2' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA2 e -> unmap-subtp (DsubB x d) (DmapB1 x a xt) (DmapB2 x a xt) (DsubB' a e)) <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA1' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA1 e -> unmap-wf' (DwfB1 x d) (DmapB1 x a xt) (DwfB1' a e)). - : unmap-subtp (subtp/sigma DwfB2 DsubB DsubA) (tunmap/sigma DmapB1 DmapA1) (tunmap/sigma DmapB2 DmapA2) (kd-sub/sigma DwfB2' DsubB' DsubA') <- unmap-subtp DsubA DmapA1 DmapA2 DsubA' <- kd-sub-reg DsubA' DwfA1' DwfA2' <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA1' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA1 e -> unmap-subtp (DsubB x d) (DmapB1 x a xt) (DmapB2 x a xt) (DsubB' a e)) <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA2' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA2 e -> unmap-wf' (DwfB2 x d) (DmapB2 x a xt) (DwfB2' a e)). %%% - : unmap-tequiv (tequiv/reflex Dwf) Dmap Dmap' Dequiv' <- tunmap-fun Dmap Dmap' Deq <- unmap-wf' Dwf Dmap Dwf' <- kd-equiv-resp kind-eq/i Deq (kd-equiv/refl Dwf') Dequiv'. - : unmap-tequiv (tequiv/symm Dequiv) Dmap Dmap' (kd-equiv/symm Dequiv') <- unmap-tequiv Dequiv Dmap' Dmap Dequiv'. - : unmap-tequiv (tequiv/trans Dsub23 Dsub12) Dmap1 Dmap3 (kd-equiv/trans Dsub23' Dsub12') <- can-tunmap _ Dmap2 <- unmap-tequiv Dsub12 Dmap1 Dmap2 Dsub12' <- unmap-tequiv Dsub23 Dmap2 Dmap3 Dsub23'. - : unmap-tequiv (tequiv/sing Dequiv) (tunmap/sing Dmap1) (tunmap/sing Dmap2) (kd-equiv/sing Dequiv') <- unmap-equiv' Dmap1 Dmap2 Dequiv tunmap/t Dequiv'. - : unmap-tequiv (tequiv/pi DequivB DequivA) (tunmap/pi DmapB1 DmapA1) (tunmap/pi DmapB2 DmapA2) (kd-equiv/pi DequivB' DequivA') <- unmap-tequiv DequivA DmapA1 DmapA2 DequivA' <- kd-equiv-reg DequivA' DwfA' _ <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA1 e -> unmap-tequiv (DequivB x d) (DmapB1 x a xt) (DmapB2 x a xt) (DequivB' a e)). - : unmap-tequiv (tequiv/sigma DequivB DequivA) (tunmap/sigma DmapB1 DmapA1) (tunmap/sigma DmapB2 DmapA2) (kd-equiv/sigma DequivB' DequivA') <- unmap-tequiv DequivA DmapA1 DmapA2 DequivA' <- kd-equiv-reg DequivA' DwfA' _ <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA1 e -> unmap-tequiv (DequivB x d) (DmapB1 x a xt) (DmapB2 x a xt) (DequivB' a e)). %%% - : unmap-equiv Dmap Dmap' (equiv/reflex Dof) DmapA Dequiv' <- unmap-fun Dmap Dmap' Deq <- unmap-of Dof Dmap DmapA Dof' <- cn-equiv-resp con-eq/i Deq kind-eq/i (cn-equiv/refl Dof') Dequiv'. - : unmap-equiv Dmap1 Dmap2 (equiv/symm Dequiv) DmapA (cn-equiv/symm Dequiv') <- unmap-equiv Dmap2 Dmap1 Dequiv DmapA Dequiv'. - : unmap-equiv Dmap1 Dmap3 (equiv/trans Dsub23 Dsub12) DmapA (cn-equiv/trans Dsub23' Dsub12') <- can-unmap _ Dmap2 <- unmap-equiv Dmap1 Dmap2 Dsub12 DmapA Dsub12' <- unmap-equiv' Dmap2 Dmap3 Dsub23 DmapA Dsub23'. - : unmap-equiv (unmap/app Dmap2 Dmap1) (unmap/app Dmap2' Dmap1') (equiv/app Dequiv2 Dequiv1) (DmapB _ _ Dmap2) (cn-equiv/app Dequiv2' Dequiv1') <- unmap-equiv Dmap1 Dmap1' Dequiv1 (tunmap/pi DmapB DmapA) Dequiv1' <- unmap-equiv' Dmap2 Dmap2' Dequiv2 DmapA Dequiv2'. - : unmap-equiv (unmap/pi1 Dmap1) (unmap/pi1 Dmap2) (equiv/pi1 Dequiv) DmapA (cn-equiv/pi1 Dequiv') <- unmap-equiv Dmap1 Dmap2 Dequiv (tunmap/sigma DmapB DmapA) Dequiv'. - : unmap-equiv (unmap/pi2 Dmap1) (unmap/pi2 Dmap2) (equiv/pi2 Dequiv) (DmapB _ _ (unmap/pi1 Dmap1)) (cn-equiv/pi2 Dequiv') <- unmap-equiv Dmap1 Dmap2 Dequiv (tunmap/sigma DmapB DmapA) Dequiv'. - : unmap-equiv (unmap/lam Dmap1 DmapA1) (unmap/lam Dmap2 DmapA2) (equiv/lam Dequiv2 Dequiv1) (tunmap/pi DmapB DmapA1) (cn-equiv/lam Dequiv2' Dequiv1') <- unmap-tequiv Dequiv1 DmapA1 DmapA2 Dequiv1' <- kd-equiv-reg Dequiv1' DwfA' _ <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA1 e -> unmap-equiv (Dmap1 x a xt) (Dmap2 x a xt) (Dequiv2 x d) (DmapB x a xt) (Dequiv2' a e)). - : unmap-equiv (unmap/pair Dmap2 Dmap1) (unmap/pair Dmap2' Dmap1') (equiv/pair Dwf2 Dequiv2 Dequiv1) (tunmap/sigma DmapB DmapA) (cn-equiv/pair Dwf2' Dequiv2' Dequiv1') <- unmap-equiv Dmap1 Dmap1' Dequiv1 DmapA Dequiv1' <- cn-equiv-reg Dequiv1' _ _ DwfA' <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA e -> unmap-wf (Dwf2 x d) (DmapB x a xt) (Dwf2' a e)) <- unmap-equiv' Dmap2 Dmap2' Dequiv2 (DmapB _ _ Dmap1) Dequiv2'. - : unmap-equiv Dmap1 Dmap2 (equiv/sing Dequiv) (tunmap/sing Dmap1) (cn-equiv/sing Dequiv') <- unmap-equiv' Dmap1 Dmap2 Dequiv tunmap/t Dequiv'. - : unmap-equiv Dmap1 Dmap2 (equiv/singelim Dof) tunmap/t (cn-equiv/singelim Dof') <- unmap-of' Dof Dmap1 (tunmap/sing Dmap2) Dof'. - : unmap-equiv Dmap1 Dmap2 (equiv/extpi Dequiv Dof2 Dof1) (tunmap/pi DmapB DmapA) (cn-equiv/extpi Dequiv' Dof2' Dof1') <- unmap-of Dof1 Dmap1 (tunmap/pi DmapB' DmapA) Dof1' <- cn-of-reg Dof1' (kd-wf/pi _ DwfA') <- ({a} {x} {xt:unmap x a} can-unmap x xt -> can-tunmap _ (DmapB'' x a xt)) <- unmap-of' Dof2 Dmap2 (tunmap/pi DmapB'' DmapA) Dof2' <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA e -> unmap-equiv (unmap/app xt Dmap1) (unmap/app xt Dmap2) (Dequiv x d) (DmapB x a xt) (Dequiv' a e)). - : unmap-equiv Dmap1 Dmap2 (equiv/extpiw Dequiv DequivPre) (tunmap/pi DmapB DmapA) (cn-equiv/extpiw Dequiv' DequivPre') <- unmap-equiv Dmap1 Dmap2 DequivPre (tunmap/pi _ DmapA) DequivPre' <- cn-equiv-reg DequivPre' _ _ (kd-wf/pi _ DwfA') <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA e -> unmap-equiv (unmap/app xt Dmap1) (unmap/app xt Dmap2) (Dequiv x d) (DmapB x a xt) (Dequiv' a e)). - : unmap-equiv Dmap Dmap' (equiv/extsigma Dwf2 Dequiv2 Dequiv1) (tunmap/sigma DmapB DmapA) (cn-equiv/extsigma Dwf2' Dequiv2' Dequiv1') <- unmap-equiv (unmap/pi1 Dmap) (unmap/pi1 Dmap') Dequiv1 DmapA Dequiv1' <- cn-equiv-reg Dequiv1' _ _ DwfA' <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA e -> unmap-wf (Dwf2 x d) (DmapB x a xt) (Dwf2' a e)) <- unmap-equiv' (unmap/pi2 Dmap) (unmap/pi2 Dmap') Dequiv2 (DmapB _ _ (unmap/pi1 Dmap)) Dequiv2'. - : unmap-equiv Dmap1 Dmap2 (equiv/one Dof2 Dof1) tunmap/one (cn-equiv/one Dof2' Dof1') <- unmap-of' Dof1 Dmap1 tunmap/one Dof1' <- unmap-of' Dof2 Dmap2 tunmap/one Dof2'. - : unmap-equiv Dmap1 Dmap2 (equiv/subsume Dsub Dequiv) DmapB (cn-equiv/subsume Dsub' Dequiv') <- unmap-equiv Dmap1 Dmap2 Dequiv DmapA Dequiv' <- can-tunmap _ DmapB <- unmap-subtp Dsub DmapA DmapB Dsub'. - : unmap-equiv (unmap/app Dmap2 (unmap/lam Dmap1 DmapA)) Dmap (equiv/beta Dof2 Dof1) (DmapB _ _ Dmap2) Dequiv'' <- unmap-fun (Dmap1 _ _ Dmap2) Dmap Deq <- unmap-of' Dof2 Dmap2 DmapA Dof2' <- cn-of-reg Dof2' DwfA' <- ({a} {e} {es} mcn-assm e es -> cn-of-reg e DwfA' -> {x} {d} {xt} can-unmap x xt -> unmap-vof d xt DmapA e -> unmap-of (Dof1 x d) (Dmap1 x a xt) (DmapB x a xt) (Dof1' a e)) <- cn-equiv-resp con-eq/i Deq kind-eq/i (cn-equiv/beta Dof2' Dof1') Dequiv''. - : unmap-equiv (unmap/pi1 (unmap/pair Dmap2 Dmap1)) Dmap1' (equiv/beta1 Dof2 Dof1) DmapA Dequiv'' <- unmap-fun Dmap1 Dmap1' Deq <- unmap-of Dof1 Dmap1 DmapA Dof1' <- unmap-of Dof2 Dmap2 DmapB Dof2' <- cn-equiv-resp con-eq/i Deq kind-eq/i (cn-equiv/beta1 Dof2' Dof1') Dequiv''. - : unmap-equiv (unmap/pi2 (unmap/pair Dmap2 Dmap1)) Dmap2' (equiv/beta2 Dof2 Dof1) DmapB Dequiv'' <- unmap-fun Dmap2 Dmap2' Deq <- unmap-of Dof1 Dmap1 DmapA Dof1' <- unmap-of Dof2 Dmap2 DmapB Dof2' <- cn-equiv-resp con-eq/i Deq kind-eq/i (cn-equiv/beta2 Dof2' Dof1') Dequiv''. %%% - : unmap-equiv' Dmap1 Dmap2 Dequiv DmapA Dequiv'' <- unmap-equiv Dmap1 Dmap2 Dequiv DmapA' Dequiv' <- tunmap-fun DmapA' DmapA Deq <- cn-equiv-resp con-eq/i con-eq/i Deq Dequiv' Dequiv''. %worlds (unmap-bind | invert-bind-for-unmap-of) (unmap-vof _ _ _ _) (unmap-of _ _ _ _) (unmap-of' _ _ _ _) (unmap-wf _ _ _) (unmap-wf' _ _ _) (unmap-subtp _ _ _ _) (unmap-tequiv _ _ _ _) (unmap-equiv _ _ _ _ _) (unmap-equiv' _ _ _ _ _).% %total (D1 D2 D3 D4 D5 D6 D7 D8 D9) (unmap-vof D1 _ _ _) (unmap-of D2 _ _ _) (unmap-of' D3 _ _ _) (unmap-wf D4 _ _) (unmap-wf' D5 _ _) (unmap-subtp D6 _ _ _) (unmap-tequiv D7 _ _ _) (unmap-equiv _ _ D8 _ _) (unmap-equiv' _ _ D9 _ _). %%%%% Unmap inverts map %%%%% invert-map : cn-of C K -> map C M %% -> unmap M C' -> cn-equiv C C' K -> type. %mode invert-map +X1 +X2 -X3 -X4. invert-tmap : kd-wf K -> tmap K A %% -> tunmap A K' -> kd-equiv K K' -> type. %mode invert-tmap +X1 +X2 -X3 -X4. %% The rest of these are all for cn-of/extpi. invert-tmap-cn-of' : cn-of C K %% -> tmap K A -> tunmap A K' -> kd-equiv K K' -> type. %mode invert-tmap-cn-of' +X1 -X2 -X3 -X4. invert-tmap-cn-of : cn-of C K -> tmap K A %% -> tunmap A K' -> kd-equiv K K' -> type. %mode invert-tmap-cn-of +X1 +X2 -X3 -X4. invert-tmap-kd-sub : kd-sub K1 K2 -> tmap K1 A1 -> tmap K2 A2 %% -> tunmap A1 K1' -> tunmap A2 K2' -> kd-equiv K1 K1' -> kd-equiv K2 K2' -> type. %mode invert-tmap-kd-sub +X1 +X2 +X3 -X4 -X5 -X6 -X7. invert-tmap-kd-equiv : kd-equiv K1 K2 -> tmap K1 A1 -> tmap K2 A2 %% -> tunmap A1 K1' -> tunmap A2 K2' -> kd-equiv K1 K1' -> kd-equiv K2 K2' -> type. %mode invert-tmap-kd-equiv +X1 +X2 +X3 -X4 -X5 -X6 -X7. invert-tmap-1 : kd-equiv K1 K2 -> tmap K1 A1 %% -> tunmap A1 K1' -> kd-equiv K1 K1' -> type. %mode invert-tmap-1 +X1 +X2 -X3 -X4. invert-tmap-2 : kd-equiv K1 K2 -> tmap K2 A2 %% -> tunmap A2 K2' -> kd-equiv K2 K2' -> type. %mode invert-tmap-2 +X1 +X2 -X3 -X4. invert-map-1 : cn-equiv C1 C2 K -> map C1 M1 %% -> unmap M1 C1' -> cn-equiv C1 C1' K -> type. %mode invert-map-1 +X1 +X2 -X3 -X4. invert-map-2 : cn-equiv C1 C2 K -> map C2 M2 %% -> unmap M2 C2' -> cn-equiv C2 C2' K -> type. %mode invert-map-2 +X1 +X2 -X3 -X4. invert-map-2' : map C2 M2 -> cn-equiv C1 C2 K %% -> unmap M2 C2' -> cn-equiv C2 C2' K -> type. %mode invert-map-2' +X1 +X2 -X3 -X4. invert-tmap-cn-equiv' : cn-equiv C1 C2 K %% -> tmap K A -> tunmap A K' -> kd-equiv K K' -> type. %mode invert-tmap-cn-equiv' +X1 -X2 -X3 -X4. invert-tmap-cn-equiv : cn-equiv C1 C2 K -> tmap K A %% -> tunmap A K' -> kd-equiv K K' -> type. %mode invert-tmap-cn-equiv +X1 +X2 -X3 -X4. %block invert-bind : some {K:kind} {K':kind} {B:etp} {DmapK:tmap K B} {DmapB:tunmap B K'} {DwfK:kd-wf K} {DwfB:ewf B} {DequivK:kd-equiv K K'} block {a:con} {da:cn-of a K} {das:cn-assm da} {_:mcn-assm da das} {_:cn-of-reg da DwfK} {x:eterm} {dx:evof x B} {at:map a x} {xt:unmap x a} {_:can-map a at} {_:map-of da at DmapK (eof/var DwfB dx)} {_:can-unmap x xt} {_:unmap-vof dx xt DmapB (cn-of/equiv DequivK da)} {_:invert-map da at xt (cn-equiv/refl da)} {_:invert-tmap-cn-of' da DmapK DmapB DequivK}. -app : invert-map (cn-of/app Dof2 Dof1) (map/app D2 D1) (unmap/app D2' D1') (cn-equiv/app Dequiv2 Dequiv1) <- invert-map Dof1 D1 D1' Dequiv1 <- invert-map Dof2 D2 D2' Dequiv2. -pi1 : invert-map (cn-of/pi1 Dof) (map/pi1 D) (unmap/pi1 D') (cn-equiv/pi1 Dequiv) <- invert-map Dof D D' Dequiv. -pi2 : invert-map (cn-of/pi2 Dof) (map/pi2 D) (unmap/pi2 D') (cn-equiv/pi2 Dequiv) <- invert-map Dof D D' Dequiv. -lam : invert-map (cn-of/lam Dof2 Dof1) (map/lam D2 D1) (unmap/lam D2' D1') (cn-equiv/lam Dequiv2 Dequiv1) <- invert-tmap Dof1 D1 D1' Dequiv1 <- kd-equiv-reg Dequiv1 DwfK _ <- map-wf' Dof1 D1 DwfA <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK -> {x} {dx:evof x A} {at} {xt} can-map a at -> map-of da at D1 (eof/var DwfA dx) -> can-unmap x xt -> unmap-vof dx xt D1' (cn-of/equiv Dequiv1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da D1 D1' Dequiv1 -> invert-map (Dof2 a da) (D2 a x at) (D2' x a xt) (Dequiv2 a da)). -pair : invert-map (cn-of/pair Dwf Dof2 Dof1) (map/pair D2 D1) (unmap/pair D2' D1') (cn-equiv/pair Dwf Dequiv2 Dequiv1) <- invert-map Dof1 D1 D1' Dequiv1 <- invert-map Dof2 D2 D2' Dequiv2. -star : invert-map cn-of/star map/star unmap/star (cn-equiv/refl cn-of/star). -sing : invert-map (cn-of/sing Dof) D D' (cn-equiv/sing Dequiv) <- invert-map Dof D D' Dequiv. -piext : invert-map (cn-of/extpi (Dof : {a} cn-of a K1 -> cn-of (app C a) (K2 a)) (DofPre : cn-of C (pi K1 K2p))) (DmapC : map C M) DunmapM (cn-equiv/extpi Dequiv2' DofPre' DofPre) <- invert-map DofPre DmapC (DunmapM : unmap M C') (DequivC : cn-equiv C C' (pi K1 K2p)) <- can-tmap K1 (DmapK1 : tmap K1 A1) <- ({x} {a} {at:map a x} can-map a at -> can-tmap (K2p a) (DmapK2p a x at : tmap (K2p a) (A2p x))) <- invert-tmap-cn-of DofPre (tmap/pi DmapK2p DmapK1) (tunmap/pi (DunmapA2 : {x} {a} unmap x a -> tunmap (A2p x) (K2p' a)) (DunmapA1 : tunmap A1 K1')) (DequivKpre : kd-equiv (pi K1 K2p) (pi K1' K2p')) <- injective-pi DequivKpre (DequivK1 : kd-equiv K1 K1') _ <- cn-of-reg DofPre (kd-wf/pi _ (DwfK1 : kd-wf K1)) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> {x} {dx:evof x A1} {at} {xt} can-map a at -> map-of da at DmapK1 (eof/var DwfA1 dx) -> can-unmap x xt -> unmap-vof dx xt DunmapA1 (cn-of/equiv DequivK1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da DmapK1 DunmapA1 DequivK1 -> invert-map (Dof a da) (map/app at DmapC) (unmap/app xt (DunmapM' x a xt : unmap M (C'' a))) (Dequiv2 a da : cn-equiv (app C a) (app (C'' a) a) (K2 a))) <- ({a} {x} {xt:unmap x a} unmap-fun (DunmapM' x a xt) DunmapM (Deq a : con-eq (C'' a) C')) <- ({a} con-resp-con ([b] app b a) (Deq a) (Deq' a : con-eq (app (C'' a) a) (app C' a))) <- ({a} {d:cn-of a K1} cn-equiv-resp con-eq/i (Deq' a) kind-eq/i (Dequiv2 a d) (Dequiv2' a d : cn-equiv (app C a) (app C' a) (K2 a))) <- cn-equiv-reg DequivC _ (DofPre' : cn-of C' (pi K1 K2p)) _. -sigext : invert-map (cn-of/extsigma Dwf Dof2 Dof1) D D' (cn-equiv/extsigma Dwf Dequiv2' Dequiv1) <- invert-map Dof1 (map/pi1 D) (unmap/pi1 D') Dequiv1 <- invert-map Dof2 (map/pi2 D) (unmap/pi2 D'') Dequiv2 <- unmap-fun D'' D' Deq <- con-resp-con pi2 Deq Deq' <- cn-equiv-resp con-eq/i Deq' kind-eq/i Dequiv2 Dequiv2'. -sub : invert-map (cn-of/subsume Dsub Dof) D D' (cn-equiv/subsume Dsub Dequiv) <- invert-map Dof D D' Dequiv. -unit : invert-map cn-of/unit map/unit unmap/unit (cn-equiv/refl cn-of/unit). -void : invert-map cn-of/void map/void unmap/void (cn-equiv/refl cn-of/void). -tagged : invert-map cn-of/tagged map/tagged unmap/tagged (cn-equiv/refl cn-of/tagged). -ref : invert-map (cn-of/ref Dof) (map/ref D) (unmap/app D' unmap/ref) (cn-equiv/trans (cn-equiv/app Dequiv (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/ref d) kd-wf/t))) (cn-equiv/symm (cn-equiv/beta Dof ([a] [e] cn-of/ref e)))) <- invert-map Dof D D' Dequiv. -tag : invert-map (cn-of/tag Dof) (map/tag D) (unmap/app D' unmap/tag) (cn-equiv/trans (cn-equiv/app Dequiv (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/tag d) kd-wf/t))) (cn-equiv/symm (cn-equiv/beta Dof ([a] [e] cn-of/tag e)))) <- invert-map Dof D D' Dequiv. -lab : invert-map (cn-of/labeled Dof) (map/labeled D) (unmap/app D' unmap/labeled) (cn-equiv/trans (cn-equiv/app Dequiv (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/labeled d : cn-of (labeled I _) _) kd-wf/t))) (cn-equiv/symm (cn-equiv/beta Dof ([a] [e] cn-of/labeled e)))) <- invert-map Dof D D' Dequiv. -arrow : invert-map (cn-of/arrow Dof2 Dof1) (map/arrow D2 D1) (unmap/app D2' (unmap/app D1' unmap/arrow)) (cn-equiv/trans (cn-equiv/app Dequiv2 (cn-equiv/app Dequiv1 (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/lam ([b] [e] cn-of/arrow e d) kd-wf/t) kd-wf/t)))) (cn-equiv/symm (cn-equiv/trans (cn-equiv/beta Dof2 ([b] [e] cn-of/arrow e Dof1)) (cn-equiv/app (cn-equiv/refl Dof2) (cn-equiv/beta Dof1 ([a] [d] cn-of/lam ([b] [e] cn-of/arrow e d) kd-wf/t)))))) <- invert-map Dof1 D1 D1' Dequiv1 <- invert-map Dof2 D2 D2' Dequiv2. -prod : invert-map (cn-of/prod Dof2 Dof1) (map/prod D2 D1) (unmap/app D2' (unmap/app D1' unmap/prod)) (cn-equiv/trans (cn-equiv/app Dequiv2 (cn-equiv/app Dequiv1 (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/lam ([b] [e] cn-of/prod e d) kd-wf/t) kd-wf/t)))) (cn-equiv/symm (cn-equiv/trans (cn-equiv/beta Dof2 ([b] [e] cn-of/prod e Dof1)) (cn-equiv/app (cn-equiv/refl Dof2) (cn-equiv/beta Dof1 ([a] [d] cn-of/lam ([b] [e] cn-of/prod e d) kd-wf/t)))))) <- invert-map Dof1 D1 D1' Dequiv1 <- invert-map Dof2 D2 D2' Dequiv2. -plus : invert-map (cn-of/plus Dof2 Dof1) (map/plus D2 D1) (unmap/app D2' (unmap/app D1' unmap/plus)) (cn-equiv/trans (cn-equiv/app Dequiv2 (cn-equiv/app Dequiv1 (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/lam ([b] [e] cn-of/plus e d) kd-wf/t) kd-wf/t)))) (cn-equiv/symm (cn-equiv/trans (cn-equiv/beta Dof2 ([b] [e] cn-of/plus e Dof1)) (cn-equiv/app (cn-equiv/refl Dof2) (cn-equiv/beta Dof1 ([a] [d] cn-of/lam ([b] [e] cn-of/plus e d) kd-wf/t)))))) <- invert-map Dof1 D1 D1' Dequiv1 <- invert-map Dof2 D2 D2' Dequiv2. -rec : invert-map (cn-of/rec (DofC2 : cn-of C2 K) (DofC1 : {a} cn-of a (pi K ([_] t)) -> {b} cn-of b K -> cn-of (C1 a b) t) (DwfK : kd-wf K)) (map/rec (Dflay : flay A SK MA) (DmapC2 : map C2 M2) (DmapC1 : {a} {x} map a x -> {b} {y} map b y -> map (C1 a b) (M1 x y)) (DmapK : tmap K A)) %% (unmap/app (unmap/pair (unmap/pair DmapM2 (unmap/lam ([x] [a] [xt] unmap/lam ([y] [b] [yt] DmapM1 x a xt y b yt) DmapA) (tunmap/pi ([_] [_] [_] tunmap/t) DmapA))) DmapMA) (unmap/rec Dskof')) (cn-equiv/symm (cn-equiv/trans (cn-equiv/symm (cn-equiv/rec (cn-equiv/symm (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm DequivC2) (cn-equiv/beta2 DofC2' (cn-of/lam ([a] [d] cn-of/lam ([b] [e] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) (cn-equiv/pi2-nd (cn-equiv/beta2 (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/lam ([a] [d] cn-of/lam ([b] [e] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK'))) DofCK)))) ([a] [d] [b] [e] cn-equiv/symm (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm (DequivC1 a d b e)) (cn-equiv/beta-nd (cn-of/equiv DequivK e) ([b] [e] DofC1' a d b (cn-of/equiv (kd-equiv/symm DequivK) e)))) (cn-equiv/app-nd (cn-equiv/refl e) (cn-equiv/trans (cn-equiv/beta-nd (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK) d) ([a] [d:cn-of a (pi K' ([_] t))] cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK'))) (cn-equiv/app-nd (cn-equiv/refl d) (cn-equiv/trans (cn-equiv/beta1 DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) (cn-equiv/pi1 (cn-equiv/beta2 (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) DofCK)))))))) (kd-equiv/trans (kd-equiv/trans DequivJCK DequivK'JCK) DequivK))) (cn-equiv/beta-nd (cn-of/pair ([a] [d] kd-wf/sigma ([_] [_] DwfJ a d) (kd-wf/pi ([_] [_] kd-wf/pi ([_] [_] kd-wf/t) (DwfJ a d)) (kd-wf/pi ([_] [_] kd-wf/t) (DwfJ a d)))) (cn-of/equiv (kd-equiv/sigma ([_] [_] kd-equiv/trans DequivK'JCK DequivK) (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/trans DequivK'JCK DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/trans DequivK'JCK DequivK)))) (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK'))))) DofCK) ([c] [f] cn-of/rec (cn-of/pi2 (cn-of/pi2 f)) ([a] [d] [b] [e] cn-of/app e (cn-of/app d (cn-of/pi1 (cn-of/pi2 f)))) (DwfJ _ (cn-of/pi1 f)))))) <- invert-tmap DwfK DmapK (DmapA : tunmap A K') (DequivK : kd-equiv K K') <- map-wf' DwfK DmapK (DwfA : ewf A) <- ({a} {da:cn-of a (pi K ([_] t))} {das:cn-assm da} mcn-assm da das -> cn-of-reg da (kd-wf/pi ([_] [_] kd-wf/t) DwfK) -> {x} {dx:evof x (epi A ([_] et))} {at} {xt} can-map a at -> map-of da at (tmap/pi ([_] [_] [_] tmap/t) DmapK) (eof/var (ewf/pi ([_] [_] ewf/t) DwfA) dx) -> can-unmap x xt -> unmap-vof dx xt (tunmap/pi ([_] [_] [_] tunmap/t) DmapA) (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK) da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da (tmap/pi ([_] [_] [_] tmap/t) DmapK) (tunmap/pi ([_] [_] [_] tunmap/t) DmapA) (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK) -> {b} {db:cn-of b K} {dbs} mcn-assm db dbs -> cn-of-reg db DwfK -> {y} {dy:evof y A} {bt} {yt} can-map b bt -> map-of db bt DmapK (eof/var DwfA dy) -> can-unmap y yt -> unmap-vof dy yt DmapA (cn-of/equiv DequivK db) -> invert-map db bt yt (cn-equiv/refl db) -> invert-tmap-cn-of' db DmapK DmapA DequivK -> invert-map (DofC1 a da b db) (DmapC1 a x at b y bt) (DmapM1 x a xt y b yt : unmap (M1 x y) (C1' a b)) (DequivC1 a da b db : cn-equiv (C1 a b) (C1' a b) t)) <- invert-map DofC2 DmapC2 (DmapM2 : unmap M2 C2') (DequivC2 : cn-equiv C2 C2' K) <- can-skof SK (Dskof : skof SK D E) <- flay-sound DwfA Dflay Dskof (DofMA : eof MA D) (DequivAE : tequiv A (E MA)) <- unmap-skof Dskof (DmapD : tunmap D I) (DmapE : {x} {a} unmap x a -> tunmap (E x) (J a)) (Dskof' : skof-il SK I J) <- can-unmap MA (DmapMA : unmap MA CK) <- cn-equiv-reg DequivC2 _ (DofC2' : cn-of C2' K) _ <- kd-equiv-reg DequivK _ (DwfK' : kd-wf K') <- ({a} {da} {das} mcn-assm da das -> cn-of-reg da (kd-wf/pi ([_] [_] kd-wf/t) DwfK) -> {b} {db} {dbs} mcn-assm db dbs -> cn-of-reg db DwfK -> cn-equiv-reg (DequivC1 a da b db) (DDDD1 a da b db) (DofC1' a da b db : cn-of (C1' a b) t) (DDDD2 a da b db)) <- unmap-of' DofMA DmapMA DmapD (DofCK : cn-of CK I) <- unmap-tequiv DequivAE DmapA (DmapE _ _ DmapMA) (DequivK'JCK : kd-equiv K' (J CK)) <- skof-il-reg Dskof' _ (DwfJ : {a} cn-of a I -> kd-wf (J a)) <- functionality-kd DwfJ (cn-equiv/symm (cn-equiv/beta1 (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) DofCK) : cn-equiv CK (pi1 (pair CK _)) I) (DequivJCK : kd-equiv (J CK) (J (pi1 (pair CK _)))). %%% -t : invert-tmap kd-wf/t tmap/t tunmap/t kd-equiv/t. -sing : invert-tmap (kd-wf/sing Dof) (tmap/sing D) (tunmap/sing D') (kd-equiv/sing Dequiv) <- invert-map Dof D D' Dequiv. -pi : invert-tmap (kd-wf/pi Dwf2 Dwf1) (tmap/pi Dmap2 Dmap1) (tunmap/pi Dunmap2 Dunmap1) (kd-equiv/pi Dequiv2 Dequiv1) <- invert-tmap Dwf1 Dmap1 Dunmap1 Dequiv1 <- map-wf' Dwf1 Dmap1 Dwf1' <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da Dwf1 -> {x} {dx:evof x A} {at} {xt} can-map a at -> map-of da at Dmap1 (eof/var Dwf1' dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1 (cn-of/equiv Dequiv1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1 Dunmap1 Dequiv1 -> invert-tmap (Dwf2 a da) (Dmap2 a x at) (Dunmap2 x a xt) (Dequiv2 a da)). -sigma : invert-tmap (kd-wf/sigma Dwf2 Dwf1) (tmap/sigma Dmap2 Dmap1) (tunmap/sigma Dunmap2 Dunmap1) (kd-equiv/sigma Dequiv2 Dequiv1) <- invert-tmap Dwf1 Dmap1 Dunmap1 Dequiv1 <- map-wf' Dwf1 Dmap1 Dwf1' <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da Dwf1 -> {x} {dx:evof x A} {at} {xt} can-map a at -> map-of da at Dmap1 (eof/var Dwf1' dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1 (cn-of/equiv Dequiv1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1 Dunmap1 Dequiv1 -> invert-tmap (Dwf2 a da) (Dmap2 a x at) (Dunmap2 x a xt) (Dequiv2 a da)). -one : invert-tmap kd-wf/one tmap/one tunmap/one kd-equiv/one. %%% - : invert-tmap-cn-of' (cn-of/pair Dwf2 _ Dof1) (tmap/sigma Dmap2 Dmap1) (tunmap/sigma Dunmap2 Dunmap1) (kd-equiv/sigma Dequiv2 Dequiv1) <- invert-tmap-cn-of' Dof1 Dmap1 Dunmap1 Dequiv1 <- cn-of-reg Dof1 Dwf1 <- map-wf' Dwf1 Dmap1 Dwf1' <- ({x} {a} {at} can-map a at -> can-tmap (K2 a) (Dmap2 a x at : tmap (K2 a) (A2 x))) <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da Dwf1 -> {x} {dx:evof x A} {at} {xt} can-map a at -> map-of da at Dmap1 (eof/var Dwf1' dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1 (cn-of/equiv Dequiv1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1 Dunmap1 Dequiv1 -> invert-tmap (Dwf2 a da) (Dmap2 a x at) (Dunmap2 x a xt) (Dequiv2 a da)). - : invert-tmap-cn-of' (cn-of/pi1 Dof) Dmap1 Dunmap1 Dequiv1 <- invert-tmap-cn-of' Dof (tmap/sigma Dmap2 Dmap1) (tunmap/sigma Dunmap2 Dunmap1) Dequiv <- injective-sigma Dequiv Dequiv1 Dequiv2. - : invert-tmap-cn-of' (cn-of/pi2 (DofC : cn-of C (sigma K1 K2))) (Dmap2 (pi1 C) (epi1 M) (map/pi1 DmapC)) (Dunmap2 (epi1 M) (pi1 C') (unmap/pi1 DunmapC)) (kd-equiv/trans (Dequiv2 (pi1 C') (cn-of/pi1 DofC')) Dequiv2s) <- can-tmap K1 (Dmap1 : tmap K1 A1) <- ({x} {a} {at} can-map a at -> can-tmap (K2 a) (Dmap2 a x at : tmap (K2 a) (A2 x))) <- invert-tmap-cn-of DofC (tmap/sigma Dmap2 Dmap1) (tunmap/sigma (Dunmap2 : {x} {a} unmap x a -> tunmap (A2 x) (K2' a)) (Dunmap1 : tunmap A1 K1')) (Dequiv : kd-equiv (sigma K1 K2) (sigma K1' K2')) <- injective-sigma Dequiv (Dequiv1 : kd-equiv K1 K1') (Dequiv2 : {a} cn-of a K1 -> kd-equiv (K2 a) (K2' a)) <- can-map C (DmapC : map C M) <- invert-map DofC DmapC (DunmapC : unmap M C') (DequivC : cn-equiv C C' (sigma K1 K2)) <- cn-of-reg DofC (kd-wf/sigma (Dwf2 : {a} cn-of a K1 -> kd-wf (K2 a)) _) <- functionality-kd Dwf2 (cn-equiv/pi1 DequivC) (Dequiv2s : kd-equiv (K2 (pi1 C)) (K2 (pi1 C'))) <- cn-equiv-reg DequivC _ (DofC' : cn-of C' (sigma K1 K2)) _. - : invert-tmap-cn-of' (cn-of/lam Dof Dwf1) (tmap/pi Dmap2 Dmap1) (tunmap/pi Dunmap2 Dunmap1) (kd-equiv/pi Dequiv2 Dequiv1) <- can-tmap _ Dmap1 <- invert-tmap Dwf1 Dmap1 Dunmap1 Dequiv1 <- map-wf' Dwf1 Dmap1 Dwf1' <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da Dwf1 -> {x} {dx:evof x A} {at} {xt} can-map a at -> map-of da at Dmap1 (eof/var Dwf1' dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1 (cn-of/equiv Dequiv1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1 Dunmap1 Dequiv1 -> invert-tmap-cn-of' (Dof a da) (Dmap2 a x at) (Dunmap2 x a xt) (Dequiv2 a da)). - : invert-tmap-cn-of' (cn-of/app (Dof2 : cn-of C2 K1) (Dof1 : cn-of C1 (pi K1 K2))) (Dmap2 C2 M2 DmapC2) (Dunmap2 M2 C2' DunmapC2) (kd-equiv/trans (Dequiv2 C2' DofC2') Dequiv2s) <- can-tmap K1 (Dmap1 : tmap K1 A1) <- ({x} {a} {at} can-map a at -> can-tmap (K2 a) (Dmap2 a x at : tmap (K2 a) (A2 x))) <- invert-tmap-cn-of Dof1 (tmap/pi Dmap2 Dmap1) (tunmap/pi (Dunmap2 : {x} {a} unmap x a -> tunmap (A2 x) (K2' a)) (Dunmap1 : tunmap A1 K1')) (Dequiv : kd-equiv (pi K1 K2) (pi K1' K2')) <- injective-pi Dequiv (Dequiv1 : kd-equiv K1 K1') (Dequiv2 : {a} cn-of a K1 -> kd-equiv (K2 a) (K2' a)) <- can-map C2 (DmapC2 : map C2 M2) <- invert-map Dof2 DmapC2 (DunmapC2 : unmap M2 C2') (DequivC2 : cn-equiv C2 C2' K1) <- cn-of-reg Dof1 (kd-wf/pi (Dwf2 : {a} cn-of a K1 -> kd-wf (K2 a)) _) <- functionality-kd Dwf2 DequivC2 (Dequiv2s : kd-equiv (K2 C2) (K2 C2')) <- cn-equiv-reg DequivC2 _ (DofC2' : cn-of C2' K1) _. - : invert-tmap-cn-of' _ tmap/one tunmap/one kd-equiv/one. - : invert-tmap-cn-of' _ tmap/t tunmap/t kd-equiv/t. - : invert-tmap-cn-of' (cn-of/sing Dof) (tmap/sing Dmap) (tunmap/sing Dunmap) (kd-equiv/sing Dequiv) <- can-map _ Dmap <- invert-map Dof Dmap Dunmap Dequiv. - : invert-tmap-cn-of' (cn-of/extpi (Dof : {a} cn-of a K1 -> cn-of (app C a) (K2 a)) (DofPre : cn-of C (pi K1 K2p))) (tmap/pi DmapK2 DmapK1) (tunmap/pi DunmapA2 DunmapA1) (kd-equiv/pi DequivK2 DequivK1) <- can-tmap K1 (DmapK1 : tmap K1 A1) <- ({x} {a} {at:map a x} can-map a at -> can-tmap (K2p a) (DmapK2p a x at : tmap (K2p a) (A2p x))) <- invert-tmap-cn-of DofPre (tmap/pi DmapK2p DmapK1) (tunmap/pi (DunmapA2p : {x} {a} unmap x a -> tunmap (A2p x) (K2p' a)) (DunmapA1 : tunmap A1 K1')) (Dequiv : kd-equiv (pi K1 K2p) (pi K1' K2p')) <- injective-pi Dequiv (DequivK1 : kd-equiv K1 K1') _ <- cn-of-reg DofPre (kd-wf/pi _ (DwfK1 : kd-wf K1)) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> {x} {dx:evof x A1} {at} {xt} can-map a at -> map-of da at DmapK1 (eof/var DwfA1 dx) -> can-unmap x xt -> unmap-vof dx xt DunmapA1 (cn-of/equiv DequivK1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da DmapK1 DunmapA1 DequivK1 -> invert-tmap-cn-of' (Dof a da) (DmapK2 a x at : tmap (K2 a) (A2 x)) (DunmapA2 x a xt : tunmap (A2 x) (K2' a)) (DequivK2 a da : kd-equiv (K2 a) (K2' a))). - : invert-tmap-cn-of' (cn-of/extsigma Dwf2 _ Dof1) (tmap/sigma Dmap2 Dmap1) (tunmap/sigma Dunmap2 Dunmap1) (kd-equiv/sigma Dequiv2 Dequiv1) <- invert-tmap-cn-of' Dof1 Dmap1 Dunmap1 Dequiv1 <- cn-of-reg Dof1 Dwf1 <- map-wf' Dwf1 Dmap1 Dwf1' <- ({x} {a} {at:map a x} can-map a at -> can-tmap (K2 a) (Dmap2 a x at)) <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da Dwf1 -> {x} {dx:evof x A} {at} {xt} can-map a at -> map-of da at Dmap1 (eof/var Dwf1' dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1 (cn-of/equiv Dequiv1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1 Dunmap1 Dequiv1 -> invert-tmap (Dwf2 a da) (Dmap2 a x at) (Dunmap2 x a xt) (Dequiv2 a da)). - : invert-tmap-cn-of' (cn-of/subsume Dsub _) Dmap2 Dunmap2 Dequiv2 <- can-tmap _ Dmap1 <- can-tmap _ Dmap2 <- invert-tmap-kd-sub Dsub Dmap1 Dmap2 _ Dunmap2 _ Dequiv2. %%% - : invert-tmap-kd-sub (kd-sub/refl D) Dmap1 Dmap2 Dunmap1 Dunmap2 Dequiv1 Dequiv2 <- invert-tmap-kd-equiv D Dmap1 Dmap2 Dunmap1 Dunmap2 Dequiv1 Dequiv2. - : invert-tmap-kd-sub (kd-sub/trans D23 D12) Dmap1 Dmap3 Dunmap1 Dunmap3 Dequiv1 Dequiv3 <- can-tmap K2 Dmap2 <- invert-tmap-kd-sub D12 Dmap1 Dmap2 Dunmap1 _ Dequiv1 _ <- invert-tmap-kd-sub D23 Dmap2 Dmap3 _ Dunmap3 _ Dequiv3. - : invert-tmap-kd-sub (kd-sub/sing-t Dof) (tmap/sing Dmap) tmap/t (tunmap/sing Dunmap) tunmap/t (kd-equiv/sing Dequiv) kd-equiv/t <- invert-map Dof Dmap Dunmap Dequiv. - : invert-tmap-kd-sub (kd-sub/pi (Dwf2a : {a} cn-of a K1a -> kd-wf (K2a a)) (Dsub2 : {a} cn-of a K1b -> kd-sub (K2a a) (K2b a)) (Dsub1 : kd-sub K1b K1a)) (tmap/pi (Dmap2a : {a} {x} map a x -> tmap (K2a a) (A2a x)) (Dmap1a : tmap K1a A1a)) (tmap/pi (Dmap2b : {a} {x} map a x -> tmap (K2b a) (A2b x)) (Dmap1b : tmap K1b A1b)) %% (tunmap/pi Dunmap2a Dunmap1a) (tunmap/pi Dunmap2b Dunmap1b) (kd-equiv/pi Dequiv2a Dequiv1a) (kd-equiv/pi Dequiv2b Dequiv1b) <- invert-tmap-kd-sub Dsub1 Dmap1b Dmap1a (Dunmap1b : tunmap A1b K1b') (Dunmap1a : tunmap A1a K1a') Dequiv1b Dequiv1a <- kd-sub-reg Dsub1 (DwfK1b : kd-wf K1b) (DwfK1a : kd-wf K1a) <- map-wf' DwfK1b Dmap1b (DwfA1b : ewf A1b) <- ({a} {da:cn-of a K1b} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1b -> {x} {dx:evof x A1b} {at} {xt} can-map a at -> map-of da at Dmap1b (eof/var DwfA1b dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1b (cn-of/equiv Dequiv1b da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1b Dunmap1b Dequiv1b -> invert-tmap-kd-sub (Dsub2 a da) (Dmap2a a x at) (Dmap2b a x at) (Dunmap2aUseless x a xt) (Dunmap2b x a xt : tunmap (A2b x) (K2b' a)) (Dequiv2aUseless a da) (Dequiv2b a da)) <- map-wf' DwfK1a Dmap1a (DwfA1a : ewf A1a) <- ({a} {da:cn-of a K1a} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1a -> {x} {dx:evof x A1a} {at} {xt} can-map a at -> map-of da at Dmap1a (eof/var DwfA1a dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1a (cn-of/equiv Dequiv1a da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1a Dunmap1a Dequiv1a -> invert-tmap (Dwf2a a da) (Dmap2a a x at) (Dunmap2a x a xt : tunmap (A2a x) (K2a' a)) (Dequiv2a a da)). - : invert-tmap-kd-sub (kd-sub/sigma (Dwf2b : {a} cn-of a K1b -> kd-wf (K2b a)) (Dsub2 : {a} cn-of a K1a -> kd-sub (K2a a) (K2b a)) (Dsub1 : kd-sub K1a K1b)) (tmap/sigma (Dmap2a : {a} {x} map a x -> tmap (K2a a) (A2a x)) (Dmap1a : tmap K1a A1a)) (tmap/sigma (Dmap2b : {a} {x} map a x -> tmap (K2b a) (A2b x)) (Dmap1b : tmap K1b A1b)) %% (tunmap/sigma Dunmap2a Dunmap1a) (tunmap/sigma Dunmap2b Dunmap1b) (kd-equiv/sigma Dequiv2a Dequiv1a) (kd-equiv/sigma Dequiv2b Dequiv1b) <- invert-tmap-kd-sub Dsub1 Dmap1a Dmap1b (Dunmap1a : tunmap A1a K1a') (Dunmap1b : tunmap A1b K1b') Dequiv1a Dequiv1b <- kd-sub-reg Dsub1 (DwfK1a : kd-wf K1a) (DwfK1b : kd-wf K1b) <- map-wf' DwfK1a Dmap1a (DwfA1a : ewf A1a) <- ({a} {da:cn-of a K1a} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1a -> {x} {dx:evof x A1a} {at} {xt} can-map a at -> map-of da at Dmap1a (eof/var DwfA1a dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1a (cn-of/equiv Dequiv1a da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1a Dunmap1a Dequiv1a -> invert-tmap-kd-sub (Dsub2 a da) (Dmap2a a x at) (Dmap2b a x at) (Dunmap2a x a xt : tunmap (A2a x) (K2a' a)) (Dunmap2bUseless x a xt) (Dequiv2a a da) (Dequiv2bUseless a da)) <- map-wf' DwfK1b Dmap1b (DwfA1b : ewf A1b) <- ({a} {da:cn-of a K1b} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1b -> {x} {dx:evof x A1b} {at} {xt} can-map a at -> map-of da at Dmap1b (eof/var DwfA1b dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1b (cn-of/equiv Dequiv1b da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1b Dunmap1b Dequiv1b -> invert-tmap (Dwf2b a da) (Dmap2b a x at) (Dunmap2b x a xt : tunmap (A2b x) (K2b' a)) (Dequiv2b a da)). %%% - : invert-tmap-kd-equiv (kd-equiv/refl Dwf) Dmap1 Dmap2 Dunmap1 Dunmap2 Dequiv1 Dequiv2 %% Dmap1 and Dmap2 are the same, but it's easier to handle them as if they might not be. <- invert-tmap Dwf Dmap1 Dunmap1 Dequiv1 <- invert-tmap Dwf Dmap2 Dunmap2 Dequiv2. - : invert-tmap-kd-equiv (kd-equiv/symm D) Dmap1 Dmap2 Dunmap1 Dunmap2 Dequiv1 Dequiv2 <- invert-tmap-kd-equiv D Dmap2 Dmap1 Dunmap2 Dunmap1 Dequiv2 Dequiv1. - : invert-tmap-kd-equiv (kd-equiv/trans D23 D12) Dmap1 Dmap3 Dunmap1 Dunmap3 Dequiv1 Dequiv3 <- can-tmap K2 Dmap2 <- invert-tmap-kd-equiv D12 Dmap1 Dmap2 Dunmap1 _ Dequiv1 _ <- invert-tmap-kd-equiv D23 Dmap2 Dmap3 _ Dunmap3 _ Dequiv3. - : invert-tmap-kd-equiv (kd-equiv/sing Dequiv) (tmap/sing Dmap1) (tmap/sing Dmap2) (tunmap/sing Dunmap1) (tunmap/sing Dunmap2) (kd-equiv/sing Dequiv1) (kd-equiv/sing Dequiv2) <- invert-map-1 Dequiv Dmap1 Dunmap1 Dequiv1 <- invert-map-2 Dequiv Dmap2 Dunmap2 Dequiv2. - : invert-tmap-kd-equiv (kd-equiv/pi (Dequiv2 : {a} cn-of a K1a -> kd-equiv (K2a a) (K2b a)) (Dequiv1 : kd-equiv K1a K1b)) (tmap/pi (Dmap2a : {a} {x} map a x -> tmap (K2a a) (A2a x)) (Dmap1a : tmap K1a A1a)) (tmap/pi (Dmap2b : {a} {x} map a x -> tmap (K2b a) (A2b x)) (Dmap1b : tmap K1b A1b)) %% (tunmap/pi Dunmap2a Dunmap1a) (tunmap/pi Dunmap2b Dunmap1b) (kd-equiv/pi Dequiv2a Dequiv1a) (kd-equiv/pi ([a] [da] Dequiv2b a (cn-of/equiv (kd-equiv/symm Dequiv1) da)) Dequiv1b) <- invert-tmap-kd-equiv Dequiv1 Dmap1a Dmap1b (Dunmap1a : tunmap A1a K1a') (Dunmap1b : tunmap A1b K1b') (Dequiv1a : kd-equiv K1a K1a') (Dequiv1b : kd-equiv K1b K1b') <- kd-equiv-reg Dequiv1 (DwfK1a : kd-wf K1a) (DwfK1b : kd-wf K1b) <- map-wf' DwfK1a Dmap1a (DwfA1a : ewf A1a) <- ({a} {da:cn-of a K1a} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1a -> {x} {dx:evof x A1a} {at} {xt} can-map a at -> map-of da at Dmap1a (eof/var DwfA1a dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1a (cn-of/equiv Dequiv1a da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1a Dunmap1a Dequiv1a -> invert-tmap-kd-equiv (Dequiv2 a da) (Dmap2a a x at) (Dmap2b a x at) (Dunmap2a x a xt : tunmap (A2a x) (K2a' a)) (Dunmap2b x a xt : tunmap (A2b x) (K2b' a)) (Dequiv2a a da : kd-equiv (K2a a) (K2a' a)) (Dequiv2b a da : kd-equiv (K2b a) (K2b' a))). - : invert-tmap-kd-equiv (kd-equiv/sigma (Dequiv2 : {a} cn-of a K1a -> kd-equiv (K2a a) (K2b a)) (Dequiv1 : kd-equiv K1a K1b)) (tmap/sigma (Dmap2a : {a} {x} map a x -> tmap (K2a a) (A2a x)) (Dmap1a : tmap K1a A1a)) (tmap/sigma (Dmap2b : {a} {x} map a x -> tmap (K2b a) (A2b x)) (Dmap1b : tmap K1b A1b)) %% (tunmap/sigma Dunmap2a Dunmap1a) (tunmap/sigma Dunmap2b Dunmap1b) (kd-equiv/sigma Dequiv2a Dequiv1a) (kd-equiv/sigma ([a] [da] Dequiv2b a (cn-of/equiv (kd-equiv/symm Dequiv1) da)) Dequiv1b) <- invert-tmap-kd-equiv Dequiv1 Dmap1a Dmap1b (Dunmap1a : tunmap A1a K1a') (Dunmap1b : tunmap A1b K1b') (Dequiv1a : kd-equiv K1a K1a') (Dequiv1b : kd-equiv K1b K1b') <- kd-equiv-reg Dequiv1 (DwfK1a : kd-wf K1a) (DwfK1b : kd-wf K1b) <- map-wf' DwfK1a Dmap1a (DwfA1a : ewf A1a) <- ({a} {da:cn-of a K1a} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1a -> {x} {dx:evof x A1a} {at} {xt} can-map a at -> map-of da at Dmap1a (eof/var DwfA1a dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1a (cn-of/equiv Dequiv1a da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1a Dunmap1a Dequiv1a -> invert-tmap-kd-equiv (Dequiv2 a da) (Dmap2a a x at) (Dmap2b a x at) (Dunmap2a x a xt : tunmap (A2a x) (K2a' a)) (Dunmap2b x a xt : tunmap (A2b x) (K2b' a)) (Dequiv2a a da : kd-equiv (K2a a) (K2a' a)) (Dequiv2b a da : kd-equiv (K2b a) (K2b' a))). %%% - : invert-tmap-cn-of Dof Dmap Dunmap Dequiv <- invert-tmap-cn-of' Dof Dmap' Dunmap' Dequiv <- tmap-fun Dmap' Dmap Deq <- tunmap-resp Deq kind-eq/i Dunmap' Dunmap. - : invert-tmap-1 Dequiv Dmap1 Dunmap1 Dequiv1 <- can-tmap _ Dmap2 <- invert-tmap-kd-equiv Dequiv Dmap1 Dmap2 Dunmap1 Dunmap2 Dequiv1 Dequiv2. - : invert-tmap-2 Dequiv Dmap2 Dunmap2 Dequiv2 <- can-tmap _ Dmap1 <- invert-tmap-kd-equiv Dequiv Dmap1 Dmap2 Dunmap1 Dunmap2 Dequiv1 Dequiv2. - : invert-map-2 Dequiv Dmap Dunmap Dequiv' <- invert-map-2' Dmap Dequiv Dunmap Dequiv'. - : invert-tmap-cn-equiv Deqv Dmap Dunmap Dequiv <- invert-tmap-cn-equiv' Deqv Dmap' Dunmap' Dequiv <- tmap-fun Dmap' Dmap Deq <- tunmap-resp Deq kind-eq/i Dunmap' Dunmap. %%% -refl : invert-map-1 (cn-equiv/refl Dof) Dmap Dunmap Dequiv <- invert-map Dof Dmap Dunmap Dequiv. -symm : invert-map-1 (cn-equiv/symm Dequiv) Dmap Dunmap Dequiv' <- invert-map-2 Dequiv Dmap Dunmap Dequiv'. -trans : invert-map-1 (cn-equiv/trans _ D) Dmap Dunmap Dequiv <- invert-map-1 D Dmap Dunmap Dequiv. -app : invert-map-1 (cn-equiv/app Dof2 Dof1) (map/app D2 D1) (unmap/app D2' D1') (cn-equiv/app Dequiv2 Dequiv1) <- invert-map-1 Dof1 D1 D1' Dequiv1 <- invert-map-1 Dof2 D2 D2' Dequiv2. -pi1 : invert-map-1 (cn-equiv/pi1 Dof) (map/pi1 D) (unmap/pi1 D') (cn-equiv/pi1 Dequiv) <- invert-map-1 Dof D D' Dequiv. -pi2 : invert-map-1 (cn-equiv/pi2 Dof) (map/pi2 D) (unmap/pi2 D') (cn-equiv/pi2 Dequiv) <- invert-map-1 Dof D D' Dequiv. -lam : invert-map-1 (cn-equiv/lam Dof2 Dof1) (map/lam D2 D1) (unmap/lam D2' D1') (cn-equiv/lam Dequiv2 Dequiv1) <- invert-tmap-1 Dof1 D1 D1' Dequiv1 <- kd-equiv-reg Dequiv1 DwfK _ <- map-wf' DwfK D1 DwfA <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK -> {x} {dx:evof x A} {at} {xt} can-map a at -> map-of da at D1 (eof/var DwfA dx) -> can-unmap x xt -> unmap-vof dx xt D1' (cn-of/equiv Dequiv1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da D1 D1' Dequiv1 -> invert-map-1 (Dof2 a da) (D2 a x at) (D2' x a xt) (Dequiv2 a da)). -pair : invert-map-1 (cn-equiv/pair Dwf Dof2 Dof1) (map/pair D2 D1) (unmap/pair D2' D1') (cn-equiv/pair Dwf Dequiv2 Dequiv1) <- invert-map-1 Dof1 D1 D1' Dequiv1 <- invert-map-1 Dof2 D2 D2' Dequiv2. -sing : invert-map-1 (cn-equiv/sing Dof) D D' (cn-equiv/sing Dequiv) <- invert-map-1 Dof D D' Dequiv. -singel : invert-map-1 (cn-equiv/singelim Dof) Dmap Dunmap (cn-equiv/subsume (kd-sub/sing-t Dof') Dequiv) <- invert-map Dof Dmap Dunmap Dequiv <- cn-of-reg Dof (kd-wf/sing Dof'). -piext : invert-map-1 (cn-equiv/extpi (Dof : {a} cn-of a K1 -> cn-equiv (app C a) (app Cr a) (K2 a)) _ (DofPre : cn-of C (pi K1 K2p))) (DmapC : map C M) DunmapM (cn-equiv/extpi Dequiv2' DofPre' DofPre) <- invert-map DofPre DmapC (DunmapM : unmap M C') (DequivC : cn-equiv C C' (pi K1 K2p)) <- can-tmap K1 (DmapK1 : tmap K1 A1) <- ({x} {a} {at:map a x} can-map a at -> can-tmap (K2p a) (DmapK2p a x at : tmap (K2p a) (A2p x))) <- invert-tmap-cn-of DofPre (tmap/pi DmapK2p DmapK1) (tunmap/pi (DunmapA2 : {x} {a} unmap x a -> tunmap (A2p x) (K2p' a)) (DunmapA1 : tunmap A1 K1')) (DequivKpre : kd-equiv (pi K1 K2p) (pi K1' K2p')) <- injective-pi DequivKpre (DequivK1 : kd-equiv K1 K1') _ <- cn-of-reg DofPre (kd-wf/pi _ (DwfK1 : kd-wf K1)) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> {x} {dx:evof x A1} {at} {xt} can-map a at -> map-of da at DmapK1 (eof/var DwfA1 dx) -> can-unmap x xt -> unmap-vof dx xt DunmapA1 (cn-of/equiv DequivK1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da DmapK1 DunmapA1 DequivK1 -> invert-map-1 (Dof a da) (map/app at DmapC) (unmap/app xt (DunmapM' x a xt : unmap M (C'' a))) (Dequiv2 a da : cn-equiv (app C a) (app (C'' a) a) (K2 a))) <- ({a} {x} {xt:unmap x a} unmap-fun (DunmapM' x a xt) DunmapM (Deq a : con-eq (C'' a) C')) <- ({a} con-resp-con ([b] app b a) (Deq a) (Deq' a : con-eq (app (C'' a) a) (app C' a))) <- ({a} {d:cn-of a K1} cn-equiv-resp con-eq/i (Deq' a) kind-eq/i (Dequiv2 a d) (Dequiv2' a d : cn-equiv (app C a) (app C' a) (K2 a))) <- cn-equiv-reg DequivC _ (DofPre' : cn-of C' (pi K1 K2p)) _. -piext : invert-map-1 (cn-equiv/extpiw (Dof : {a} cn-of a K1 -> cn-equiv (app C a) (app Cr a) (K2 a)) (DeqvPre : cn-equiv C Cr (pi K1 K2p))) (DmapC : map C M) DunmapM (cn-equiv/extpi Dequiv2' DofPre' DofPre) <- cn-equiv-reg DeqvPre (DofPre : cn-of C (pi K1 K2p)) _ _ <- invert-map-1 DeqvPre DmapC (DunmapM : unmap M C') (DequivC : cn-equiv C C' (pi K1 K2p)) <- invert-tmap-cn-equiv' DeqvPre (tmap/pi (DmapK2p : {a} {x} map a x -> tmap (K2p a) (A2p x)) (DmapK1 : tmap K1 A1)) (tunmap/pi (DunmapA2 : {x} {a} unmap x a -> tunmap (A2p x) (K2p' a)) (DunmapA1 : tunmap A1 K1')) (DequivKpre : kd-equiv (pi K1 K2p) (pi K1' K2p')) <- injective-pi DequivKpre (DequivK1 : kd-equiv K1 K1') _ <- cn-of-reg DofPre (kd-wf/pi _ (DwfK1 : kd-wf K1)) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> {x} {dx:evof x A1} {at} {xt} can-map a at -> map-of da at DmapK1 (eof/var DwfA1 dx) -> can-unmap x xt -> unmap-vof dx xt DunmapA1 (cn-of/equiv DequivK1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da DmapK1 DunmapA1 DequivK1 -> invert-map-1 (Dof a da) (map/app at DmapC) (unmap/app xt (DunmapM' x a xt : unmap M (C'' a))) (Dequiv2 a da : cn-equiv (app C a) (app (C'' a) a) (K2 a))) <- ({a} {x} {xt:unmap x a} unmap-fun (DunmapM' x a xt) DunmapM (Deq a : con-eq (C'' a) C')) <- ({a} con-resp-con ([b] app b a) (Deq a) (Deq' a : con-eq (app (C'' a) a) (app C' a))) <- ({a} {d:cn-of a K1} cn-equiv-resp con-eq/i (Deq' a) kind-eq/i (Dequiv2 a d) (Dequiv2' a d : cn-equiv (app C a) (app C' a) (K2 a))) <- cn-equiv-reg DequivC _ (DofPre' : cn-of C' (pi K1 K2p)) _. -sigext : invert-map-1 (cn-equiv/extsigma Dwf Dof2 Dof1) D D' (cn-equiv/extsigma Dwf Dequiv2' Dequiv1) <- invert-map-1 Dof1 (map/pi1 D) (unmap/pi1 D') Dequiv1 <- invert-map-1 Dof2 (map/pi2 D) (unmap/pi2 D'') Dequiv2 <- unmap-fun D'' D' Deq <- con-resp-con pi2 Deq Deq' <- cn-equiv-resp con-eq/i Deq' kind-eq/i Dequiv2 Dequiv2'. -one : invert-map-1 (cn-equiv/one _ Dof) Dmap Dunmap Dequiv <- invert-map Dof Dmap Dunmap Dequiv. -sub : invert-map-1 (cn-equiv/subsume Dsub Dof) D D' (cn-equiv/subsume Dsub Dequiv) <- invert-map-1 Dof D D' Dequiv. -ref : invert-map-1 (cn-equiv/ref Deqv) (map/ref D) (unmap/app D' unmap/ref) (cn-equiv/trans (cn-equiv/app Dequiv (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/ref d) kd-wf/t))) (cn-equiv/symm (cn-equiv/beta Dof ([a] [e] cn-of/ref e)))) <- invert-map-1 Deqv D D' Dequiv <- cn-equiv-reg Deqv Dof _ _. -tag : invert-map-1 (cn-equiv/tag Deqv) (map/tag D) (unmap/app D' unmap/tag) (cn-equiv/trans (cn-equiv/app Dequiv (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/tag d) kd-wf/t))) (cn-equiv/symm (cn-equiv/beta Dof ([a] [e] cn-of/tag e)))) <- invert-map-1 Deqv D D' Dequiv <- cn-equiv-reg Deqv Dof _ _. -lab : invert-map-1 (cn-equiv/labeled Deqv) (map/labeled D) (unmap/app D' unmap/labeled) (cn-equiv/trans (cn-equiv/app Dequiv (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/labeled d : cn-of (labeled I _) _) kd-wf/t))) (cn-equiv/symm (cn-equiv/beta Dof ([a] [e] cn-of/labeled e)))) <- invert-map-1 Deqv D D' Dequiv <- cn-equiv-reg Deqv Dof _ _. -arrow : invert-map-1 (cn-equiv/arrow Deqv2 Deqv1) (map/arrow D2 D1) (unmap/app D2' (unmap/app D1' unmap/arrow)) (cn-equiv/trans (cn-equiv/app Dequiv2 (cn-equiv/app Dequiv1 (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/lam ([b] [e] cn-of/arrow e d) kd-wf/t) kd-wf/t)))) (cn-equiv/symm (cn-equiv/trans (cn-equiv/beta Dof2 ([b] [e] cn-of/arrow e Dof1)) (cn-equiv/app (cn-equiv/refl Dof2) (cn-equiv/beta Dof1 ([a] [d] cn-of/lam ([b] [e] cn-of/arrow e d) kd-wf/t)))))) <- invert-map-1 Deqv1 D1 D1' Dequiv1 <- invert-map-1 Deqv2 D2 D2' Dequiv2 <- cn-equiv-reg Deqv1 Dof1 _ _ <- cn-equiv-reg Deqv2 Dof2 _ _. -prod : invert-map-1 (cn-equiv/prod Deqv2 Deqv1) (map/prod D2 D1) (unmap/app D2' (unmap/app D1' unmap/prod)) (cn-equiv/trans (cn-equiv/app Dequiv2 (cn-equiv/app Dequiv1 (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/lam ([b] [e] cn-of/prod e d) kd-wf/t) kd-wf/t)))) (cn-equiv/symm (cn-equiv/trans (cn-equiv/beta Dof2 ([b] [e] cn-of/prod e Dof1)) (cn-equiv/app (cn-equiv/refl Dof2) (cn-equiv/beta Dof1 ([a] [d] cn-of/lam ([b] [e] cn-of/prod e d) kd-wf/t)))))) <- invert-map-1 Deqv1 D1 D1' Dequiv1 <- invert-map-1 Deqv2 D2 D2' Dequiv2 <- cn-equiv-reg Deqv1 Dof1 _ _ <- cn-equiv-reg Deqv2 Dof2 _ _. -plus : invert-map-1 (cn-equiv/plus Deqv2 Deqv1) (map/plus D2 D1) (unmap/app D2' (unmap/app D1' unmap/plus)) (cn-equiv/trans (cn-equiv/app Dequiv2 (cn-equiv/app Dequiv1 (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/lam ([b] [e] cn-of/plus e d) kd-wf/t) kd-wf/t)))) (cn-equiv/symm (cn-equiv/trans (cn-equiv/beta Dof2 ([b] [e] cn-of/plus e Dof1)) (cn-equiv/app (cn-equiv/refl Dof2) (cn-equiv/beta Dof1 ([a] [d] cn-of/lam ([b] [e] cn-of/plus e d) kd-wf/t)))))) <- invert-map-1 Deqv1 D1 D1' Dequiv1 <- invert-map-1 Deqv2 D2 D2' Dequiv2 <- cn-equiv-reg Deqv1 Dof1 _ _ <- cn-equiv-reg Deqv2 Dof2 _ _. -rec : invert-map-1 (cn-equiv/rec (DeqvC2 : cn-equiv C2 C2r K) (DeqvC1 : {a} cn-of a (pi K ([_] t)) -> {b} cn-of b K -> cn-equiv (C1 a b) (C1r a b) t) (DeqvK : kd-equiv K Kr)) (map/rec (Dflay : flay A SK MA) (DmapC2 : map C2 M2) (DmapC1 : {a} {x} map a x -> {b} {y} map b y -> map (C1 a b) (M1 x y)) (DmapK : tmap K A)) %% (unmap/app (unmap/pair (unmap/pair DmapM2 (unmap/lam ([x] [a] [xt] unmap/lam ([y] [b] [yt] DmapM1 x a xt y b yt) DmapA) (tunmap/pi ([_] [_] [_] tunmap/t) DmapA))) DmapMA) (unmap/rec Dskof')) (cn-equiv/symm (cn-equiv/trans (cn-equiv/symm (cn-equiv/rec (cn-equiv/symm (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm DequivC2) (cn-equiv/beta2 DofC2' (cn-of/lam ([a] [d] cn-of/lam ([b] [e] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) (cn-equiv/pi2-nd (cn-equiv/beta2 (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/lam ([a] [d] cn-of/lam ([b] [e] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK'))) DofCK)))) ([a] [d] [b] [e] cn-equiv/symm (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm (DequivC1 a d b e)) (cn-equiv/beta-nd (cn-of/equiv DequivK e) ([b] [e] DofC1' a d b (cn-of/equiv (kd-equiv/symm DequivK) e)))) (cn-equiv/app-nd (cn-equiv/refl e) (cn-equiv/trans (cn-equiv/beta-nd (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK) d) ([a] [d:cn-of a (pi K' ([_] t))] cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK'))) (cn-equiv/app-nd (cn-equiv/refl d) (cn-equiv/trans (cn-equiv/beta1 DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) (cn-equiv/pi1 (cn-equiv/beta2 (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) DofCK)))))))) (kd-equiv/trans (kd-equiv/trans DequivJCK DequivK'JCK) DequivK))) (cn-equiv/beta-nd (cn-of/pair ([a] [d] kd-wf/sigma ([_] [_] DwfJ a d) (kd-wf/pi ([_] [_] kd-wf/pi ([_] [_] kd-wf/t) (DwfJ a d)) (kd-wf/pi ([_] [_] kd-wf/t) (DwfJ a d)))) (cn-of/equiv (kd-equiv/sigma ([_] [_] kd-equiv/trans DequivK'JCK DequivK) (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/trans DequivK'JCK DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/trans DequivK'JCK DequivK)))) (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK'))))) DofCK) ([c] [f] cn-of/rec (cn-of/pi2 (cn-of/pi2 f)) ([a] [d] [b] [e] cn-of/app e (cn-of/app d (cn-of/pi1 (cn-of/pi2 f)))) (DwfJ _ (cn-of/pi1 f)))))) <- kd-equiv-reg DeqvK (DwfK : kd-wf K) _ <- invert-tmap-1 DeqvK DmapK (DmapA : tunmap A K') (DequivK : kd-equiv K K') <- map-wf' DwfK DmapK (DwfA : ewf A) <- ({a} {da:cn-of a (pi K ([_] t))} {das:cn-assm da} mcn-assm da das -> cn-of-reg da (kd-wf/pi ([_] [_] kd-wf/t) DwfK) -> {x} {dx:evof x (epi A ([_] et))} {at} {xt} can-map a at -> map-of da at (tmap/pi ([_] [_] [_] tmap/t) DmapK) (eof/var (ewf/pi ([_] [_] ewf/t) DwfA) dx) -> can-unmap x xt -> unmap-vof dx xt (tunmap/pi ([_] [_] [_] tunmap/t) DmapA) (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK) da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da (tmap/pi ([_] [_] [_] tmap/t) DmapK) (tunmap/pi ([_] [_] [_] tunmap/t) DmapA) (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK) -> {b} {db:cn-of b K} {dbs} mcn-assm db dbs -> cn-of-reg db DwfK -> {y} {dy:evof y A} {bt} {yt} can-map b bt -> map-of db bt DmapK (eof/var DwfA dy) -> can-unmap y yt -> unmap-vof dy yt DmapA (cn-of/equiv DequivK db) -> invert-map db bt yt (cn-equiv/refl db) -> invert-tmap-cn-of' db DmapK DmapA DequivK -> invert-map-1 (DeqvC1 a da b db) (DmapC1 a x at b y bt) (DmapM1 x a xt y b yt : unmap (M1 x y) (C1' a b)) (DequivC1 a da b db : cn-equiv (C1 a b) (C1' a b) t)) <- invert-map-1 DeqvC2 DmapC2 (DmapM2 : unmap M2 C2') (DequivC2 : cn-equiv C2 C2' K) <- can-skof SK (Dskof : skof SK D E) <- flay-sound DwfA Dflay Dskof (DofMA : eof MA D) (DequivAE : tequiv A (E MA)) <- unmap-skof Dskof (DmapD : tunmap D I) (DmapE : {x} {a} unmap x a -> tunmap (E x) (J a)) (Dskof' : skof-il SK I J) <- can-unmap MA (DmapMA : unmap MA CK) <- cn-equiv-reg DequivC2 _ (DofC2' : cn-of C2' K) _ <- kd-equiv-reg DequivK _ (DwfK' : kd-wf K') <- ({a} {da} {das} mcn-assm da das -> cn-of-reg da (kd-wf/pi ([_] [_] kd-wf/t) DwfK) -> {b} {db} {dbs} mcn-assm db dbs -> cn-of-reg db DwfK -> cn-equiv-reg (DequivC1 a da b db) (DDDD1 a da b db) (DofC1' a da b db : cn-of (C1' a b) t) (DDDD2 a da b db)) <- unmap-of' DofMA DmapMA DmapD (DofCK : cn-of CK I) <- unmap-tequiv DequivAE DmapA (DmapE _ _ DmapMA) (DequivK'JCK : kd-equiv K' (J CK)) <- skof-il-reg Dskof' _ (DwfJ : {a} cn-of a I -> kd-wf (J a)) <- functionality-kd DwfJ (cn-equiv/symm (cn-equiv/beta1 (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) DofCK) : cn-equiv CK (pi1 (pair CK _)) I) (DequivJCK : kd-equiv (J CK) (J (pi1 (pair CK _)))). - : invert-map-1 (cn-equiv/beta (Dof1 : cn-of C1 K1) (Dof2 : {a} cn-of a K1 -> cn-of (C2 a) (K2 a))) (map/app (DmapC1 : map C1 M1) (map/lam (DmapC2 : {a} {x} map a x -> map (C2 a) (M2 x)) (DmapK1 : tmap K1 A1))) (unmap/app DunmapM1 (unmap/lam DunmapM2 DunmapA1)) (cn-equiv/app Dequiv1 (cn-equiv/lam Dequiv2 DequivK1)) <- invert-map Dof1 DmapC1 (DunmapM1 : unmap M1 C1') (Dequiv1 : cn-equiv C1 C1' K1) <- invert-tmap-cn-of Dof1 DmapK1 (DunmapA1 : tunmap A1 K1') (DequivK1 : kd-equiv K1 K1') <- cn-of-reg Dof1 (DwfK1 : kd-wf K1) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> {x} {dx:evof x A1} {at} {xt} can-map a at -> map-of da at DmapK1 (eof/var DwfA1 dx) -> can-unmap x xt -> unmap-vof dx xt DunmapA1 (cn-of/equiv DequivK1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da DmapK1 DunmapA1 DequivK1 -> invert-map (Dof2 a da) (DmapC2 a x at) (DunmapM2 x a xt : unmap (M2 x) (C2' a)) (Dequiv2 a da : cn-equiv (C2 a) (C2' a) (K2 a))). - : invert-map-1 (cn-equiv/beta1 (Dof2 : cn-of C2 K2) (Dof1 : cn-of C1 K1)) (map/pi1 (map/pair (Dmap2 : map C2 M2) (Dmap1 : map C1 M1))) (unmap/pi1 (unmap/pair Dunmap2 Dunmap1)) (cn-equiv/pi1 (cn-equiv/pair ([_] [_] DwfK2) Dequiv2 Dequiv1)) <- invert-map Dof1 Dmap1 Dunmap1 Dequiv1 <- invert-map Dof2 Dmap2 Dunmap2 Dequiv2 <- cn-of-reg Dof2 (DwfK2 : kd-wf K2). - : invert-map-1 (cn-equiv/beta2 (Dof2 : cn-of C2 K2) (Dof1 : cn-of C1 K1)) (map/pi2 (map/pair (Dmap2 : map C2 M2) (Dmap1 : map C1 M1))) (unmap/pi2 (unmap/pair Dunmap2 Dunmap1)) (cn-equiv/pi2 (cn-equiv/pair ([_] [_] DwfK2) Dequiv2 Dequiv1)) <- invert-map Dof1 Dmap1 Dunmap1 Dequiv1 <- invert-map Dof2 Dmap2 Dunmap2 Dequiv2 <- cn-of-reg Dof2 (DwfK2 : kd-wf K2). %%% -refl : invert-map-2' Dmap (cn-equiv/refl Dof) Dunmap Dequiv <- invert-map Dof Dmap Dunmap Dequiv. -symm : invert-map-2' Dmap (cn-equiv/symm Dequiv) Dunmap Dequiv' <- invert-map-1 Dequiv Dmap Dunmap Dequiv'. -trans : invert-map-2' Dmap (cn-equiv/trans D _) Dunmap Dequiv <- invert-map-2 D Dmap Dunmap Dequiv. -app : invert-map-2' (map/app D2 D1) (cn-equiv/app Deqv2 Deqv1) (unmap/app D2' D1') (cn-equiv/equiv DequivSub (cn-equiv/app Dequiv2 Dequiv1)) <- invert-map-2 Deqv1 D1 D1' Dequiv1 <- invert-map-2 Deqv2 D2 D2' Dequiv2 <- cn-equiv-reg Deqv1 _ _ (kd-wf/pi DwfK2 DwfK1) <- functionality-kd DwfK2 (cn-equiv/symm Deqv2) DequivSub. -pi1 : invert-map-2' (map/pi1 D) (cn-equiv/pi1 Dof) (unmap/pi1 D') (cn-equiv/pi1 Dequiv) <- invert-map-2 Dof D D' Dequiv. -pi2 : invert-map-2' (map/pi2 D) (cn-equiv/pi2 Deqv) (unmap/pi2 D') (cn-equiv/equiv DequivSub (cn-equiv/pi2 Dequiv)) <- invert-map-2 Deqv D D' Dequiv <- cn-equiv-reg Deqv _ _ (kd-wf/sigma DwfK2 DwfK1) <- functionality-kd DwfK2 (cn-equiv/symm (cn-equiv/pi1 Deqv)) DequivSub. -lam : invert-map-2' (map/lam Dmap2 Dmap1) (cn-equiv/lam Deqv2 (Deqv1 : kd-equiv Kl K)) (unmap/lam Dunmap2 Dunmap1) (cn-equiv/equiv (kd-equiv/symm (kd-equiv/pi ([a] [d] kd-equiv/refl (Dwf2 a d)) Deqv1)) (cn-equiv/lam ([a] [d] Dequiv2 a (cn-of/equiv (kd-equiv/symm Deqv1) d)) Dequiv1)) <- can-tmap Kl Dmap1l <- invert-tmap-kd-equiv Deqv1 Dmap1l Dmap1 Dunmap1l Dunmap1 (Dequiv1l : kd-equiv Kl Kl') (Dequiv1 : kd-equiv K K') <- kd-equiv-reg Dequiv1l DwfKl _ <- map-wf' DwfKl Dmap1l DwfAl <- ({a} {da:cn-of a Kl} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfKl -> {x} {dx:evof x Al} {at} {xt} can-map a at -> map-of da at Dmap1l (eof/var DwfAl dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1l (cn-of/equiv Dequiv1l da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1l Dunmap1l Dequiv1l -> invert-map-2 (Deqv2 a da) (Dmap2 a x at) (Dunmap2 x a xt) (Dequiv2 a da)) <- ({a} {da:cn-of a Kl} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfKl -> cn-equiv-reg (Deqv2 a da) (Duseless1 a da) (Duseless2 a da) (Dwf2 a da : kd-wf (K2 a))). -pair : invert-map-2' (map/pair D2 D1) (cn-equiv/pair Dwf Deqv2 Deqv1) (unmap/pair D2' D1') (cn-equiv/pair Dwf (cn-equiv/equiv DequivSub Dequiv2) Dequiv1) <- invert-map-2 Deqv1 D1 D1' Dequiv1 <- invert-map-2 Deqv2 D2 D2' Dequiv2 <- functionality-kd Dwf Deqv1 DequivSub. -sing : invert-map-2' D (cn-equiv/sing Deqv) D' (cn-equiv/equiv (kd-equiv/sing (cn-equiv/symm Deqv)) (cn-equiv/sing Dequiv)) <- invert-map-2 Deqv D D' Dequiv. -singel : invert-map-2' Dmap (cn-equiv/singelim Dof) Dunmap Dequiv' <- invert-tmap-cn-of Dof (tmap/sing Dmap) (tunmap/sing Dunmap) Dequiv <- injective-sing Dequiv Dequiv'. -piext : invert-map-2' (DmapC : map C M) (cn-equiv/extpi (Deqv : {a} cn-of a K1 -> cn-equiv (app Cl a) (app C a) (K2 a)) (DofPre : cn-of C (pi K1 K2p)) _) DunmapM (cn-equiv/extpi Dequiv2' DofPre' DofPre) <- invert-map DofPre DmapC (DunmapM : unmap M C') (DequivC : cn-equiv C C' (pi K1 K2p)) <- can-tmap K1 (DmapK1 : tmap K1 A1) <- ({x} {a} {at:map a x} can-map a at -> can-tmap (K2p a) (DmapK2p a x at : tmap (K2p a) (A2p x))) <- invert-tmap-cn-of DofPre (tmap/pi DmapK2p DmapK1) (tunmap/pi (DunmapA2 : {x} {a} unmap x a -> tunmap (A2p x) (K2p' a)) (DunmapA1 : tunmap A1 K1')) (DequivKpre : kd-equiv (pi K1 K2p) (pi K1' K2p')) <- injective-pi DequivKpre (DequivK1 : kd-equiv K1 K1') _ <- cn-of-reg DofPre (kd-wf/pi _ (DwfK1 : kd-wf K1)) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> {x} {dx:evof x A1} {at} {xt} can-map a at -> map-of da at DmapK1 (eof/var DwfA1 dx) -> can-unmap x xt -> unmap-vof dx xt DunmapA1 (cn-of/equiv DequivK1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da DmapK1 DunmapA1 DequivK1 -> invert-map-2 (Deqv a da) (map/app at DmapC) (unmap/app xt (DunmapM' x a xt : unmap M (C'' a))) (Dequiv2 a da : cn-equiv (app C a) (app (C'' a) a) (K2 a))) <- ({a} {x} {xt:unmap x a} unmap-fun (DunmapM' x a xt) DunmapM (Deq a : con-eq (C'' a) C')) <- ({a} con-resp-con ([b] app b a) (Deq a) (Deq' a : con-eq (app (C'' a) a) (app C' a))) <- ({a} {d:cn-of a K1} cn-equiv-resp con-eq/i (Deq' a) kind-eq/i (Dequiv2 a d) (Dequiv2' a d : cn-equiv (app C a) (app C' a) (K2 a))) <- cn-equiv-reg DequivC _ (DofPre' : cn-of C' (pi K1 K2p)) _. -piext : invert-map-2' (DmapC : map C M) (cn-equiv/extpiw (Deqv : {a} cn-of a K1 -> cn-equiv (app Cr a) (app C a) (K2 a)) (DeqvPre : cn-equiv Cr C (pi K1 K2p))) DunmapM (cn-equiv/extpi Dequiv2' DofPre' DofPre) <- cn-equiv-reg DeqvPre _ (DofPre : cn-of C (pi K1 K2p)) _ <- invert-map-2 DeqvPre DmapC (DunmapM : unmap M C') (DequivC : cn-equiv C C' (pi K1 K2p)) <- invert-tmap-cn-equiv' DeqvPre (tmap/pi (DmapK2p : {a} {x} map a x -> tmap (K2p a) (A2p x)) (DmapK1 : tmap K1 A1)) (tunmap/pi (DunmapA2 : {x} {a} unmap x a -> tunmap (A2p x) (K2p' a)) (DunmapA1 : tunmap A1 K1')) (DequivKpre : kd-equiv (pi K1 K2p) (pi K1' K2p')) <- injective-pi DequivKpre (DequivK1 : kd-equiv K1 K1') _ <- cn-of-reg DofPre (kd-wf/pi _ (DwfK1 : kd-wf K1)) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> {x} {dx:evof x A1} {at} {xt} can-map a at -> map-of da at DmapK1 (eof/var DwfA1 dx) -> can-unmap x xt -> unmap-vof dx xt DunmapA1 (cn-of/equiv DequivK1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da DmapK1 DunmapA1 DequivK1 -> invert-map-2 (Deqv a da) (map/app at DmapC) (unmap/app xt (DunmapM' x a xt : unmap M (C'' a))) (Dequiv2 a da : cn-equiv (app C a) (app (C'' a) a) (K2 a))) <- ({a} {x} {xt:unmap x a} unmap-fun (DunmapM' x a xt) DunmapM (Deq a : con-eq (C'' a) C')) <- ({a} con-resp-con ([b] app b a) (Deq a) (Deq' a : con-eq (app (C'' a) a) (app C' a))) <- ({a} {d:cn-of a K1} cn-equiv-resp con-eq/i (Deq' a) kind-eq/i (Dequiv2 a d) (Dequiv2' a d : cn-equiv (app C a) (app C' a) (K2 a))) <- cn-equiv-reg DequivC _ (DofPre' : cn-of C' (pi K1 K2p)) _. -sigext : invert-map-2' D (cn-equiv/extsigma Dwf Deqv2 Deqv1) D' (cn-equiv/extsigma Dwf (cn-equiv/equiv DequivSub Dequiv2') Dequiv1) <- invert-map-2 Deqv1 (map/pi1 D) (unmap/pi1 D') Dequiv1 <- invert-map-2 Deqv2 (map/pi2 D) (unmap/pi2 D'') Dequiv2 <- unmap-fun D'' D' Deq <- con-resp-con pi2 Deq Deq' <- cn-equiv-resp con-eq/i Deq' kind-eq/i Dequiv2 Dequiv2' <- functionality-kd Dwf Deqv1 DequivSub. -one : invert-map-2' Dmap (cn-equiv/one Dof _) Dunmap Dequiv <- invert-map Dof Dmap Dunmap Dequiv. -sub : invert-map-2' D (cn-equiv/subsume Dsub Dof) D' (cn-equiv/subsume Dsub Dequiv) <- invert-map-2 Dof D D' Dequiv. -ref : invert-map-2' (map/ref D) (cn-equiv/ref Deqv) (unmap/app D' unmap/ref) (cn-equiv/trans (cn-equiv/app Dequiv (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/ref d) kd-wf/t))) (cn-equiv/symm (cn-equiv/beta Dof ([a] [e] cn-of/ref e)))) <- invert-map-2 Deqv D D' Dequiv <- cn-equiv-reg Deqv _ Dof _. -tag : invert-map-2' (map/tag D) (cn-equiv/tag Deqv) (unmap/app D' unmap/tag) (cn-equiv/trans (cn-equiv/app Dequiv (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/tag d) kd-wf/t))) (cn-equiv/symm (cn-equiv/beta Dof ([a] [e] cn-of/tag e)))) <- invert-map-2 Deqv D D' Dequiv <- cn-equiv-reg Deqv _ Dof _. -lab : invert-map-2' (map/labeled D) (cn-equiv/labeled Deqv) (unmap/app D' unmap/labeled) (cn-equiv/trans (cn-equiv/app Dequiv (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/labeled d : cn-of (labeled I _) _) kd-wf/t))) (cn-equiv/symm (cn-equiv/beta Dof ([a] [e] cn-of/labeled e)))) <- invert-map-2 Deqv D D' Dequiv <- cn-equiv-reg Deqv _ Dof _. -arrow : invert-map-2' (map/arrow D2 D1) (cn-equiv/arrow Deqv2 Deqv1) (unmap/app D2' (unmap/app D1' unmap/arrow)) (cn-equiv/trans (cn-equiv/app Dequiv2 (cn-equiv/app Dequiv1 (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/lam ([b] [e] cn-of/arrow e d) kd-wf/t) kd-wf/t)))) (cn-equiv/symm (cn-equiv/trans (cn-equiv/beta Dof2 ([b] [e] cn-of/arrow e Dof1)) (cn-equiv/app (cn-equiv/refl Dof2) (cn-equiv/beta Dof1 ([a] [d] cn-of/lam ([b] [e] cn-of/arrow e d) kd-wf/t)))))) <- invert-map-2 Deqv1 D1 D1' Dequiv1 <- invert-map-2 Deqv2 D2 D2' Dequiv2 <- cn-equiv-reg Deqv1 _ Dof1 _ <- cn-equiv-reg Deqv2 _ Dof2 _. -prod : invert-map-2' (map/prod D2 D1) (cn-equiv/prod Deqv2 Deqv1) (unmap/app D2' (unmap/app D1' unmap/prod)) (cn-equiv/trans (cn-equiv/app Dequiv2 (cn-equiv/app Dequiv1 (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/lam ([b] [e] cn-of/prod e d) kd-wf/t) kd-wf/t)))) (cn-equiv/symm (cn-equiv/trans (cn-equiv/beta Dof2 ([b] [e] cn-of/prod e Dof1)) (cn-equiv/app (cn-equiv/refl Dof2) (cn-equiv/beta Dof1 ([a] [d] cn-of/lam ([b] [e] cn-of/prod e d) kd-wf/t)))))) <- invert-map-2 Deqv1 D1 D1' Dequiv1 <- invert-map-2 Deqv2 D2 D2' Dequiv2 <- cn-equiv-reg Deqv1 _ Dof1 _ <- cn-equiv-reg Deqv2 _ Dof2 _. -plus : invert-map-2' (map/plus D2 D1) (cn-equiv/plus Deqv2 Deqv1) (unmap/app D2' (unmap/app D1' unmap/plus)) (cn-equiv/trans (cn-equiv/app Dequiv2 (cn-equiv/app Dequiv1 (cn-equiv/refl (cn-of/lam ([a] [d] cn-of/lam ([b] [e] cn-of/plus e d) kd-wf/t) kd-wf/t)))) (cn-equiv/symm (cn-equiv/trans (cn-equiv/beta Dof2 ([b] [e] cn-of/plus e Dof1)) (cn-equiv/app (cn-equiv/refl Dof2) (cn-equiv/beta Dof1 ([a] [d] cn-of/lam ([b] [e] cn-of/plus e d) kd-wf/t)))))) <- invert-map-2 Deqv1 D1 D1' Dequiv1 <- invert-map-2 Deqv2 D2 D2' Dequiv2 <- cn-equiv-reg Deqv1 _ Dof1 _ <- cn-equiv-reg Deqv2 _ Dof2 _. -rec : invert-map-2' (map/rec (Dflay : flay A SK MA) (DmapC2 : map C2 M2) (DmapC1 : {a} {x} map a x -> {b} {y} map b y -> map (C1 a b) (M1 x y)) (DmapK : tmap K A)) (cn-equiv/rec (DeqvC2 : cn-equiv C2r C2 Kr) (DeqvC1 : {a} cn-of a (pi Kr ([_] t)) -> {b} cn-of b Kr -> cn-equiv (C1r a b) (C1 a b) t) (DeqvK : kd-equiv Kr K)) %% (unmap/app (unmap/pair (unmap/pair DmapM2 (unmap/lam ([x] [a] [xt] unmap/lam ([y] [b] [yt] DmapM1 x a xt y b yt) DmapA) (tunmap/pi ([_] [_] [_] tunmap/t) DmapA))) DmapMA) (unmap/rec Dskof')) (cn-equiv/symm (cn-equiv/trans (cn-equiv/symm (cn-equiv/rec (cn-equiv/symm (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm (cn-equiv/equiv DeqvK DequivC2)) (cn-equiv/beta2 DofC2' (cn-of/lam ([a] [d] cn-of/lam ([b] [e] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) (cn-equiv/pi2-nd (cn-equiv/beta2 (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/lam ([a] [d] cn-of/lam ([b] [e] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK'))) DofCK)))) ([a] [d] [b] [e] cn-equiv/symm (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm (DequivC1 a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DeqvK)) d) b (cn-of/equiv (kd-equiv/symm DeqvK) e))) (cn-equiv/beta-nd (cn-of/equiv DequivK e) ([b] [e] DofC1' a d b (cn-of/equiv (kd-equiv/symm DequivK) e)))) (cn-equiv/app-nd (cn-equiv/refl e) (cn-equiv/trans (cn-equiv/beta-nd (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK) d) ([a] [d:cn-of a (pi K' ([_] t))] cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK'))) (cn-equiv/app-nd (cn-equiv/refl d) (cn-equiv/trans (cn-equiv/beta1 DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) (cn-equiv/pi1 (cn-equiv/beta2 (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) DofCK)))))))) (kd-equiv/trans (kd-equiv/trans DequivJCK DequivK'JCK) DequivK))) (cn-equiv/beta-nd (cn-of/pair ([a] [d] kd-wf/sigma ([_] [_] DwfJ a d) (kd-wf/pi ([_] [_] kd-wf/pi ([_] [_] kd-wf/t) (DwfJ a d)) (kd-wf/pi ([_] [_] kd-wf/t) (DwfJ a d)))) (cn-of/equiv (kd-equiv/sigma ([_] [_] kd-equiv/trans DequivK'JCK DequivK) (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/trans DequivK'JCK DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/trans DequivK'JCK DequivK)))) (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK'))))) DofCK) ([c] [f] cn-of/rec (cn-of/pi2 (cn-of/pi2 f)) ([a] [d] [b] [e] cn-of/app e (cn-of/app d (cn-of/pi1 (cn-of/pi2 f)))) (DwfJ _ (cn-of/pi1 f)))))) <- can-tmap Kr (DmapKr : tmap Kr Ar) <- kd-equiv-reg DeqvK (DwfKr : kd-wf Kr) (DwfK : kd-wf K) <- invert-tmap-1 DeqvK DmapKr (DmapAr : tunmap Ar Kr') (DequivKr : kd-equiv Kr Kr') <- invert-tmap-2 DeqvK DmapK (DmapA : tunmap A K') (DequivK : kd-equiv K K') <- map-wf' DwfK DmapK (DwfA : ewf A) <- map-wf' DwfKr DmapKr (DwfAr : ewf Ar) <- ({a} {da:cn-of a (pi Kr ([_] t))} {das:cn-assm da} mcn-assm da das -> cn-of-reg da (kd-wf/pi ([_] [_] kd-wf/t) DwfKr) -> {x} {dx:evof x (epi Ar ([_] et))} {at} {xt} can-map a at -> map-of da at (tmap/pi ([_] [_] [_] tmap/t) DmapKr) (eof/var (ewf/pi ([_] [_] ewf/t) DwfAr) dx) -> can-unmap x xt -> unmap-vof dx xt (tunmap/pi ([_] [_] [_] tunmap/t) DmapAr) (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) DequivKr) da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da (tmap/pi ([_] [_] [_] tmap/t) DmapKr) (tunmap/pi ([_] [_] [_] tunmap/t) DmapAr) (kd-equiv/pi ([_] [_] kd-equiv/t) DequivKr) -> {b} {db:cn-of b Kr} {dbs} mcn-assm db dbs -> cn-of-reg db DwfKr -> {y} {dy:evof y Ar} {bt} {yt} can-map b bt -> map-of db bt DmapKr (eof/var DwfAr dy) -> can-unmap y yt -> unmap-vof dy yt DmapAr (cn-of/equiv DequivKr db) -> invert-map db bt yt (cn-equiv/refl db) -> invert-tmap-cn-of' db DmapKr DmapAr DequivKr -> invert-map-2 (DeqvC1 a da b db) (DmapC1 a x at b y bt) (DmapM1 x a xt y b yt : unmap (M1 x y) (C1' a b)) (DequivC1 a da b db : cn-equiv (C1 a b) (C1' a b) t)) <- invert-map-2 DeqvC2 DmapC2 (DmapM2 : unmap M2 C2') (DequivC2 : cn-equiv C2 C2' Kr) <- can-skof SK (Dskof : skof SK D E) <- flay-sound DwfA Dflay Dskof (DofMA : eof MA D) (DequivAE : tequiv A (E MA)) <- unmap-skof Dskof (DmapD : tunmap D I) (DmapE : {x} {a} unmap x a -> tunmap (E x) (J a)) (Dskof' : skof-il SK I J) <- can-unmap MA (DmapMA : unmap MA CK) <- cn-equiv-reg (cn-equiv/equiv DeqvK DequivC2) _ (DofC2' : cn-of C2' K) _ <- kd-equiv-reg DequivK _ (DwfK' : kd-wf K') <- ({a} {da} {das} mcn-assm da das -> cn-of-reg da (kd-wf/pi ([_] [_] kd-wf/t) DwfK) -> {b} {db} {dbs} mcn-assm db dbs -> cn-of-reg db DwfK -> cn-equiv-reg (DequivC1 a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DeqvK)) da) b (cn-of/equiv (kd-equiv/symm DeqvK) db)) (DDDD1 a da b db) (DofC1' a da b db : cn-of (C1' a b) t) (DDDD2 a da b db)) <- unmap-of' DofMA DmapMA DmapD (DofCK : cn-of CK I) <- unmap-tequiv DequivAE DmapA (DmapE _ _ DmapMA) (DequivK'JCK : kd-equiv K' (J CK)) <- skof-il-reg Dskof' _ (DwfJ : {a} cn-of a I -> kd-wf (J a)) <- functionality-kd DwfJ (cn-equiv/symm (cn-equiv/beta1 (cn-of/pair ([_] [_] DwfK) DofC2' (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK))) (cn-of/lam ([a] [d] cn-of/lam ([b] [e:cn-of b K'] DofC1' a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/symm DequivK)) d) b (cn-of/equiv (kd-equiv/symm DequivK) e)) DwfK') (kd-wf/pi ([_] [_] kd-wf/t) DwfK')))) DofCK) : cn-equiv CK (pi1 (pair CK _)) I) (DequivJCK : kd-equiv (J CK) (J (pi1 (pair CK _)))). - : invert-map-1 (cn-equiv/beta (Dof1 : cn-of C1 K1) (Dof2 : {a} cn-of a K1 -> cn-of (C2 a) (K2 a))) (map/app (DmapC1 : map C1 M1) (map/lam (DmapC2 : {a} {x} map a x -> map (C2 a) (M2 x)) (DmapK1 : tmap K1 A1))) (unmap/app DunmapM1 (unmap/lam DunmapM2 DunmapA1)) (cn-equiv/app Dequiv1 (cn-equiv/lam Dequiv2 DequivK1)) <- invert-map Dof1 DmapC1 (DunmapM1 : unmap M1 C1') (Dequiv1 : cn-equiv C1 C1' K1) <- invert-tmap-cn-of Dof1 DmapK1 (DunmapA1 : tunmap A1 K1') (DequivK1 : kd-equiv K1 K1') <- cn-of-reg Dof1 (DwfK1 : kd-wf K1) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> {x} {dx:evof x A1} {at} {xt} can-map a at -> map-of da at DmapK1 (eof/var DwfA1 dx) -> can-unmap x xt -> unmap-vof dx xt DunmapA1 (cn-of/equiv DequivK1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da DmapK1 DunmapA1 DequivK1 -> invert-map (Dof2 a da) (DmapC2 a x at) (DunmapM2 x a xt : unmap (M2 x) (C2' a)) (Dequiv2 a da : cn-equiv (C2 a) (C2' a) (K2 a))). -beta : invert-map-2' (Dmaps : map (C2 C1) Ms) (cn-equiv/beta (Dof1 : cn-of C1 K1) (Dof2 : {a} cn-of a K1 -> cn-of (C2 a) (K2 a))) Dunmaps (cn-equiv/trans (cn-equiv/equiv (kd-equiv/symm DequivK2sub) (Dequiv2 C1' DofC1')) DequivC2sub) <- can-tmap K1 (DmapK1 : tmap K1 A1) <- can-map C1 (DmapC1 : map C1 M1) <- ({x} {a} {at:map a x} can-map a at -> can-map (C2 a) (DmapC2 a x at : map (C2 a) (M2 x))) <- invert-map Dof1 DmapC1 (DunmapM1 : unmap M1 C1') (Dequiv1 : cn-equiv C1 C1' K1) <- invert-tmap-cn-of Dof1 DmapK1 (DunmapA1 : tunmap A1 K1') (DequivK1 : kd-equiv K1 K1') <- cn-of-reg Dof1 (DwfK1 : kd-wf K1) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> {x} {dx:evof x A1} {at} {xt} can-map a at -> map-of da at DmapK1 (eof/var DwfA1 dx) -> can-unmap x xt -> unmap-vof dx xt DunmapA1 (cn-of/equiv DequivK1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da DmapK1 DunmapA1 DequivK1 -> invert-map (Dof2 a da) (DmapC2 a x at) (DunmapM2 x a xt : unmap (M2 x) (C2' a)) (Dequiv2 a da : cn-equiv (C2 a) (C2' a) (K2 a))) <- map-fun (DmapC2 C1 M1 DmapC1) Dmaps (Deq : eterm-eq (M2 M1) Ms) <- unmap-resp Deq con-eq/i (DunmapM2 M1 C1' DunmapM1) (Dunmaps : unmap Ms (C2' C1')) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> cn-equiv-reg (Dequiv2 a da) (DofC2 a da : cn-of (C2 a) (K2 a)) (DofC2' a da : cn-of (C2' a) (K2 a)) (DwfK2 a da : kd-wf (K2 a))) <- functionality-kd DwfK2 Dequiv1 (DequivK2sub : kd-equiv (K2 C1) (K2 C1')) <- functionality-cn DofC2 Dequiv1 (DequivC2sub : cn-equiv (C2 C1) (C2 C1') (K2 C1)) <- cn-equiv-reg Dequiv1 _ (DofC1' : cn-of C1' K1) _. - : invert-map-2' (Dmap1 : map C1 M1) (cn-equiv/beta1 (Dof2 : cn-of C2 K2) (Dof1 : cn-of C1 K1)) Dunmap1 Dequiv1 <- invert-map Dof1 Dmap1 Dunmap1 Dequiv1. - : invert-map-2' (Dmap2 : map C2 M2) (cn-equiv/beta2 (Dof2 : cn-of C2 K2) (Dof1 : cn-of C1 K1)) Dunmap2 Dequiv2 <- invert-map Dof2 Dmap2 Dunmap2 Dequiv2. %%% - : invert-tmap-cn-equiv' (cn-equiv/refl Dof) Dmap Dunmap Dequiv <- invert-tmap-cn-of' Dof Dmap Dunmap Dequiv. - : invert-tmap-cn-equiv' (cn-equiv/symm Deqv) Dmap Dunmap Dequiv <- invert-tmap-cn-equiv' Deqv Dmap Dunmap Dequiv. - : invert-tmap-cn-equiv' (cn-equiv/trans _ Deqv) Dmap Dunmap Dequiv <- invert-tmap-cn-equiv' Deqv Dmap Dunmap Dequiv. - : invert-tmap-cn-equiv' (cn-equiv/pair Dwf2 _ Deqv1) (tmap/sigma Dmap2 Dmap1) (tunmap/sigma Dunmap2 Dunmap1) (kd-equiv/sigma Dequiv2 Dequiv1) <- invert-tmap-cn-equiv' Deqv1 Dmap1 Dunmap1 Dequiv1 <- cn-equiv-reg Deqv1 _ _ Dwf1 <- map-wf' Dwf1 Dmap1 Dwf1' <- ({x} {a} {at} can-map a at -> can-tmap (K2 a) (Dmap2 a x at : tmap (K2 a) (A2 x))) <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da Dwf1 -> {x} {dx:evof x A} {at} {xt} can-map a at -> map-of da at Dmap1 (eof/var Dwf1' dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1 (cn-of/equiv Dequiv1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1 Dunmap1 Dequiv1 -> invert-tmap (Dwf2 a da) (Dmap2 a x at) (Dunmap2 x a xt) (Dequiv2 a da)). - : invert-tmap-cn-equiv' (cn-equiv/pi1 Dof) Dmap1 Dunmap1 Dequiv1 <- invert-tmap-cn-equiv' Dof (tmap/sigma Dmap2 Dmap1) (tunmap/sigma Dunmap2 Dunmap1) Dequiv <- injective-sigma Dequiv Dequiv1 Dequiv2. - : invert-tmap-cn-equiv' (cn-equiv/pi2 (DeqvC : cn-equiv C Cr (sigma K1 K2))) (Dmap2 (pi1 C) (epi1 M) (map/pi1 DmapC)) (Dunmap2 (epi1 M) (pi1 C') (unmap/pi1 DunmapC)) (kd-equiv/trans (Dequiv2 (pi1 C') (cn-of/pi1 DofC')) Dequiv2s) <- can-tmap K1 (Dmap1 : tmap K1 A1) <- ({x} {a} {at} can-map a at -> can-tmap (K2 a) (Dmap2 a x at : tmap (K2 a) (A2 x))) <- invert-tmap-cn-equiv DeqvC (tmap/sigma Dmap2 Dmap1) (tunmap/sigma (Dunmap2 : {x} {a} unmap x a -> tunmap (A2 x) (K2' a)) (Dunmap1 : tunmap A1 K1')) (Dequiv : kd-equiv (sigma K1 K2) (sigma K1' K2')) <- injective-sigma Dequiv (Dequiv1 : kd-equiv K1 K1') (Dequiv2 : {a} cn-of a K1 -> kd-equiv (K2 a) (K2' a)) <- can-map C (DmapC : map C M) <- cn-equiv-reg DeqvC DofC _ _ <- invert-map-1 DeqvC DmapC (DunmapC : unmap M C') (DequivC : cn-equiv C C' (sigma K1 K2)) <- cn-of-reg DofC (kd-wf/sigma (Dwf2 : {a} cn-of a K1 -> kd-wf (K2 a)) _) <- functionality-kd Dwf2 (cn-equiv/pi1 DequivC) (Dequiv2s : kd-equiv (K2 (pi1 C)) (K2 (pi1 C'))) <- cn-equiv-reg DequivC _ (DofC' : cn-of C' (sigma K1 K2)) _. - : invert-tmap-cn-equiv' (cn-equiv/lam Deqv Deqv1) (tmap/pi Dmap2 Dmap1) (tunmap/pi Dunmap2 Dunmap1) (kd-equiv/pi Dequiv2 Dequiv1) <- can-tmap _ Dmap1 <- invert-tmap-1 Deqv1 Dmap1 Dunmap1 Dequiv1 <- kd-equiv-reg Deqv1 Dwf1 _ <- map-wf' Dwf1 Dmap1 Dwf1' <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da Dwf1 -> {x} {dx:evof x A} {at} {xt} can-map a at -> map-of da at Dmap1 (eof/var Dwf1' dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1 (cn-of/equiv Dequiv1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1 Dunmap1 Dequiv1 -> invert-tmap-cn-equiv' (Deqv a da) (Dmap2 a x at) (Dunmap2 x a xt) (Dequiv2 a da)). - : invert-tmap-cn-equiv' (cn-equiv/app (Deqv2 : cn-equiv C2 C2r K1) (Deqv1 : cn-equiv C1 C1r (pi K1 K2))) (Dmap2 C2 M2 DmapC2) (Dunmap2 M2 C2' DunmapC2) (kd-equiv/trans (Dequiv2 C2' DofC2') Dequiv2s) <- can-tmap K1 (Dmap1 : tmap K1 A1) <- ({x} {a} {at} can-map a at -> can-tmap (K2 a) (Dmap2 a x at : tmap (K2 a) (A2 x))) <- invert-tmap-cn-equiv Deqv1 (tmap/pi Dmap2 Dmap1) (tunmap/pi (Dunmap2 : {x} {a} unmap x a -> tunmap (A2 x) (K2' a)) (Dunmap1 : tunmap A1 K1')) (Dequiv : kd-equiv (pi K1 K2) (pi K1' K2')) <- injective-pi Dequiv (Dequiv1 : kd-equiv K1 K1') (Dequiv2 : {a} cn-of a K1 -> kd-equiv (K2 a) (K2' a)) <- can-map C2 (DmapC2 : map C2 M2) <- invert-map-1 Deqv2 DmapC2 (DunmapC2 : unmap M2 C2') (DequivC2 : cn-equiv C2 C2' K1) <- cn-equiv-reg Deqv1 _ _ (kd-wf/pi (Dwf2 : {a} cn-of a K1 -> kd-wf (K2 a)) _) <- functionality-kd Dwf2 DequivC2 (Dequiv2s : kd-equiv (K2 C2) (K2 C2')) <- cn-equiv-reg DequivC2 _ (DofC2' : cn-of C2' K1) _. - : invert-tmap-cn-equiv' _ tmap/one tunmap/one kd-equiv/one. - : invert-tmap-cn-equiv' _ tmap/t tunmap/t kd-equiv/t. - : invert-tmap-cn-equiv' (cn-equiv/sing Dof) (tmap/sing Dmap) (tunmap/sing Dunmap) (kd-equiv/sing Dequiv) <- can-map _ Dmap <- invert-map-1 Dof Dmap Dunmap Dequiv. - : invert-tmap-cn-equiv' (cn-equiv/extpi (Deqv : {a} cn-of a K1 -> cn-equiv (app C a) (app Cr a) (K2 a)) _ (DofPre : cn-of C (pi K1 K2p))) (tmap/pi DmapK2 DmapK1) (tunmap/pi DunmapA2 DunmapA1) (kd-equiv/pi DequivK2 DequivK1) <- can-tmap K1 (DmapK1 : tmap K1 A1) <- ({x} {a} {at:map a x} can-map a at -> can-tmap (K2p a) (DmapK2p a x at : tmap (K2p a) (A2p x))) <- invert-tmap-cn-of DofPre (tmap/pi DmapK2p DmapK1) (tunmap/pi (DunmapA2p : {x} {a} unmap x a -> tunmap (A2p x) (K2p' a)) (DunmapA1 : tunmap A1 K1')) (Dequiv : kd-equiv (pi K1 K2p) (pi K1' K2p')) <- injective-pi Dequiv (DequivK1 : kd-equiv K1 K1') _ <- cn-of-reg DofPre (kd-wf/pi _ (DwfK1 : kd-wf K1)) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> {x} {dx:evof x A1} {at} {xt} can-map a at -> map-of da at DmapK1 (eof/var DwfA1 dx) -> can-unmap x xt -> unmap-vof dx xt DunmapA1 (cn-of/equiv DequivK1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da DmapK1 DunmapA1 DequivK1 -> invert-tmap-cn-equiv' (Deqv a da) (DmapK2 a x at : tmap (K2 a) (A2 x)) (DunmapA2 x a xt : tunmap (A2 x) (K2' a)) (DequivK2 a da : kd-equiv (K2 a) (K2' a))). - : invert-tmap-cn-equiv' (cn-equiv/extpiw (Deqv : {a} cn-of a K1 -> cn-equiv (app C a) (app Cr a) (K2 a)) (DeqvPre : cn-equiv C Cr (pi K1 K2p))) (tmap/pi DmapK2 DmapK1) (tunmap/pi DunmapA2 DunmapA1) (kd-equiv/pi DequivK2 DequivK1) <- can-tmap K1 (DmapK1 : tmap K1 A1) <- ({x} {a} {at:map a x} can-map a at -> can-tmap (K2p a) (DmapK2p a x at : tmap (K2p a) (A2p x))) <- invert-tmap-cn-equiv DeqvPre (tmap/pi DmapK2p DmapK1) (tunmap/pi (DunmapA2p : {x} {a} unmap x a -> tunmap (A2p x) (K2p' a)) (DunmapA1 : tunmap A1 K1')) (Dequiv : kd-equiv (pi K1 K2p) (pi K1' K2p')) <- injective-pi Dequiv (DequivK1 : kd-equiv K1 K1') _ <- cn-equiv-reg DeqvPre _ _ (kd-wf/pi _ (DwfK1 : kd-wf K1)) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- ({a} {da:cn-of a K1} {das:cn-assm da} mcn-assm da das -> cn-of-reg da DwfK1 -> {x} {dx:evof x A1} {at} {xt} can-map a at -> map-of da at DmapK1 (eof/var DwfA1 dx) -> can-unmap x xt -> unmap-vof dx xt DunmapA1 (cn-of/equiv DequivK1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da DmapK1 DunmapA1 DequivK1 -> invert-tmap-cn-equiv' (Deqv a da) (DmapK2 a x at : tmap (K2 a) (A2 x)) (DunmapA2 x a xt : tunmap (A2 x) (K2' a)) (DequivK2 a da : kd-equiv (K2 a) (K2' a))). - : invert-tmap-cn-equiv' (cn-equiv/extsigma Dwf2 _ Dof1) (tmap/sigma Dmap2 Dmap1) (tunmap/sigma Dunmap2 Dunmap1) (kd-equiv/sigma Dequiv2 Dequiv1) <- invert-tmap-cn-equiv' Dof1 Dmap1 Dunmap1 Dequiv1 <- cn-equiv-reg Dof1 _ _ Dwf1 <- map-wf' Dwf1 Dmap1 Dwf1' <- ({x} {a} {at:map a x} can-map a at -> can-tmap (K2 a) (Dmap2 a x at)) <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da Dwf1 -> {x} {dx:evof x A} {at} {xt} can-map a at -> map-of da at Dmap1 (eof/var Dwf1' dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1 (cn-of/equiv Dequiv1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1 Dunmap1 Dequiv1 -> invert-tmap (Dwf2 a da) (Dmap2 a x at) (Dunmap2 x a xt) (Dequiv2 a da)). - : invert-tmap-cn-equiv' (cn-equiv/subsume Dsub _) Dmap2 Dunmap2 Dequiv2 <- can-tmap _ Dmap1 <- can-tmap _ Dmap2 <- invert-tmap-kd-sub Dsub Dmap1 Dmap2 _ Dunmap2 _ Dequiv2. - : invert-tmap-cn-equiv' (cn-equiv/beta Dof1 Dof2) (Dmap2 C M DmapC) (Dunmap2 M C' DunmapM) (kd-equiv/trans (Dequiv2 C' DofC') Dequiv2sub) <- invert-tmap-cn-of' Dof1 Dmap1 Dunmap1 Dequiv1 <- cn-of-reg Dof1 Dwf1 <- map-wf' Dwf1 Dmap1 Dwf1' <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da Dwf1 -> {x} {dx:evof x A} {at} {xt} can-map a at -> map-of da at Dmap1 (eof/var Dwf1' dx) -> can-unmap x xt -> unmap-vof dx xt Dunmap1 (cn-of/equiv Dequiv1 da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da Dmap1 Dunmap1 Dequiv1 -> invert-tmap-cn-of' (Dof2 a da) (Dmap2 a x at : tmap (K2 a) (A2 x)) (Dunmap2 x a xt : tunmap (A2 x) (K2' a)) (Dequiv2 a da)) <- can-map C (DmapC : map C M) <- invert-map Dof1 DmapC (DunmapM : unmap M C') DequivC <- ({a} {da:cn-of a K} {das:cn-assm da} mcn-assm da das -> cn-of-reg da Dwf1 -> cn-of-reg (Dof2 a da) (Dwf2 a da : kd-wf (K2 a))) <- functionality-kd Dwf2 DequivC Dequiv2sub <- cn-equiv-reg DequivC _ DofC' _. - : invert-tmap-cn-equiv' (cn-equiv/beta1 Dof2 Dof1) Dmap Dunmap Dequiv <- invert-tmap-cn-of' Dof1 Dmap Dunmap Dequiv. - : invert-tmap-cn-equiv' (cn-equiv/beta2 Dof2 Dof1) Dmap Dunmap Dequiv <- invert-tmap-cn-of' Dof2 Dmap Dunmap Dequiv. %worlds (invert-bind) (invert-map _ _ _ _) (invert-tmap _ _ _ _) (invert-tmap-cn-of' _ _ _ _) (invert-tmap-cn-of _ _ _ _) (invert-tmap-kd-sub _ _ _ _ _ _ _) (invert-tmap-kd-equiv _ _ _ _ _ _ _) (invert-tmap-1 _ _ _ _) (invert-tmap-2 _ _ _ _) (invert-map-1 _ _ _ _) (invert-map-2' _ _ _ _) (invert-map-2 _ _ _ _) (invert-tmap-cn-equiv' _ _ _ _) (invert-tmap-cn-equiv _ _ _ _). %total (D1 D2 D3 D4 D5 D6 D7 D8 D9 D10 D11 D12 D13) (invert-map D1 _ _ _) (invert-tmap D2 _ _ _) (invert-tmap-cn-of' D3 _ _ _) (invert-tmap-cn-of D4 _ _ _) (invert-tmap-kd-sub D5 _ _ _ _ _ _) (invert-tmap-kd-equiv D6 _ _ _ _ _ _) (invert-tmap-1 D7 _ _ _) (invert-tmap-2 D8 _ _ _) (invert-map-1 D9 _ _ _) (invert-map-2' _ D10 _ _) (invert-map-2 D11 _ _ _) (invert-tmap-cn-equiv' D12 _ _ _) (invert-tmap-cn-equiv D13 _ _ _). invert-tmap' : kd-wf K -> tmap K A -> tunmap A K' %% -> kd-equiv K K' -> type. %mode invert-tmap' +X1 +X2 +X3 -X4. - : invert-tmap' Dwf Dmap Dunmap Dequiv' <- invert-tmap Dwf Dmap Dunmap' Dequiv <- tunmap-fun Dunmap' Dunmap Deq <- kd-equiv-resp kind-eq/i Deq Dequiv Dequiv'. %worlds (invert-bind) (invert-tmap' _ _ _ _). %total {} (invert-tmap' _ _ _ _). %%%%% Consistency %%%%% false-implies-similar : false %% -> similar T1 T2 -> type. %mode +{T1:con} +{T2:con} +{X1:false} -{X2:similar T1 T2} (false-implies-similar X1 X2). %worlds () (false-implies-similar _ _). %total {} (false-implies-similar _ _). ekof-rec-unary : {SK} ekof (const/rec SK) (epi A ([_] et)) -> type. %mode ekof-rec-unary +X1 -X2. - : ekof-rec-unary SK (ekof/i (etopen-rec _ _ _ _ _ _ DopenA DskelA DopenB DskelB) (ckof/rec Dcskof)) <- can-cskof SK Dcskof <- cskof-implies-skof Dcskof DopenA DskelA DopenB _ <- ({x} can-etp-skel _ (DskelB x)). %worlds () (ekof-rec-unary _ _). %total {} (ekof-rec-unary _ _). eq-unit-tagged : constant-eq const/unit const/tagged -> false -> type. %mode eq-unit-tagged +X1 -X2. %worlds () (eq-unit-tagged _ _). %total {} (eq-unit-tagged _ _). eq-unit-void : constant-eq const/unit const/void -> false -> type. %mode eq-unit-void +X1 -X2. %worlds () (eq-unit-void _ _). %total {} (eq-unit-void _ _). eq-void-tagged : constant-eq const/void const/tagged -> false -> type. %mode eq-void-tagged +X1 -X2. %worlds () (eq-void-tagged _ _). %total {} (eq-void-tagged _ _). eq-prod-arrow : constant-eq const/prod const/arrow -> false -> type. %mode eq-prod-arrow +X1 -X2. %worlds () (eq-prod-arrow _ _). %total {} (eq-prod-arrow _ _). eq-prod-plus : constant-eq const/prod const/plus -> false -> type. %mode eq-prod-plus +X1 -X2. %worlds () (eq-prod-plus _ _). %total {} (eq-prod-plus _ _). eq-arrow-plus : constant-eq const/arrow const/plus -> false -> type. %mode eq-arrow-plus +X1 -X2. %worlds () (eq-arrow-plus _ _). %total {} (eq-arrow-plus _ _). eq-ref-tag : constant-eq const/ref const/tag -> false -> type. %mode eq-ref-tag +X1 -X2. %worlds () (eq-ref-tag _ _). %total {} (eq-ref-tag _ _). eq-ref-labeled : constant-eq const/ref (const/labeled I) -> false -> type. %mode eq-ref-labeled +X1 -X2. %worlds () (eq-ref-labeled _ _). %total {} (eq-ref-labeled _ _). eq-ref-rec : constant-eq const/ref (const/rec _) -> false -> type. %mode eq-ref-rec +X1 -X2. %worlds () (eq-ref-rec _ _). %total {} (eq-ref-rec _ _). eq-tag-rec : constant-eq const/tag (const/rec _) -> false -> type. %mode eq-tag-rec +X1 -X2. %worlds () (eq-tag-rec _ _). %total {} (eq-tag-rec _ _). eq-labeled-rec : constant-eq (const/labeled I) (const/rec _) -> false -> type. %mode eq-labeled-rec +X1 -X2. %worlds () (eq-labeled-rec _ _). %total {} (eq-labeled-rec _ _). eq-labeled-tag : constant-eq (const/labeled I) const/tag -> false -> type. %mode eq-labeled-tag +X1 -X2. %worlds () (eq-labeled-tag _ _). %total {} (eq-labeled-tag _ _). etopen/tt : etopen (carrow ct ct) (epi et ([_] et)) = etopen/arrow etopen/t etp-skel/t etopen/t. etopen/ttt : etopen (carrow ct (carrow ct ct)) (epi et ([_] epi et ([_] et))) = etopen/arrow (etopen/arrow etopen/t etp-skel/t etopen/t) etp-skel/t etopen/t. consistency : cn-equiv T1 T2 t -> similar T1 T1 -> similar T2 _ %% -> similar T1 T2 -> type. %mode consistency +X1 +X2 +X3 -X4. %% Successful cases. - : consistency _ _ _ similar/unit. - : consistency _ _ _ similar/void. - : consistency _ _ _ similar/prod. - : consistency _ _ _ similar/arrow. - : consistency _ _ _ similar/plus. - : consistency _ _ _ similar/ref. - : consistency _ _ _ similar/tag. - : consistency _ _ _ similar/labeled. - : consistency _ _ _ similar/tagged. - : consistency _ _ _ similar/rec. %% Contradiction cases. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/unit map/void tmap/t Dequiv' <- nullary-equiv-head (ekof/i etopen/t ckof/unit) (ekof/i etopen/t ckof/void) Dequiv' Deq <- eq-unit-void Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/unit (map/prod _ _) tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/ttt ckof/prod) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/unit (map/arrow _ _) tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/ttt ckof/arrow) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/unit (map/plus _ _) tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/ttt ckof/plus) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/unit (map/ref _) tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/tt ckof/ref) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/unit (map/tag _) tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/tt ckof/tag) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ Dmap <- map-equiv-i2 Dequiv map/unit (map/labeled Dmap) tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/tt ckof/labeled) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/unit map/tagged tmap/t Dequiv' <- nullary-equiv-head (ekof/i etopen/t ckof/unit) (ekof/i etopen/t ckof/tagged) Dequiv' Deq <- eq-unit-tagged Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/unit (map/rec _ _ _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- nullary-unary-equiv (ekof/i etopen/t ckof/unit) Dkof Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/void map/unit tmap/t Dequiv' <- nullary-equiv-head (ekof/i etopen/t ckof/unit) (ekof/i etopen/t ckof/void) (equiv/symm Dequiv') Deq <- eq-unit-void Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/void (map/prod _ _) tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/ttt ckof/prod) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/void (map/arrow _ _) tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/ttt ckof/arrow) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/void (map/plus _ _) tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/ttt ckof/plus) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/void (map/ref _) tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/tt ckof/ref) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/void (map/tag _) tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/tt ckof/tag) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ Dmap <- map-equiv-i2 Dequiv map/void (map/labeled Dmap) tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/tt ckof/labeled) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/void map/tagged tmap/t Dequiv' <- nullary-equiv-head (ekof/i etopen/t ckof/void) (ekof/i etopen/t ckof/tagged) Dequiv' Deq <- eq-void-tagged Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/void (map/rec _ _ _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- nullary-unary-equiv (ekof/i etopen/t ckof/void) Dkof Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/prod _ _) map/unit tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/ttt ckof/prod) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/prod _ _) map/void tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/ttt ckof/prod) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/prod _ _) (map/arrow _ _) tmap/t Dequiv' <- binary-equiv-head (ekof/i etopen/ttt ckof/prod) (ekof/i etopen/ttt ckof/arrow) Dequiv' Deq <- eq-prod-arrow Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/prod _ _) (map/plus _ _) tmap/t Dequiv' <- binary-equiv-head (ekof/i etopen/ttt ckof/prod) (ekof/i etopen/ttt ckof/plus) Dequiv' Deq <- eq-prod-plus Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/prod _ _) (map/ref _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/ref) (ekof/i etopen/ttt ckof/prod) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/prod _ _) (map/tag _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/tag) (ekof/i etopen/ttt ckof/prod) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i2 Dequiv (map/prod _ _) (map/labeled D) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/labeled) (ekof/i etopen/ttt ckof/prod) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/prod _ _) map/tagged tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/ttt ckof/prod) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/prod _ _) (map/rec _ _ _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-binary-equiv Dkof (ekof/i etopen/ttt ckof/prod) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/arrow _ _) map/unit tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/ttt ckof/arrow) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/arrow _ _) map/void tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/ttt ckof/arrow) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/arrow _ _) (map/prod _ _) tmap/t Dequiv' <- binary-equiv-head (ekof/i etopen/ttt ckof/prod) (ekof/i etopen/ttt ckof/arrow) (equiv/symm Dequiv') Deq <- eq-prod-arrow Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/arrow _ _) (map/plus _ _) tmap/t Dequiv' <- binary-equiv-head (ekof/i etopen/ttt ckof/arrow) (ekof/i etopen/ttt ckof/plus) Dequiv' Deq <- eq-arrow-plus Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/arrow _ _) (map/ref _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/ref) (ekof/i etopen/ttt ckof/arrow) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/arrow _ _) (map/tag _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/tag) (ekof/i etopen/ttt ckof/arrow) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i2 Dequiv (map/arrow _ _) (map/labeled D) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/labeled) (ekof/i etopen/ttt ckof/arrow) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/arrow _ _) map/tagged tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/ttt ckof/arrow) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/arrow _ _) (map/rec _ _ _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-binary-equiv Dkof (ekof/i etopen/ttt ckof/arrow) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/plus _ _) map/unit tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/ttt ckof/plus) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/plus _ _) map/void tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/ttt ckof/plus) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/plus _ _) (map/prod _ _) tmap/t Dequiv' <- binary-equiv-head (ekof/i etopen/ttt ckof/prod) (ekof/i etopen/ttt ckof/plus) (equiv/symm Dequiv') Deq <- eq-prod-plus Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/plus _ _) (map/arrow _ _) tmap/t Dequiv' <- binary-equiv-head (ekof/i etopen/ttt ckof/arrow) (ekof/i etopen/ttt ckof/plus) (equiv/symm Dequiv') Deq <- eq-arrow-plus Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/plus _ _) (map/ref _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/ref) (ekof/i etopen/ttt ckof/plus) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/plus _ _) (map/tag _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/tag) (ekof/i etopen/ttt ckof/plus) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i2 Dequiv (map/plus _ _) (map/labeled D) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/labeled) (ekof/i etopen/ttt ckof/plus) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/plus _ _) map/tagged tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/ttt ckof/plus) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/plus _ _) (map/rec _ _ _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-binary-equiv Dkof (ekof/i etopen/ttt ckof/plus) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/ref _) map/unit tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/tt ckof/ref) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/ref _) map/void tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/tt ckof/ref) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/ref _) (map/prod _ _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/ref) (ekof/i etopen/ttt ckof/prod) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/ref _) (map/arrow _ _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/ref) (ekof/i etopen/ttt ckof/arrow) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/ref _) (map/plus _ _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/ref) (ekof/i etopen/ttt ckof/plus) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/ref _) (map/tag _) tmap/t Dequiv' <- unary-equiv-head (ekof/i etopen/tt ckof/ref) (ekof/i etopen/tt ckof/tag) Dequiv' Deq <- eq-ref-tag Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i2 Dequiv (map/ref D1) (map/labeled D) tmap/t Dequiv' <- unary-equiv-head (ekof/i etopen/tt ckof/ref) (ekof/i etopen/tt ckof/labeled) Dequiv' Deq <- eq-ref-labeled Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/ref _) map/tagged tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/tt ckof/ref) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/ref _) (map/rec _ _ _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-equiv-head (ekof/i etopen/tt ckof/ref) Dkof Dequiv' Deq <- eq-ref-rec Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/tag _) map/unit tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/tt ckof/tag) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/tag _) map/void tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/tt ckof/tag) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/tag _) (map/prod _ _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/tag) (ekof/i etopen/ttt ckof/prod) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/tag _) (map/arrow _ _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/tag) (ekof/i etopen/ttt ckof/arrow) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/tag _) (map/plus _ _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/tag) (ekof/i etopen/ttt ckof/plus) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/tag _) (map/ref _) tmap/t Dequiv' <- unary-equiv-head (ekof/i etopen/tt ckof/ref) (ekof/i etopen/tt ckof/tag) (equiv/symm Dequiv') Deq <- eq-ref-tag Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i2 Dequiv (map/tag D1) (map/labeled D) tmap/t Dequiv' <- unary-equiv-head (ekof/i etopen/tt ckof/labeled) (ekof/i etopen/tt ckof/tag) (equiv/symm Dequiv') Deq <- eq-labeled-tag Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/tag _) map/tagged tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/tt ckof/tag) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/tag _) (map/rec _ _ _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-equiv-head (ekof/i etopen/tt ckof/tag) Dkof Dequiv' Deq <- eq-tag-rec Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i1 Dequiv (map/labeled D) map/unit tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/unit) (ekof/i etopen/tt ckof/labeled) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i1 Dequiv (map/labeled D) map/void tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/void) (ekof/i etopen/tt ckof/labeled) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i1 Dequiv (map/labeled D) (map/prod _ _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/labeled) (ekof/i etopen/ttt ckof/prod) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i1 Dequiv (map/labeled D) (map/arrow _ _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/labeled) (ekof/i etopen/ttt ckof/arrow) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i1 Dequiv (map/labeled D) (map/plus _ _) tmap/t Dequiv' <- unary-binary-equiv (ekof/i etopen/tt ckof/labeled) (ekof/i etopen/ttt ckof/plus) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i1 Dequiv (map/labeled D) (map/ref _) tmap/t Dequiv' <- unary-equiv-head (ekof/i etopen/tt ckof/ref) (ekof/i etopen/tt ckof/labeled) (equiv/symm Dequiv') Deq <- eq-ref-labeled Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i1 Dequiv (map/labeled D) (map/tag _) tmap/t Dequiv' <- unary-equiv-head (ekof/i etopen/tt ckof/labeled) (ekof/i etopen/tt ckof/tag) Dequiv' Deq <- eq-labeled-tag Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i1 Dequiv (map/labeled D) map/tagged tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/tt ckof/labeled) (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i1 Dequiv (map/labeled D) (map/rec _ _ _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-equiv-head (ekof/i etopen/tt ckof/labeled) Dkof Dequiv' Deq <- eq-labeled-rec Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/tagged map/unit tmap/t Dequiv' <- nullary-equiv-head (ekof/i etopen/t ckof/unit) (ekof/i etopen/t ckof/tagged) (equiv/symm Dequiv') Deq <- eq-unit-tagged Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/tagged map/void tmap/t Dequiv' <- nullary-equiv-head (ekof/i etopen/t ckof/void) (ekof/i etopen/t ckof/tagged) (equiv/symm Dequiv') Deq <- eq-void-tagged Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/tagged (map/prod _ _) tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/ttt ckof/prod) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/tagged (map/arrow _ _) tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/ttt ckof/arrow) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/tagged (map/plus _ _) tmap/t Dequiv' <- nullary-binary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/ttt ckof/plus) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/tagged (map/ref _) tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/tt ckof/ref) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/tagged (map/tag _) tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/tt ckof/tag) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i2 Dequiv map/tagged (map/labeled D) tmap/t Dequiv' <- nullary-unary-equiv (ekof/i etopen/t ckof/tagged) (ekof/i etopen/tt ckof/labeled) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv map/tagged (map/rec _ _ _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- nullary-unary-equiv (ekof/i etopen/t ckof/tagged) Dkof Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/rec _ _ _ _) map/unit tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- nullary-unary-equiv (ekof/i etopen/t ckof/unit) Dkof (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/rec _ _ _ _) map/void tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- nullary-unary-equiv (ekof/i etopen/t ckof/void) Dkof (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/rec _ _ _ _) (map/prod _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-binary-equiv Dkof (ekof/i etopen/ttt ckof/prod) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/rec _ _ _ _) (map/arrow _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-binary-equiv Dkof (ekof/i etopen/ttt ckof/arrow) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/rec _ _ _ _) (map/plus _ _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-binary-equiv Dkof (ekof/i etopen/ttt ckof/plus) Dequiv' Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/rec _ _ _ _) (map/ref _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-equiv-head (ekof/i etopen/tt ckof/ref) Dkof (equiv/symm Dequiv') Deq <- eq-ref-rec Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/rec _ _ _ _) (map/tag _) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-equiv-head (ekof/i etopen/tt ckof/tag) Dkof (equiv/symm Dequiv') Deq <- eq-tag-rec Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- can-map _ D <- map-equiv-i2 Dequiv (map/rec _ _ _ _) (map/labeled D) tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- unary-equiv-head (ekof/i etopen/tt ckof/labeled) Dkof (equiv/symm Dequiv') Deq <- eq-labeled-rec Deq Dfalse <- false-implies-similar Dfalse Dsimilar. - : consistency Dequiv _ _ Dsimilar <- map-equiv Dequiv (map/rec _ _ _ _) map/tagged tmap/t Dequiv' <- ekof-rec-unary _ Dkof <- nullary-unary-equiv (ekof/i etopen/t ckof/tagged) Dkof (equiv/symm Dequiv') Dfalse <- false-implies-similar Dfalse Dsimilar. %worlds () (consistency _ _ _ _). %total {} (consistency _ _ _ _). %%%%% Injectivity Lemmas %%%%% injective-prod : cn-equiv (prod T1a T1b) (prod T2a T2b) t %% -> cn-equiv T1a T2a t -> cn-equiv T1b T2b t -> type. %mode injective-prod +X1 -X2 -X3. - : injective-prod (Dequiv : cn-equiv (prod T1a T1b) (prod T2a T2b) t) %% (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm Dequiv2a) Dequiv1) Dequiv1a) (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm Dequiv2b) Dequiv2) Dequiv1b) <- cn-equiv-reg Dequiv (Dof1 : cn-of (prod T1a T1b) t) (Dof2 : cn-of (prod T2a T2b) t) _ <- inversion-prod Dof1 (Dof1a : cn-of T1a t) (Dof1b : cn-of T1b t) <- inversion-prod Dof2 (Dof2a : cn-of T2a t) (Dof2b : cn-of T2b t) <- map-equiv Dequiv (map/prod (Dmap1b : map T1b M1b) (Dmap1a : map T1a M1a)) (map/prod (Dmap2b : map T2b M2b) (Dmap2a : map T2a M2a)) tmap/t (Dequiv' : equiv (eapp (eapp (econst const/prod) M1a) M1b) (eapp (eapp (econst const/prod) M2a) M2b) et) <- binary-equiv-inversion (ekof/i etopen/ttt ckof/prod) Dequiv' (Dequiv1' : equiv M1a M2a et) (Dequiv2' : equiv M1b M2b et) <- invert-map Dof1a Dmap1a (Dunmap1a : unmap M1a T1a') (Dequiv1a : cn-equiv T1a T1a' t) <- invert-map Dof1b Dmap1b (Dunmap1b : unmap M1b T1b') (Dequiv1b : cn-equiv T1b T1b' t) <- invert-map Dof2a Dmap2a (Dunmap2a : unmap M2a T2a') (Dequiv2a : cn-equiv T2a T2a' t) <- invert-map Dof2b Dmap2b (Dunmap2b : unmap M2b T2b') (Dequiv2b : cn-equiv T2b T2b' t) <- unmap-equiv Dunmap1a Dunmap2a Dequiv1' tunmap/t (Dequiv1 : cn-equiv T1a' T2a' t) <- unmap-equiv Dunmap1b Dunmap2b Dequiv2' tunmap/t (Dequiv2 : cn-equiv T1b' T2b' t). %worlds () (injective-prod _ _ _). %total {} (injective-prod _ _ _). injective-arrow : cn-equiv (arrow T1a T1b) (arrow T2a T2b) t %% -> cn-equiv T1a T2a t -> cn-equiv T1b T2b t -> type. %mode injective-arrow +X1 -X2 -X3. - : injective-arrow (Dequiv : cn-equiv (arrow T1a T1b) (arrow T2a T2b) t) %% (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm Dequiv2a) Dequiv1) Dequiv1a) (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm Dequiv2b) Dequiv2) Dequiv1b) <- cn-equiv-reg Dequiv (Dof1 : cn-of (arrow T1a T1b) t) (Dof2 : cn-of (arrow T2a T2b) t) _ <- inversion-arrow Dof1 (Dof1a : cn-of T1a t) (Dof1b : cn-of T1b t) <- inversion-arrow Dof2 (Dof2a : cn-of T2a t) (Dof2b : cn-of T2b t) <- map-equiv Dequiv (map/arrow (Dmap1b : map T1b M1b) (Dmap1a : map T1a M1a)) (map/arrow (Dmap2b : map T2b M2b) (Dmap2a : map T2a M2a)) tmap/t (Dequiv' : equiv (eapp (eapp (econst const/arrow) M1a) M1b) (eapp (eapp (econst const/arrow) M2a) M2b) et) <- binary-equiv-inversion (ekof/i etopen/ttt ckof/arrow) Dequiv' (Dequiv1' : equiv M1a M2a et) (Dequiv2' : equiv M1b M2b et) <- invert-map Dof1a Dmap1a (Dunmap1a : unmap M1a T1a') (Dequiv1a : cn-equiv T1a T1a' t) <- invert-map Dof1b Dmap1b (Dunmap1b : unmap M1b T1b') (Dequiv1b : cn-equiv T1b T1b' t) <- invert-map Dof2a Dmap2a (Dunmap2a : unmap M2a T2a') (Dequiv2a : cn-equiv T2a T2a' t) <- invert-map Dof2b Dmap2b (Dunmap2b : unmap M2b T2b') (Dequiv2b : cn-equiv T2b T2b' t) <- unmap-equiv Dunmap1a Dunmap2a Dequiv1' tunmap/t (Dequiv1 : cn-equiv T1a' T2a' t) <- unmap-equiv Dunmap1b Dunmap2b Dequiv2' tunmap/t (Dequiv2 : cn-equiv T1b' T2b' t). %worlds () (injective-arrow _ _ _). %total {} (injective-arrow _ _ _). injective-plus : cn-equiv (plus T1a T1b) (plus T2a T2b) t %% -> cn-equiv T1a T2a t -> cn-equiv T1b T2b t -> type. %mode injective-plus +X1 -X2 -X3. - : injective-plus (Dequiv : cn-equiv (plus T1a T1b) (plus T2a T2b) t) %% (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm Dequiv2a) Dequiv1) Dequiv1a) (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm Dequiv2b) Dequiv2) Dequiv1b) <- cn-equiv-reg Dequiv (Dof1 : cn-of (plus T1a T1b) t) (Dof2 : cn-of (plus T2a T2b) t) _ <- inversion-plus Dof1 (Dof1a : cn-of T1a t) (Dof1b : cn-of T1b t) <- inversion-plus Dof2 (Dof2a : cn-of T2a t) (Dof2b : cn-of T2b t) <- map-equiv Dequiv (map/plus (Dmap1b : map T1b M1b) (Dmap1a : map T1a M1a)) (map/plus (Dmap2b : map T2b M2b) (Dmap2a : map T2a M2a)) tmap/t (Dequiv' : equiv (eapp (eapp (econst const/plus) M1a) M1b) (eapp (eapp (econst const/plus) M2a) M2b) et) <- binary-equiv-inversion (ekof/i etopen/ttt ckof/plus) Dequiv' (Dequiv1' : equiv M1a M2a et) (Dequiv2' : equiv M1b M2b et) <- invert-map Dof1a Dmap1a (Dunmap1a : unmap M1a T1a') (Dequiv1a : cn-equiv T1a T1a' t) <- invert-map Dof1b Dmap1b (Dunmap1b : unmap M1b T1b') (Dequiv1b : cn-equiv T1b T1b' t) <- invert-map Dof2a Dmap2a (Dunmap2a : unmap M2a T2a') (Dequiv2a : cn-equiv T2a T2a' t) <- invert-map Dof2b Dmap2b (Dunmap2b : unmap M2b T2b') (Dequiv2b : cn-equiv T2b T2b' t) <- unmap-equiv Dunmap1a Dunmap2a Dequiv1' tunmap/t (Dequiv1 : cn-equiv T1a' T2a' t) <- unmap-equiv Dunmap1b Dunmap2b Dequiv2' tunmap/t (Dequiv2 : cn-equiv T1b' T2b' t). %worlds () (injective-plus _ _ _). %total {} (injective-plus _ _ _). injective-ref : cn-equiv (ref T1) (ref T2) t %% -> cn-equiv T1 T2 t -> type. %mode injective-ref +X1 -X2. - : injective-ref (Dequiv : cn-equiv (ref T1) (ref T2) t) %% (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm Dequiv2) Dequiv') Dequiv1) <- cn-equiv-reg Dequiv (Dof1 : cn-of (ref T1) t) (Dof2 : cn-of (ref T2) t) _ <- inversion-ref Dof1 (Dof1' : cn-of T1 t) <- inversion-ref Dof2 (Dof2' : cn-of T2 t) <- map-equiv Dequiv (map/ref (Dmap1 : map T1 M1)) (map/ref (Dmap2 : map T2 M2)) tmap/t (DequivSing : equiv (eapp (econst const/ref) M1) (eapp (econst const/ref) M2) et) <- unary-equiv-inversion (ekof/i etopen/tt ckof/ref) DequivSing (DequivSing' : equiv M1 M2 et) <- invert-map Dof1' Dmap1 (Dunmap1 : unmap M1 T1') (Dequiv1 : cn-equiv T1 T1' t) <- invert-map Dof2' Dmap2 (Dunmap2 : unmap M2 T2') (Dequiv2 : cn-equiv T2 T2' t) <- unmap-equiv Dunmap1 Dunmap2 DequivSing' tunmap/t (Dequiv' : cn-equiv T1' T2' t). %worlds () (injective-ref _ _). %total {} (injective-ref _ _). injective-tag : cn-equiv (tag T1) (tag T2) t %% -> cn-equiv T1 T2 t -> type. %mode injective-tag +X1 -X2. - : injective-tag (Dequiv : cn-equiv (tag T1) (tag T2) t) %% (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm Dequiv2) Dequiv') Dequiv1) <- cn-equiv-reg Dequiv (Dof1 : cn-of (tag T1) t) (Dof2 : cn-of (tag T2) t) _ <- inversion-tag Dof1 (Dof1' : cn-of T1 t) <- inversion-tag Dof2 (Dof2' : cn-of T2 t) <- map-equiv Dequiv (map/tag (Dmap1 : map T1 M1)) (map/tag (Dmap2 : map T2 M2)) tmap/t (DequivSing : equiv (eapp (econst const/tag) M1) (eapp (econst const/tag) M2) et) <- unary-equiv-inversion (ekof/i etopen/tt ckof/tag) DequivSing (DequivSing' : equiv M1 M2 et) <- invert-map Dof1' Dmap1 (Dunmap1 : unmap M1 T1') (Dequiv1 : cn-equiv T1 T1' t) <- invert-map Dof2' Dmap2 (Dunmap2 : unmap M2 T2') (Dequiv2 : cn-equiv T2 T2' t) <- unmap-equiv Dunmap1 Dunmap2 DequivSing' tunmap/t (Dequiv' : cn-equiv T1' T2' t). %worlds () (injective-tag _ _). %total {} (injective-tag _ _). injective-rec : cn-equiv (rec K1 C1a C1b) (rec K2 C2a C2b) t %% -> kd-equiv K1 K2 -> ({a} cn-of a (pi K1 ([_] t)) -> {b} cn-of b K1 -> cn-equiv (C1a a b) (C2a a b) t) -> cn-equiv C1b C2b K1 -> type. %mode injective-rec +X1 -X2 -X3 -X4. - : injective-rec (Dequiv : cn-equiv (rec K1 C1a C1b) (rec K2 C2a C2b) t) %% (kd-equiv/trans (kd-equiv/trans (kd-equiv/symm DequivK2) DequivK) DequivK1) ([a] [da] [b] [db] cn-equiv/trans (cn-equiv/trans (cn-equiv/symm (DequivC2a a (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) (kd-equiv/trans (kd-equiv/trans (kd-equiv/symm DequivK2) DequivK) DequivK1)) da) b (cn-of/equiv (kd-equiv/trans (kd-equiv/trans (kd-equiv/symm DequivK2) DequivK) DequivK1) db))) (DequivCa a da b db)) (DequivC1a a da b db)) (cn-equiv/trans (cn-equiv/trans (cn-equiv/equiv (kd-equiv/symm (kd-equiv/trans (kd-equiv/trans (kd-equiv/symm DequivK2) DequivK) DequivK1)) (cn-equiv/symm DequivC2b)) (cn-equiv/equiv (kd-equiv/symm DequivK1) DequivCb)) DequivC1b) <- cn-equiv-reg Dequiv (Dof1 : cn-of (rec K1 C1a C1b) t) (Dof2 : cn-of (rec K2 C2a C2b) t) _ <- inversion-rec Dof1 (DwfK1 : kd-wf K1) (DofC1a : {a} cn-of a (pi K1 ([_] t)) -> {b} cn-of b K1 -> cn-of (C1a a b) t) (DofC1b : cn-of C1b K1) <- inversion-rec Dof2 (DwfK2 : kd-wf K2) (DofC2a : {a} cn-of a (pi K2 ([_] t)) -> {b} cn-of b K2 -> cn-of (C2a a b) t) (DofC2b : cn-of C2b K2) <- map-equiv Dequiv (map/rec (Dflay1 : flay A1 SK1 MA1) (DmapC1b : map C1b M1b) (DmapC1a : {a} {x} map a x -> {b} {y} map b y -> map (C1a a b) (M1a x y)) (DmapK1 : tmap K1 A1)) (map/rec (Dflay2 : flay A2 SK2 MA2) (DmapC2b : map C2b M2b) (DmapC2a : {a} {x} map a x -> {b} {y} map b y -> map (C2a a b) (M2a x y)) (DmapK2 : tmap K2 A2)) tmap/t (Dequiv' : equiv (eapp (econst (const/rec SK1)) (epair MA1 (epair (elam (epi A1 ([_] et)) ([x] elam A1 ([y] M1a x y))) M1b))) (eapp (econst (const/rec SK2)) (epair MA2 (epair (elam (epi A2 ([_] et)) ([x] elam A2 ([y] M2a x y))) M2b))) et) <- can-skof SK1 (Dskof1 : skof SK1 D1 E1) <- skof-implies-cskof Dskof1 (Dcskof1 : cskof SK1 D1c E1c) (DopenD1 : etopen D1c D1) (DskelD1 : etp-skel D1 D1s) (DopenE1 : {xc} {x} etopenr xc D1s x -> etopen (E1c xc) (E1 x)) <- ({x} can-etp-skel (E1 x) (DskelE1 x)) <- can-skof SK2 (Dskof2 : skof SK2 D2 E2) <- skof-implies-cskof Dskof2 (Dcskof2 : cskof SK2 D2c E2c) (DopenD2 : etopen D2c D2) (DskelD2 : etp-skel D2 D2s) (DopenE2 : {xc} {x} etopenr xc D2s x -> etopen (E2c xc) (E2 x)) <- ({x} can-etp-skel (E2 x) (DskelE2 x)) <- unary-equiv-head (ekof/i (etopen-rec _ _ _ _ _ _ DopenD2 DskelD2 DopenE2 DskelE2) (ckof/rec Dcskof2)) (ekof/i (etopen-rec _ _ _ _ _ _ DopenD1 DskelD1 DopenE1 DskelE1) (ckof/rec Dcskof1)) (equiv/symm Dequiv') %% (DeqConst : constant-eq (const/rec SK2) (const/rec SK1)) <- constant-eq-cdr-rec DeqConst (DeqSK : skel-eq SK2 SK1) <- eterm-resp-skel ([SK] eapp (econst (const/rec SK)) (epair MA2 (epair (elam (epi A2 ([_] et)) ([x] elam A2 ([y] M2a x y))) M2b))) DeqSK DeqTerm <- equiv-resp eterm-eq/i DeqTerm etp-eq/i Dequiv' (Dequiv'' : equiv (eapp (econst (const/rec SK1)) (epair MA1 (epair (elam (epi A1 ([_] et)) ([x] elam A1 ([y] M1a x y))) M1b))) (eapp (econst (const/rec SK1)) (epair MA2 (epair (elam (epi A2 ([_] et)) ([x] elam A2 ([y] M2a x y))) M2b))) et) <- unary-equiv-inversion (ekof/i (etopen-rec _ _ _ _ _ _ DopenD1 DskelD1 DopenE1 DskelE1) (ckof/rec Dcskof1)) Dequiv'' %% (Dequiv''' : equiv (epair MA1 (epair (elam (epi A1 ([m:eterm] et)) ([x:eterm] elam A1 ([y:eterm] M1a x y))) M1b)) (epair MA2 (epair (elam (epi A2 ([m:eterm] et)) ([x:eterm] elam A2 ([y:eterm] M2a x y))) M2b)) (esigma D1 ([m:eterm] esigma (epi (epi (E1 m) ([m1:eterm] et)) ([m1:eterm] epi (E1 m) ([m2:eterm] et))) ([m1:eterm] E1 m)))) <- epair-equiv-invert Dequiv''' (DequivMA : equiv MA1 MA2 D1) (Dequiv'''' : equiv (epair (elam (epi A1 ([m:eterm] et)) ([x:eterm] elam A1 ([y:eterm] M1a x y))) M1b) (epair (elam (epi A2 ([m:eterm] et)) ([x:eterm] elam A2 ([y:eterm] M2a x y))) M2b) (esigma (epi (epi (E1 MA1) ([m1:eterm] et)) ([m1:eterm] epi (E1 MA1) ([m2:eterm] et))) ([m1:eterm] E1 MA1))) <- epair-equiv-invert Dequiv'''' (DequivLam : equiv (elam (epi A1 ([m:eterm] et)) ([x:eterm] elam A1 ([y:eterm] M1a x y))) (elam (epi A2 ([m:eterm] et)) ([x:eterm] elam A2 ([y:eterm] M2a x y))) (epi (epi (E1 MA1) ([_] et)) ([_] epi (E1 MA1) ([_] et)))) (DequivMb : equiv M1b M2b (E1 MA1)) <- map-wf' DwfK1 DmapK1 (DwfA1 : ewf A1) <- flay-sound DwfA1 Dflay1 Dskof1 (DofMA1 : eof MA1 D1) (DequivA1 : tequiv A1 (E1 MA1)) <- map-wf' DwfK2 DmapK2 (DwfA2 : ewf A2) <- flay-sound DwfA2 Dflay2 Dskof2 (DofMA2 : eof MA2 D2) (DequivA2 : tequiv A2 (E2 MA2)) <- elam2-equiv-invert (equiv/equiv (tequiv/symm (tequiv/pi ([_] [_] tequiv/pi ([_] [_] tequiv/t) DequivA1) (tequiv/pi ([_] [_] tequiv/t) DequivA1))) DequivLam) _ _ _ _ (DequivMa : {x} evof x (epi A1 ([_] et)) -> {y} evof y A1 -> equiv (M1a x y) (M2a x y) et) <- skof-reg Dskof1 (DwfD1 : ewf D1) (DwfE1 : {x} evof x D1 -> ewf (E1 x)) <- skof-resp DeqSK etp-eq/i ([_] etp-eq/i) Dskof2 (Dskof2' : skof SK1 D2 E2) <- skof-fun Dskof2' Dskof1 (DeqD : etp-eq D2 D1) (DeqE : {x} etp-eq (E2 x) (E1 x)) <- tfunctionality DwfE1 DequivMA (DequivEMA : tequiv (E1 MA1) (E1 MA2)) <- tequiv-resp etp-eq/i (DeqE MA2) DequivA2 (DequivA2' : tequiv A2 (E1 MA2)) <- invert-tmap DwfK1 DmapK1 (DmapA1 : tunmap A1 K1') (DequivK1 : kd-equiv K1 K1') <- invert-tmap DwfK2 DmapK2 (DmapA2 : tunmap A2 K2') (DequivK2 : kd-equiv K2 K2') <- unmap-tequiv (tequiv/trans (tequiv/trans (tequiv/symm DequivA2') DequivEMA) DequivA1 : tequiv A1 A2) DmapA1 DmapA2 (DequivK : kd-equiv K1' K2') <- ({a} {da:cn-of a (pi K1 ([_] t))} {das} mcn-assm da das -> cn-of-reg da (kd-wf/pi ([_] [_] kd-wf/t) DwfK1) -> {x} {dx:evof x (epi A1 ([_] et))} {at} {xt} can-map a at -> map-of da at (tmap/pi ([_] [_] [_] tmap/t) DmapK1) (eof/var (ewf/pi ([_] [_] ewf/t) DwfA1) dx) -> can-unmap x xt -> unmap-vof dx xt (tunmap/pi ([_] [_] [_] tunmap/t) DmapA1) (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK1) da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da (tmap/pi ([_] [_] [_] tmap/t) DmapK1) (tunmap/pi ([_] [_] [_] tunmap/t) DmapA1) (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK1) %% -> {b} {db:cn-of b K1} {dbs} mcn-assm db dbs -> cn-of-reg db DwfK1 -> {y} {dy:evof y A1} {bt} {yt} can-map b bt -> map-of db bt DmapK1 (eof/var DwfA1 dy) -> can-unmap y yt -> unmap-vof dy yt DmapA1 (cn-of/equiv DequivK1 db) -> invert-map db bt yt (cn-equiv/refl db) -> invert-tmap-cn-of' db DmapK1 DmapA1 DequivK1 %% -> invert-map (DofC1a a da b db) (DmapC1a a x at b y bt) (DmapM1a x a xt y b yt : unmap (M1a x y) (C1a' a b)) (DequivC1a a da b db : cn-equiv (C1a a b) (C1a' a b) t)) <- ({a} {da:cn-of a (pi K2 ([_] t))} {das:cn-assm da} mcn-assm da das -> cn-of-reg da (kd-wf/pi ([_] [_] kd-wf/t) DwfK2) -> {x} {dx:evof x (epi A2 ([_] et))} {at} {xt} can-map a at -> map-of da at (tmap/pi ([_] [_] [_] tmap/t) DmapK2) (eof/var (ewf/pi ([_] [_] ewf/t) DwfA2) dx) -> can-unmap x xt -> unmap-vof dx xt (tunmap/pi ([_] [_] [_] tunmap/t) DmapA2) (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK2) da) -> invert-map da at xt (cn-equiv/refl da) -> invert-tmap-cn-of' da (tmap/pi ([_] [_] [_] tmap/t) DmapK2) (tunmap/pi ([_] [_] [_] tunmap/t) DmapA2) (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK2) %% -> {b} {db:cn-of b K2} {dbs} mcn-assm db dbs -> cn-of-reg db DwfK2 -> {y} {dy:evof y A2} {bt} {yt} can-map b bt -> map-of db bt DmapK2 (eof/var DwfA2 dy) -> can-unmap y yt -> unmap-vof dy yt DmapA2 (cn-of/equiv DequivK2 db) -> invert-map db bt yt (cn-equiv/refl db) -> invert-tmap-cn-of' db DmapK2 DmapA2 DequivK2 %% -> invert-map (DofC2a a da b db) (DmapC2a a x at b y bt) (DmapM2a x a xt y b yt : unmap (M2a x y) (C2a' a b)) (DequivC2a a da b db : cn-equiv (C2a a b) (C2a' a b) t)) <- ({a} {da:cn-of a (pi K1 ([_] t))} {das} mcn-assm da das -> cn-of-reg da (kd-wf/pi ([_] [_] kd-wf/t) DwfK1) -> {x} {dx} {at} {xt} can-map a at -> map-of da at (tmap/pi ([_] [_] [_] tmap/t) DmapK1) (eof/var (ewf/pi ([_] [_] ewf/t) DwfA1) dx) -> can-unmap x xt -> unmap-vof dx xt (tunmap/pi ([_] [_] [_] tunmap/t) DmapA1) (cn-of/equiv (kd-equiv/pi ([_] [_] kd-equiv/t) DequivK1) da) %% -> {b} {db:cn-of b K1} {dbs} mcn-assm db dbs -> cn-of-reg db DwfK1 -> {y} {dy} {bt} {yt} can-map b bt -> map-of db bt DmapK1 (eof/var DwfA1 dy) -> can-unmap y yt -> unmap-vof dy yt DmapA1 (cn-of/equiv DequivK1 db) %% -> unmap-equiv' (DmapM1a x a xt y b yt) (DmapM2a x a xt y b yt) (DequivMa x dx y dy) tunmap/t (DequivCa a da b db : cn-equiv (C1a' a b) (C2a' a b) t)) <- invert-map DofC1b DmapC1b (DmapM1b : unmap M1b C1b') (DequivC1b : cn-equiv C1b C1b' K1) <- invert-map DofC2b DmapC2b (DmapM2b : unmap M2b C2b') (DequivC2b : cn-equiv C2b C2b' K2) <- unmap-equiv' DmapM1b DmapM2b (equiv/equiv (tequiv/symm DequivA1) DequivMb : equiv M1b M2b A1) DmapA1 (DequivCb : cn-equiv C1b' C2b' K1'). %worlds () (injective-rec _ _ _ _). %total {} (injective-rec _ _ _ _). injective-labeled : cn-equiv (labeled L1 T1) (labeled L2 T2) t %% -> label-eq L1 L2 -> cn-equiv T1 T2 t -> type. %mode injective-labeled +X1 -X2 -X3. injective-labeled-eq : label-eq L1 L2 -> equiv (eapp (econst (const/labeled L1)) M1) (eapp (econst (const/labeled L2)) M2) et %% -> equiv (eapp (econst (const/labeled L1)) M1) (eapp (econst (const/labeled L1)) M2) et -> type. %mode injective-labeled-eq +X1 +X2 -X3. - : injective-labeled (Dequiv : cn-equiv (labeled L1 T1) (labeled L2 T2) t) %% DeqL (cn-equiv/trans (cn-equiv/trans (cn-equiv/symm Dequiv2) Dequiv') Dequiv1) <- cn-equiv-reg Dequiv (Dof1 : cn-of (labeled L1 T1) t) (Dof2 : cn-of (labeled L2 T2) t) _ <- inversion-labeled Dof1 (Dof1' : cn-of T1 t) <- inversion-labeled Dof2 (Dof2' : cn-of T2 t) <- can-map _ (Dmap1 : map T1 M1) <- can-map _ (Dmap2 : map T2 M2) <- map-equiv'' (map/labeled Dmap1) (map/labeled Dmap2) Dequiv tmap/t (DequivSing : equiv (eapp (econst (const/labeled L1)) M1) (eapp (econst (const/labeled L2)) M2) et) <- unary-equiv-head (ekof/i etopen/tt ckof/labeled) (ekof/i etopen/tt ckof/labeled) DequivSing %% (DeqConst : constant-eq (const/labeled L1) (const/labeled L2)) <- constant-eq-cdr-labeled DeqConst (DeqL : label-eq L1 L2) <- injective-labeled-eq DeqL DequivSing (DequivSing' : equiv (eapp (econst (const/labeled L1)) M1) (eapp (econst (const/labeled L1)) M2) et) <- unary-equiv-inversion (ekof/i etopen/tt ckof/labeled) DequivSing' (DequivSing'' : equiv M1 M2 et) <- invert-map Dof1' Dmap1 (Dunmap1 : unmap M1 T1') (Dequiv1 : cn-equiv T1 T1' t) <- invert-map Dof2' Dmap2 (Dunmap2 : unmap M2 T2') (Dequiv2 : cn-equiv T2 T2' t) <- unmap-equiv Dunmap1 Dunmap2 DequivSing'' tunmap/t (Dequiv' : cn-equiv T1' T2' t). - : injective-labeled-eq _ D D. %worlds () (injective-labeled-eq _ _ _). %total {} (injective-labeled-eq _ _ _). %worlds () (injective-labeled _ _ _). %total {} (injective-labeled _ _ _).