(b1 b2 : DProp) : DProp := Build_DProp (b1 -> b2) _ _. Declare Scope dprop_scope. Delimit Scope dprop_scope with dprop. Bind Scope dprop_scope with DProp. Declare Scope dhprop_scope. Delimit Scope dhprop_scope with dhprop. Bind Scope dhprop_scope with DHProp. Infix "&&" := dand : dprop_scope. Infix "&&" := dhand : dhprop_scope. Infix "||" := dor : dprop_scope. Infix "||" := dhor : dhprop_scope. Infix "->" := : dprop_scope. Notation "!! P" := (dneg P) : dprop_scope. Local Open Scope dprop_scope. Class IsTrue (P : DProp) := dprop_istrue : P. Class IsFalse (P : DProp) := dprop_isfalse : ~ P. Global Instance true_istrue : IsTrue True := tt. Global Instance false_isfalse : IsFalse False := idmap. Global Instance dand_true_true {P Q} `{IsTrue P} `{IsTrue Q} : IsTrue (P && Q). Proof. exact (dprop_istrue, dprop_istrue). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HProp. Require Import Truncations.Core Modalities.ReflectiveSubuniverse.