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)