Add conical properties for and and or

Author: MatthewDaggitt

CHANGELOG.md

@@ -1800,6 +1800,12 @@ Other minor changes
 * Added new proofs in `Data.Bool.Properties`:
   ```agda
   <-wellFounded : WellFounded _<_
+  ∨-conicalˡ : LeftConical false _∨_
+  ∨-conicalʳ : RightConical false _∨_
+  ∨-conical : Conical false _∨_
+  ∧-conicalˡ : LeftConical true _∧_
+  ∧-conicalʳ : RightConical true _∧_
+  ∧-conical : Conical true _∧_
   ```
 
 * Added new functions in `Data.Fin.Base`:

src/Data/Bool/Properties.agda

@@ -273,6 +273,15 @@ true  <? _     = no  (λ())
 ∨-sel false y = inj₂ refl
 ∨-sel true y  = inj₁ refl
 
+∨-conicalˡ : LeftConical false _∨_
+∨-conicalˡ false false _ = refl
+
+∨-conicalʳ : RightConical false _∨_
+∨-conicalʳ false false _ = refl
+
+∨-conical : Conical false _∨_
+∨-conical = ∨-conicalˡ , ∨-conicalʳ
+
 ∨-isMagma : IsMagma _∨_
 ∨-isMagma = record
   { isEquivalence = isEquivalence
@@ -397,6 +406,15 @@ true  <? _     = no  (λ())
 ∧-sel false y = inj₁ refl
 ∧-sel true y  = inj₂ refl
 
+∧-conicalˡ : LeftConical true _∧_
+∧-conicalˡ true true _ = refl
+
+∧-conicalʳ : RightConical true _∧_
+∧-conicalʳ true true _ = refl
+
+∧-conical : Conical true _∧_
+∧-conical = ∧-conicalˡ , ∧-conicalʳ
+
 ∧-distribˡ-∨ : _∧_ DistributesOverˡ _∨_
 ∧-distribˡ-∨ true  y z = refl
 ∧-distribˡ-∨ false y z = refl