Agda-2.3.2.2: test/bugs/univ.agda
{-# OPTIONS --disable-positivity-check #-}
module univ where
import Logic.ChainReasoning
module Chain {A : Set}
( _==_ : A -> A -> Set)
(refl : {x : A} -> x == x)
(trans : {x y z : A} -> x == y -> y == z -> x == z) =
Logic.ChainReasoning.Mono.Homogenous _==_ (\x -> refl) (\x y z -> trans)
data N1 : Set where
T : N1
data N0 : Set where
data Sigma (A:Set)(B : A -> Set) : Set where
Pair : (x:A) -> B x -> Sigma A B
rel : Set -> Set1
rel A = A -> A -> Set
pred : Set -> Set1
pred A = A -> Set
Refl : {A:Set} -> rel A -> Set
Refl {A} R = {x : A} -> R x x
Sym : {A:Set} -> rel A -> Set
Sym {A} R = {x y : A} -> R x y -> R y x
Trans : {A:Set} -> rel A -> Set
Trans {A} R = {x y z : A} -> R x y -> R y z -> R x z
Map : (A:Set) -> rel A -> (B:Set) -> rel B -> pred (A -> B)
Map A _R_ B _S_ f = {x y : A} -> x R y -> f x S f y
postulate
N : Set
_=N_ : rel N
refN : Refl _=N_
symN : Sym _=N_
transN : Trans _=N_
-- mutual inductive recursive definition of S and the functions _=S_, El, eq, and all the
-- proofs on these functions
mutual
infix 40 _==_ _=S_
infixr 80 _<<_
data S : Set where
nat : S
pi : (A:S) -> (f:El A -> S) -> Map (El A) _==_ S _=S_ f -> S
_=S'_ : rel S
nat =S' nat = N1
nat =S' pi A f pf = N0
pi _ _ _ =S' nat = N0
pi A F pF =S' pi B G pG =
Sigma (A =S B) \ A=B -> (x : El B) -> F (A=B << x) =S G x
data _=S_ (A B : S) : Set where
eqS : A =S' B -> A =S B
El' : S -> Set
El' nat = N
El' (pi A F pF) =
Sigma ((x : El A) -> El (F x))
\f -> {x y : El A}(x=y : x == y) ->
f x == pF x=y << f y
data El (A : S) : Set where
el : El' A -> El A
_=='_ : {A : S} -> rel (El A)
_=='_ {nat} (el x) (el y) = x =N y
_=='_ {pi A F pF} (el (Pair f pf)) (el (Pair g pg)) =
(x : El A) -> f x == g x
data _==_ {A : S}(x y : El A) : Set where
eq : x ==' y -> x == y
_<<_ : {A B : S} -> A =S B -> El B -> El A
_<<_ {nat} {nat} p x = x
_<<_ {pi A F pF} {pi B G pG} (eqS (Pair A=B F=G)) (el (Pair g pg)) =
el (Pair f (\{x}{y} -> pf x y))
where
B=A = symS A=B
F=Gc : (x : El A) -> F x =S G (B=A << x)
F=Gc x =
transS (transS refS (symS (pF (castlem A=B (symS A=B) x))))
(F=G (symS A=B << x))
-- chain> F x
-- === F (A=B << B=A << x) by symS (pF (castlem A=B B=A x))
-- === G (B=A << x) by F=G (B=A << x)
-- where
-- open module C = Chain _=S_ refS transS
f : (x : El A) -> El (F x)
f x = F=Gc x << g (B=A << x)
pf : (x y : El A)(p : x == y) -> f x == pF p << f y
pf x y x=y = trans fx=ccgy ccgy=cfy
where
cx = B=A << x
cy = B=A << y
cx=cy : cx == cy
cx=cy = p<< B=A x=y
cgy : El (G cx)
cgy = pG cx=cy << g cy
gx=gy : g cx == cgy
gx=gy = pg cx=cy
ccgy : El (F x)
ccgy = F=Gc x << cgy
fx=ccgy : f x == ccgy
fx=ccgy = p<< (F=Gc x) gx=gy
cfy : El (F x)
cfy = pF x=y << f y
ccgy=cfy : ccgy == cfy
ccgy=cfy = castlem2 (F=Gc x) (pF x=y)
(pG cx=cy) (F=Gc y)
(g cy)
p<< : {A B : S}(A=B : A =S B) -> Map (El B) _==_ (El A) _==_ (_<<_ A=B)
p<< {nat}{nat} _ x=y = x=y
p<< {pi A F pF} {pi B G pG} (eqS (Pair A=B F=G))
{el (Pair f pf)} {el (Pair g pg)} (eq f=g) = eq cf=cg
where
open module C = Logic.ChainReasoning.Mono.Homogenous _=S_ (\x -> refS) (\x y z -> transS)
B=A = symS A=B
F=Gc : (x : El A) -> F x =S G (B=A << x)
F=Gc x =
chain> F x
=== F (A=B << B=A << x) by symS (pF (castlem A=B B=A x))
=== G (B=A << x) by F=G _
cf=cg : (x : El A) -> F=Gc x << f (B=A << x)
== F=Gc x << g (B=A << x)
cf=cg x = p<< (F=Gc x) (f=g (B=A << x))
p<< {nat} {pi _ _ _} (eqS ()) _
p<< {pi _ _ _} {nat} (eqS ()) _
refS : Refl _=S_
refS {nat} = eqS T
refS {pi A F pF} = eqS (Pair refS \(x : El A) -> pF (castref refS x))
transS : Trans _=S_
transS {nat}{nat}{nat} p q = p
transS {nat}{nat}{pi _ _ _} _ (eqS ())
transS {nat}{pi _ _ _}{_} (eqS ()) _
transS {pi _ _ _}{nat}{_} (eqS ()) _
transS {pi _ _ _}{pi _ _ _}{nat} _ (eqS ())
transS {pi A F pF}{pi B G pG}{pi C H pH}
(eqS (Pair A=B F=G)) (eqS (Pair B=C G=H)) =
eqS (Pair A=C F=H)
where
open module C = Chain _=S_ refS transS
A=C = transS A=B B=C
F=H : (x : El C) -> F (A=C << x) =S H x
F=H x =
chain> F (A=C << x)
=== F (A=B << B=C << x) by symS (pF (casttrans A=B B=C A=C x))
=== G (B=C << x) by F=G (B=C << x)
=== H x by G=H x
symS : Sym _=S_
symS {nat}{nat} p = p
symS {pi _ _ _}{nat} (eqS ())
symS {nat}{pi _ _ _} (eqS ())
symS {pi A F pF}{pi B G pg} (eqS (Pair A=B F=G)) = eqS (Pair B=A G=F)
where
open module C = Chain _=S_ refS transS
B=A = symS A=B
G=F : (x : El A) -> G (B=A << x) =S F x
G=F x =
chain> G (B=A << x)
=== F (A=B << B=A << x) by symS (F=G (B=A << x))
=== F x by pF (castlem A=B B=A x)
pfi : {A B : S}(p q : A =S B)(x : El B) -> p << x == q << x
pfi {nat}{nat} _ _ x = ref
pfi {nat}{pi _ _ _} (eqS ()) _ _
pfi {pi _ _ _}{nat} (eqS ()) _ _
pfi {pi A F pF}{pi B G pG} (eqS (Pair A=B1 F=G1)) (eqS (Pair A=B2 F=G2))
(el (Pair f pf)) = eq f1=f2
where
B=A1 = symS A=B1
B=A2 = symS A=B2
f1=f2 : (x : El A) -> _ << f (B=A1 << x) == _ << f (B=A2 << x)
f1=f2 x =
chain> _ << f (B=A1 << x)
=== _ << _ << f (B=A2 << x) by p<< _ lem2
=== _ << f (B=A2 << x) by casttrans _ _ _ _
where
open module C = Chain _==_ (ref {F x}) (trans {F x})
lem1 : B=A1 << x == B=A2 << x
lem1 = pfi B=A1 B=A2 x
lem2 : f (B=A1 << x) == _ << f (B=A2 << x)
lem2 = pf lem1
castref : {A : S}(p : A =S A)(x : El A) -> p << x == x
castref {nat} p x = ref
castref {pi A F pF} (eqS (Pair A=A F=F)) (el (Pair f pf)) = eq cf=f
where
A=A' = symS A=A
cf=f : (x : El A) -> _ << f (A=A' << x) == f x
cf=f x =
chain> Fx=Fcx << f (A=A' << x)
=== Fx=Fcx << _ << f x by p<< Fx=Fcx lem2
=== refS << f x by casttrans _ _ _ (f x)
=== f x by castref _ (f x)
where
Fx=Fcx = _
open module C = Chain _==_ (ref {F x}) (trans {F x})
lem1 : A=A' << x == x
lem1 = castref A=A' x
lem2 : f (A=A' << x) == _ << f x
lem2 = pf lem1
casttrans : {A B C : S}(A=B : A =S B)(B=C : B =S C)(A=C : A =S C)(x : El C) ->
A=B << B=C << x == A=C << x
casttrans {nat}{nat}{nat} _ _ _ x = ref
casttrans {nat}{nat}{pi _ _ _} _ (eqS ()) _ _
casttrans {nat}{pi _ _ _}{_} (eqS ()) _ _ _
casttrans {pi _ _ _}{nat}{_} (eqS ()) _ _ _
casttrans {pi _ _ _}{pi _ _ _}{nat} _ (eqS ()) _ _
casttrans {pi A F pF}{pi B G pG}{pi C H pH}
(eqS (Pair A=B F=G))(eqS (Pair B=C G=H))(eqS (Pair A=C F=H))
(el (Pair h ph)) = eq prf
where
B=A = symS A=B
C=B = symS B=C
C=A = symS A=C
prf : (x : El A) -> _ << _ << h (C=B << B=A << x) == _ << h (C=A << x)
prf x =
chain> Fx=Gcx << Gcx=Hccx << h (C=B << B=A << x)
=== Fx=Hccx << h (C=B << B=A << x) by casttrans _ _ _ _
=== Fx=Hccx << _ << h (C=A << x) by p<< _ (ph (casttrans C=B B=A C=A x))
=== Fx=Hcx << h (C=A << x) by casttrans _ _ _ _
where
Fx=Gcx = _
Gcx=Hccx = _
Fx=Hccx = transS (lemF=Gc A=B pF pG F=G _)
(lemF=Gc B=C pG pH G=H _)
Fx=Hcx = _
open module C = Chain _==_ (ref {F x}) (trans {F x})
lemF=Gc : {A B : S}(A=B : A =S B)
{F : El A -> S}(pF : Map (El A) _==_ S _=S_ F)
{G : El B -> S}(pG : Map (El B) _==_ S _=S_ G)
(F=G : (x : El B) -> F (A=B << x) =S G x)
(x : El A) -> F x =S G (symS A=B << x)
lemF=Gc A=B {F} pF {G} pG F=G x =
chain> F x
=== F (A=B << B=A << x) by symS (pF (castlem A=B B=A x))
=== G (B=A << x) by F=G _
where
open module C = Chain _=S_ refS transS
B=A = symS A=B
castlem : {A B : S}(p : A =S B)(q : B =S A)(x : El A) ->
p << q << x == x
castlem {A}{B} p q x =
chain> p << q << x
=== refS << x by casttrans p q refS x
=== x by castref refS x
where open module C = Chain _==_ (ref {A}) (trans {A})
castlem2 : {A B B' C : S}(A=B : A =S B)(A=B' : A =S B')(B=C : B =S C)(B'=C : B' =S C)
(x : El C) ->
A=B << B=C << x == A=B' << B'=C << x
castlem2 {A} p p' q q' x =
chain> p << q << x
=== transS p q << x by casttrans _ _ _ x
=== transS p' q' << x by pfi _ _ _
=== p' << q' << x by sym (casttrans _ _ _ x)
where open module C = Chain _==_ (ref {A}) (trans {A})
ref : {A:S} -> Refl {El A} _==_
ref {nat} {el n} = eq refN
ref {pi A F pF}{el (Pair f pf)} = eq f=f
where
f=f : (x : El A) -> f x == f x
f=f x = ref
trans : {A:S} -> Trans {El A} _==_
trans {nat}{el x}{el y}{el z} (eq p) (eq q) = eq (transN p q)
trans {pi A F pF}{el (Pair f pf)}{el (Pair g pg)}{el (Pair h ph)}
(eq f=g)(eq g=h) = eq f=h
where
f=h : (x : El A) -> f x == h x
f=h x = trans (f=g x) (g=h x)
sym : {A:S} -> Sym {El A} _==_
sym {nat}{el x}{el y} (eq p) = eq (symN p)
sym {pi A F pF}{el (Pair f pf)}{el (Pair g pg)}
(eq f=g) = eq g=f
where
g=f : (x : El A) -> g x == f x
g=f x = sym (f=g x)