Transport over Bool.not

Bools.ard

\data Bool1 | tt1 | ff1 \where {
  \func to2 (b : Bool1) : Bool2
    | tt1 => Bool2.tt2
    | ff1 => Bool2.ff2
  \lemma lemma (b : Bool1) : Bool2.to1 (to2 b) = b
    | tt1 => idp
    | ff1 => idp
}
\data Bool2 | tt2 | ff2 \where {
  \func to1 (b : Bool2) : Bool1
    | tt2 => Bool1.tt1
    | ff2 => Bool1.ff1
  \lemma lemma (b : Bool2) : Bool1.to2 (to1 b) = b
    | tt2 => idp
    | ff2 => idp
}

\func not1 (b : Bool1) : Bool1
  | tt1 => ff1
  | ff1 => tt1
\func path => iso Bool1.to2 Bool2.to1 Bool1.lemma Bool2.lemma
\func not2 => coe (\lam i => path i -> path i) not1 right