Generic combinator for injectivity proofs.

generic-injective.agda

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 }