proofs: make all modules pass the strict flag set

src/EpistemicTypes/EchoBridge.agda

@@ -165,8 +165,8 @@ data _≤G_ : Grade -> Grade -> Set where
   top≤    : {g : Grade} -> g ≤G infinity
 
 ≤G-trans : {a b c : Grade} -> a ≤G b -> b ≤G c -> a ≤G c
+≤G-trans _ top≤ = top≤
 ≤G-trans (finite≤ p) (finite≤ q) = finite≤ (≤ℕ-trans p q)
-≤G-trans p top≤ = top≤
 
 ≤G-plus : (a b : Grade) -> a ≤G gradePlus a b
 ≤G-plus (finite a) (finite b) = finite≤ (≤ℕ-plus a b)

src/EpistemicTypes/Kripke/Residual.agda

@@ -45,8 +45,14 @@ E _ = ⊤
 -- "Thing x is here": true only at world x.
 Is : W → W → Set
 Is a a = ⊤
+Is a b = ⊥
+Is a c = ⊥
+Is b a = ⊥
 Is b b = ⊤
-Is _ _ = ⊥
+Is b c = ⊥
+Is c a = ⊥
+Is c b = ⊥
+Is c c = ⊥
 
 Present : W → Set
 Present w = Σ W (λ x → Is x w)

src/EpistemicTypes/ProofTransportExample.agda

@@ -28,9 +28,9 @@ Payload _ _ = Bool
 open import EpistemicTypes.ProofTransport Agent Claim Artifact Meaning Payload
 
 checkPayload : (a : Artifact) -> (c : Claim) -> Payload a c -> Bool
+checkPayload _ ImpossibleClaim _ = false
 checkPayload true ArtifactIsTrue p = p
 checkPayload false ArtifactIsTrue _ = false
-checkPayload _ ImpossibleClaim _ = false
 
 checkPayloadSound :
   (holder : Agent) (a : Artifact) (c : Claim) (p : Payload a c) ->