theory Bool_HoTT
imports
  MLTT.Prelude
  Propositions

begin

end