 Zipperposition (Bentkamp et al. 2018) is new and inspiring higher-order theorem prover which, at the current state of development, is still working for a comparably weak fragment of Church’s type theory, called lambda-free higher-order logic (a comprehension-free higher-order logic, which is nevertheless supporting λ-notation). The system, which is based on superposition calculi, is developed bottom up, and it is progressively extended towards stronger fragments of Church’s type theory and to support other relevant extensions such datatypes, recursive functions and arithmetic. 