(VPi u v,VPi u' v') ->
let w@(VVar n _) = mkVarNice ns "X" u
in conv ns u u' && conv (n:ns) (app v w) (app v' w)
(VSigma u v,VSigma u' v') ->
let w@(VVar n _) = mkVarNice ns "X" u
in conv ns u u' && conv (n:ns) (app v w) (app v' w)
(VCon c us,VCon c' us') -> (c == c') && conv ns us us'
(VPCon c v us phis,VPCon c' v' us' phis') ->
(c == c') && conv ns (v,us,phis) (v',us',phis')
(VPair u v,VPair u' v') -> conv ns u u' && conv ns v v'
(VPair u v,w) -> conv ns u (fstVal w) && conv ns v (sndVal w)
(w,VPair u v) -> conv ns (fstVal w) u && conv ns (sndVal w) v
(VFst u,VFst u') -> conv ns u u'
(VSnd u,VSnd u') -> conv ns u u'
(VApp u v,VApp u' v') -> conv ns u u' && conv ns v v'
(VSplit u v,VSplit u' v') -> conv ns u u' && conv ns v v'
(VOpaque x _, VOpaque x' _) -> x == x'
(VVar x _, VVar x' _) -> x == x'
(VPathP a b c,VPathP a' b' c') -> conv ns a a' && conv ns b b' && conv ns c c'
(VPLam i a,VPLam i' a') -> conv ns (a `C.swap` (i,j)) (a' `C.swap` (i',j))
(VPLam i a,p') -> conv ns (a `C.swap` (i,j)) (p' @@ j)
(p,VPLam i' a') -> conv ns (p @@ j) (a' `C.swap` (i',j))
(VAppFormula u x,VAppFormula u' x') -> conv ns (u,x) (u',x')
(VComp a u ts,VComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts')
(VHComp a u ts,VHComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts')
(VGlue v equivs,VGlue v' equivs') -> conv ns (v,equivs) (v',equivs')
(VGlueElem (VUnGlueElem b equivs) ts,g) -> conv ns (C.border b equivs,b) (ts,g)
(g,VGlueElem (VUnGlueElem b equivs) ts) -> conv ns (C.border b equivs,b) (ts,g)
(VGlueElem (VUnGlueElemU b _ equivs) ts,g) -> conv ns (C.border b equivs,b) (ts,g)
(g,VGlueElem (VUnGlueElemU b _ equivs) ts) -> conv ns (C.border b equivs,b) (ts,g)
(VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us')
(VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u'
(VUnGlueElem u _,VUnGlueElem u' _) -> conv ns u u'
(VCompU u es,VCompU u' es') -> conv ns (u,es) (u',es')
(VIdPair v vs,VIdPair v' vs') -> conv ns (v,vs) (v',vs')
(VId a u v,VId a' u' v') -> conv ns (a,u,v) (a',u',v')
(VIdJ a u c d x p,VIdJ a' u' c' d' x' p') ->
conv ns [a,u,c,d,x,p] [a',u',c',d',x',p']
_ -> False
instance Convertible Ctxt where
conv _ _ _ = True
instance Convertible () where
conv _ _ _ = True
instance (Convertible a, Convertible b) => Convertible (a, b) where
conv ns (u, v) (u', v') = conv ns u u' && conv ns v v'
instance (Convertible a, Convertible b, Convertible c)
=> Convertible (a, b, c) where
conv ns (u, v, w) (u', v', w') = conv ns (u,(v,w)) (u',(v',w'))
instance (Convertible a,Convertible b,Convertible c,Convertible d)
=> Convertible (a,b,c,d) where
conv ns (u,v,w,x) (u',v',w',x') = conv ns (u,v,(w,x)) (u',v',(w',x'))
instance Convertible a => Convertible [a] where
conv ns us us' = length us == length us' &&
and [conv ns u u' | (u,u') <- zip us us']
instance Convertible a => Convertible (C.System a) where
conv ns ts ts' = keys ts == keys ts' &&
and (elems (intersectionWith (conv ns) ts ts'))
instance Convertible C.Formula where
conv _ phi psi = C.dnf phi == C.dnf psi
instance Convertible (C.Nameless a) where
conv _ _ _ = True