fact: Record Algebra {σ : Signature} : Type := Build_Algebra { carriers : Carriers σ ; operations : forall (u : Symbol σ), Operation carriers (σ u) ; hset_algebra : forall (s : Sort σ), IsHSet (carriers s) }.
imports: HoTT.Basics HoTT.Types HoTT.HSet