class LO.InterpretabilityLogicalConnective (F : Type u_1) extends LO.BasicModalLogicalConnective F, LO.Rhd F : Type u_1

• top : F
• bot : F
• tilde : F → F
• arrow : F → F → F
• wedge : F → F → F
• vee : F → F → F
• box : F → F
• dia : F → F
• rhd : F → F → F