let XNor = ./Type

in  λ(a : Type) →
    λ(ea : ../Eq/Type a) →
    λ(b : Type) →
    λ(eb : ../Eq/Type b) →
        { eq =
            λ(x : XNor a b) →
            λ(y : XNor a b) →
              merge
                { Both =
                    λ(xx : { head : a, tail : b }) →
                      merge
                        { Both =
                            λ(yy : { head : a, tail : b }) →
                              ea.eq xx.head yy.head && eb.eq xx.tail yy.tail
                        , Neither = False
                        }
                        y
                , Neither =
                    merge
                      { Both = λ(yy : { head : a, tail : b }) → False
                      , Neither = True
                      }
                      y
                }
                x
        }
      : ../Eq/Type (XNor a b)