30 lines
790 B
Agda
30 lines
790 B
Agda
module hwk2 where
|
||
|
||
open import Data.Nat
|
||
open import Data.Sum
|
||
open import Data.Unit
|
||
open import Data.Empty
|
||
open import Relation.Binary.PropositionalEquality as Eq hiding (subst)
|
||
open Eq.≡-Reasoning
|
||
|
||
J : {A : Set}
|
||
→ (C : (x y : A) → x ≡ y → Set)
|
||
→ (c : (x : A) → C x x refl)
|
||
→ (x y : A) → (p : x ≡ y) → C x y p
|
||
J C c x x refl = c x
|
||
|
||
subst : {A : Set} {a b : A}
|
||
→ (P : A → Set)
|
||
→ (c : a ≡ b)
|
||
→ (p : P a)
|
||
→ P b
|
||
subst {A} {a} {b} P c = J (λ x y p → (P x → P y)) (λ x → (λ a → a)) a b c
|
||
|
||
discriminate : {A : Set} {B : Set} → (s : A ⊎ B) → Set
|
||
discriminate (inj₁ x) = ⊤
|
||
discriminate (inj₂ y) = ⊥
|
||
|
||
problem2 : {A : Set} {B : Set}
|
||
→ (a : A) → (b : B)
|
||
→ inj₁ a ≢ inj₂ b
|
||
problem2 a b p = subst discriminate p tt |