Smart coproduct injections

Inj.agda

{-# OPTIONS --overlapping-instances #-}

record _<:_ (sub sup : Set) : Set where
  field
    inj : sub → sup

open import Function

open _<:_{{...}}

infixr 10 _+_ 
data _+_ (A B : Set) : Set where
  inl : A → A + B
  inr : B → A + B

instance
  _ : {A : Set} → A <: A
  _ = record { inj = id }

  _ : {A B : Set} → A <: (A + B)
  _ = record { inj = inl }

  _ : {A B C : Set}{{ _ : A <: B}} → A <: ( C + B)
  _ = record { inj = inr ∘ inj }


open import Data.Bool
open import Data.Nat hiding (_+_)
open import Data.String

_ : Bool + ℕ + String
_ = inj 8

_ : Bool + ℕ + String
_ = inj true

_ : Bool + ℕ + String
_ = inj "foo"

Coq

Class Inject (sub sup : Set) : Set :=
{
  inj : sub -> sup
}.

Notation "A <: B" := (Inject A B) (at level 20, right associativity).


Instance refl {A : Set} : A <: A :=
{|
  inj := fun x => x
|}.

(* assign priority to instances ?? that's what " | 2 " is 
https://softwarefoundations.cis.upenn.edu/qc-current/Typeclasses.html
*)
Instance S1 {A B : Set} : A <: (A + B) | 2 :=
{|
  inj := inl
|}.

Instance S2 {A B C : Set}{_ : A <: B} : A <: (C + B) | 3 := 
{|
  inj := fun x => inr (inj x)
|}.

(* not working yet*)
Definition example : nat + bool + unit := inj true.