fact: Record Signature := Build_Signature { Sort : Type ; Symbol : Type ; symbol_types : Symbol -> SymbolTypeOf Sort ; hset_sort : IsHSet Sort ; hset_symbol : IsHSet Symbol }.
imports: HoTT.Basics HoTT.Types HoTT.HSet