### Abstract

Pseudo-hoops are algebraic structures introduced by B. Bosbach under the name of complementary semigroups. In this formalization we prove some properties of pseudo-hoops and we define the basic concepts of filter and normal filter. The lattice of normal filters is isomorphic with the lattice of congruences of a pseudo-hoop. We also study some important classes of pseudo-hoops. Bounded Wajsberg pseudo-hoops are equivalent to pseudo-Wajsberg algebras and bounded basic pseudo-hoops are equivalent to pseudo-BL algebras. Some examples of pseudo-hoops are given in the last section of the formalization.

### License

### Topics

### Session PseudoHoops

- Operations
- LeftComplementedMonoid
- RightComplementedMonoid
- PseudoHoops
- PseudoHoopFilters
- PseudoWaisbergAlgebra
- SpecialPseudoHoops
- Examples