You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
74 lines
3.5 KiB
74 lines
3.5 KiB
let Id : (A : Type) -> A -> A -> Type = \A x y -> Path (\i -> A) x y in
|
|
let the : (A : Type) -> A -> A = \A x -> x in
|
|
let
|
|
fill : (i : I) (A : I -> Type)
|
|
(phi : I) (u : (i : I) -> Partial phi (A i))
|
|
-> Sub (A i0) phi (u i0) -> A i
|
|
= \i A phi u a0 ->
|
|
comp (\j -> A (i && j)) (phi || ~i) (\j -> [ phi -> u (i && j), ~i -> a0 ]) a0
|
|
in let
|
|
trans : (A : Type) (a b c : A)
|
|
-> Path (\i -> A) a b
|
|
-> Path (\i -> A) b c
|
|
-> Path (\i -> A) a c
|
|
= \A a b c p q i ->
|
|
comp (\j -> A) (i || ~i)
|
|
(\j -> [ ~i -> a, i -> q j ])
|
|
(p i)
|
|
in
|
|
let isContr : Type -> Type
|
|
= \A -> (x : A) * (y : A) -> Path (\i -> A) x y in
|
|
let fiber : (T A : Type) -> (T -> A) -> A -> Type
|
|
= \T A f y -> (x : T) * Path (\i -> A) y (f x) in
|
|
let isEquiv : (T A : Type) -> (T -> A) -> Type
|
|
= \T A f -> (y : A) -> isContr (fiber T A f y) in
|
|
let idFun : (B : Type) -> B -> B = \A x -> x in
|
|
let idEquiv : (B : Type) -> isEquiv B B (idFun B)
|
|
= \B y -> ((y, \i -> y), \u -> \i -> (u.2 i, \j -> u.2 (i && j))) in
|
|
let equiv : (A B : Type) -> Type
|
|
= \A B -> (f : A -> B) * isEquiv A B f in
|
|
let
|
|
univalence : (A B : Type) -> equiv A B -> Path (\i -> Type) A B
|
|
= \A B fun i -> Glue B (i || ~i) [~i -> A, i -> B] [~i -> fun, i -> (idFun B, idEquiv B)]
|
|
in
|
|
let idToEquiv : (A B : Type) -> Path (\i -> Type) A B -> equiv A B
|
|
= \A B p -> comp (\i -> equiv A (p i)) i0 (\i -> []) (idFun A,
|
|
idEquiv A)
|
|
in
|
|
let transp : (A B : Type) (p : Path (\i -> Type) A B) -> A -> B = \A B p -> comp (\i -> p i) i0 (\j -> []) in
|
|
let
|
|
univalenceBeta : (A B : Type) (f : equiv A B)
|
|
-> Id (A -> B) (transp A B (univalence A B f)) f.1
|
|
= \A B f i a ->
|
|
let b : B = transp B B (\i -> B) (f.1 a) in
|
|
let rem1 : Id B b (f.1 a) = \i -> fill ~i (\i -> B) i0 (\j -> []) (f.1 a) in
|
|
let rem2 : Id B (transp B B (\i -> B) b) b = \i -> fill ~i (\i -> B) i0 (\j -> []) b in
|
|
let goal : Id B (transp B B (\i -> B) b) (f.1 a) =
|
|
trans B (transp B B (\i -> B) b) b (f.1 a) rem2 rem1
|
|
in goal i
|
|
in
|
|
|
|
let not : Bool -> Bool = if (\x -> Bool) ff tt in
|
|
|
|
let notInv : (b : Bool) -> Id Bool b (not (not b)) = if (\x -> Id Bool x (not (not x))) (\i -> tt) (\i -> ff) in
|
|
|
|
let trueNotFalse : (A : Type) -> Id Bool tt ff -> A =
|
|
\A p -> comp (\i -> if (\b -> Type) (A -> A) A (p i)) i0 (\j -> []) (\x -> x) in
|
|
|
|
let notEquiv : isEquiv Bool Bool not =
|
|
let contract1 : (a : Bool) (b : Path (\i -> Bool) tt (not a)) -> Path (\i -> fiber Bool Bool not tt) (ff, \i -> tt) (a, b)
|
|
= \a -> if (\a -> (b : Path (\i -> Bool) tt (not a)) -> Path (\i -> fiber Bool Bool not tt) (ff, \i -> tt) (a, b))
|
|
(\b -> trueNotFalse (Path (\i -> fiber Bool Bool not tt) (ff, \i -> tt) (tt, b)) b)
|
|
(\b i -> (ff, \j -> b (i && j)))
|
|
a in
|
|
let contract2 : (a : Bool) (b : Path (\i -> Bool) ff (not a)) -> Path (\i -> fiber Bool Bool not ff) (tt, \i -> ff) (a, b) =
|
|
\a -> if (\a -> (b : Path (\i -> Bool) ff (not a)) -> Path (\i -> fiber Bool Bool not ff) (tt, \i -> ff) (a, b))
|
|
(\b i -> (tt, \j -> b (i && j)))
|
|
(\b -> trueNotFalse (Path (\i -> fiber Bool Bool not ff) (tt, \i -> ff) (ff, b)) (\j -> b ~j))
|
|
a in
|
|
\b -> if (\b -> isContr (fiber Bool Bool not b))
|
|
((ff, \i -> tt), \fiber -> contract1 fiber.1 fiber.2)
|
|
((tt, \i -> ff), \fiber -> contract2 fiber.1 fiber.2)
|
|
b
|
|
|
|
in the (Id Bool (not ff) tt) (\i -> transp Bool Bool (univalence Bool Bool (not, notEquiv)) ff)
|