Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Generic combinator for injectivity proofs.
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality
open import Data.Maybe
open import Function
cong⁻¹ : {A B : Set} {a a'} (f : A Maybe B)
(eq : a ≡ a')
from-just (f a) ≅ from-just (f a')
cong⁻¹ {a = a} f refl = refl
data A : Set where
C : A A
D : A A A
C-injective : {a b} C a ≡ C b a ≅ b
C-injective = cong⁻¹ λ { (C a) just a; _ nothing }
D₁-injective : {a b c} D a b ≡ D b c a ≅ b
D₁-injective = cong⁻¹ λ { (D a _) just a; _ nothing }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment