Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Binary Sum Types and Truncations #12

Open
wants to merge 45 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
45 commits
Select commit Hold shift + click to select a range
778eb6e
adding union types
vrahli Dec 17, 2023
a1637c8
still adding union types
vrahli Dec 18, 2023
0f1e422
still adding union types
vrahli Dec 18, 2023
8820cf3
still adding union types (got started on Fundamental)
vrahli Dec 18, 2023
ccc8f38
still on unions
vrahli Dec 19, 2023
44b2a0f
still adding unions
vrahli Dec 21, 2023
ad2fda2
still working on unions
vrahli Dec 22, 2023
05ee04d
some progress on cases
vrahli Jan 9, 2024
910a795
a bit more on cases
vrahli Jan 10, 2024
0c1cc98
changed the logical relation for unit
vrahli Jan 12, 2024
ad8fb90
still on cases
vrahli Jan 12, 2024
b0b0f0c
some progress with cases
vrahli Jan 13, 2024
f7b90de
still on cases
vrahli Jan 13, 2024
8a7afe1
some progress with cases
vrahli Jan 13, 2024
1114c97
still working on unions
vrahli Jan 13, 2024
04962d2
not much
vrahli Jan 14, 2024
2734d50
still fixing cases
vrahli Jan 16, 2024
ea2cae1
still fixing cases
vrahli Jan 16, 2024
eb901db
still fixing cases
vrahli Jan 16, 2024
62782bb
not much
vrahli Jan 16, 2024
fcb4382
not much
vrahli Jan 16, 2024
ccc260d
not much
vrahli Jan 17, 2024
f9f6222
still working on cases
vrahli Jan 19, 2024
2c5f8a8
a bit of progress on unions
vrahli Feb 2, 2024
d2eea7c
still experimenting
vrahli Feb 3, 2024
abbbda7
still experimenting
vrahli Feb 4, 2024
18ff19f
still experimenting
vrahli Feb 4, 2024
fcf9c5c
still experimenting
vrahli Feb 4, 2024
1085c09
still experimenting
vrahli Feb 5, 2024
786cb08
finished adding union types
vrahli Feb 5, 2024
cb08374
removed commented out code
vrahli Feb 5, 2024
2acee10
started adding truncations
vrahli Feb 5, 2024
4feaabb
still adding truncations
vrahli Feb 5, 2024
94da668
still looking into truncation
vrahli Feb 5, 2024
9c3a2ac
still on truncations
vrahli Feb 6, 2024
1aad983
still on truncations
vrahli Feb 7, 2024
4f9f4d9
still on truncation
vrahli Feb 7, 2024
a5dcf8a
still on truncation
vrahli Feb 7, 2024
a83b6b6
still on truncation
vrahli Feb 7, 2024
97d1dcc
still on truncations
vrahli Feb 8, 2024
479f5a6
still on truncation
vrahli Feb 8, 2024
374f15c
finished adding truncations
vrahli Feb 8, 2024
f173455
removed some unncessary hyps
vrahli Feb 11, 2024
ca25e67
not much
vrahli Mar 1, 2024
15bbade
cubical compatible
vrahli Jul 4, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
still adding unions
vrahli committed Dec 21, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
commit 44b2a0f129a0a00df3216d7b4c47a132c137343d
4 changes: 4 additions & 0 deletions Definition/LogicalRelation/ShapeView.agda
Original file line number Diff line number Diff line change
@@ -77,6 +77,10 @@ B-intr : ∀ {A l} W → Γ ⊩⟨ l ⟩B⟨ W ⟩ A → Γ ⊩⟨ l ⟩ A
B-intr W (noemb x) = Bᵣ W x
B-intr W (emb 0<1 x) = emb 0<1 (B-intr W x)

∪-intr : ∀ {A l} → Γ ⊩⟨ l ⟩∪ A → Γ ⊩⟨ l ⟩ A
∪-intr (noemb x) = ∪ᵣ x
∪-intr (emb 0<1 x) = emb 0<1 (∪-intr x)

-- Construct a specific reducible type from a general with some criterion

U-elim : ∀ {l} → Γ ⊩⟨ l ⟩ U → Γ ⊩⟨ l ⟩U
248 changes: 248 additions & 0 deletions Definition/LogicalRelation/Substitution/Introductions/Injection.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,248 @@
{-# OPTIONS --without-K --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Injection {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk ; _∷_)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Introductions.Union
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst

open import Tools.Nat
open import Tools.Product
import Tools.PropositionalEquality as PE

private
variable
n : Nat
A t : Term n
Γ : Con Term n

injl′ : ∀ {A B t l l′}
([A] : Γ ⊩⟨ l ⟩ A)
([B] : Γ ⊩⟨ l ⟩ B)
([t] : Γ ⊩⟨ l ⟩ t ∷ A / [A])
([∪FG] : Γ ⊩⟨ l′ ⟩∪ A ∪ B)
→ Γ ⊩⟨ l′ ⟩ injl t ∷ A ∪ B / ∪-intr [∪FG]
injl′ {Γ = Γ} {A} {B} {t} {l} {l′} [A] [B] [t]
[∪FG]@(noemb (∪ᵣ A₁ B₁ D ⊢A ⊢B A≡A [A]₁ [B]₁)) with
∪-PE-injectivity (whnfRed* (red D) ∪ₙ)
... | PE.refl , PE.refl =
let ⊢t = escapeTerm [A] [t]
⊢Γ = wf ⊢A
⊢inj = injlⱼ ⊢t ⊢B
in ∪₁ₜ (injl t)
(idRedTerm:*: ⊢inj)
(≅-injl-cong ⊢A ⊢B (escapeTermEq [A] (reflEqTerm [A] [t])))
t
injlₙ
(irrelevanceTerm′ (PE.sym (wk-id A)) [A] ([A]₁ id ⊢Γ) [t])
injl′ {Γ = Γ} {A} {B} {t} {l} {l′} [B] [A] [t]
[∪FG]@(emb 0<1 x) = injl′ [B] [A] [t] x

injr′ : ∀ {A B t l l′}
([A] : Γ ⊩⟨ l ⟩ A)
([B] : Γ ⊩⟨ l ⟩ B)
([t] : Γ ⊩⟨ l ⟩ t ∷ B / [B])
([∪FG] : Γ ⊩⟨ l′ ⟩∪ A ∪ B)
→ Γ ⊩⟨ l′ ⟩ injr t ∷ A ∪ B / ∪-intr [∪FG]
injr′ {Γ = Γ} {A} {B} {t} {l} {l′} [A] [B] [t]
[∪FG]@(noemb (∪ᵣ A₁ B₁ D ⊢A ⊢B A≡A [A]₁ [B]₁)) with
∪-PE-injectivity (whnfRed* (red D) ∪ₙ)
... | PE.refl , PE.refl =
let ⊢t = escapeTerm [B] [t]
⊢Γ = wf ⊢B
⊢inj = injrⱼ ⊢A ⊢t
in ∪₂ₜ (injr t)
(idRedTerm:*: ⊢inj)
(≅-injr-cong ⊢A ⊢B (escapeTermEq [B] (reflEqTerm [B] [t])))
t
injrₙ
(irrelevanceTerm′ (PE.sym (wk-id B)) [B] ([B]₁ id ⊢Γ) [t])
injr′ {Γ = Γ} {A} {B} {t} {l} {l′} [B] [A] [t]
[∪FG]@(emb 0<1 x) = injr′ [B] [A] [t] x

injl″ : ∀ {A B t l l′}
([A] : Γ ⊩⟨ l ⟩ A)
([B] : Γ ⊩⟨ l ⟩ B)
([t] : Γ ⊩⟨ l ⟩ t ∷ A / [A])
([∪AB] : Γ ⊩⟨ l′ ⟩ A ∪ B)
→ Γ ⊩⟨ l′ ⟩ injl t ∷ A ∪ B / [∪AB]
injl″ [A] [B] [t] [∪AB] =
irrelevanceTerm (∪-intr (∪-elim [∪AB])) [∪AB] (injl′ [A] [B] [t] (∪-elim [∪AB]))

injr″ : ∀ {A B t l l′}
([A] : Γ ⊩⟨ l ⟩ A)
([B] : Γ ⊩⟨ l ⟩ B)
([t] : Γ ⊩⟨ l ⟩ t ∷ B / [B])
([∪AB] : Γ ⊩⟨ l′ ⟩ A ∪ B)
→ Γ ⊩⟨ l′ ⟩ injr t ∷ A ∪ B / [∪AB]
injr″ [A] [B] [t] [∪AB] =
irrelevanceTerm (∪-intr (∪-elim [∪AB])) [∪AB] (injr′ [A] [B] [t] (∪-elim [∪AB]))

injl-cong′ : ∀ {A B t u l l′}
([A] : Γ ⊩⟨ l ⟩ A)
([B] : Γ ⊩⟨ l ⟩ B)
([t] : Γ ⊩⟨ l ⟩ t ∷ A / [A])
([u] : Γ ⊩⟨ l ⟩ u ∷ A / [A])
([t≡u] : Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A])
([∪AB] : Γ ⊩⟨ l′ ⟩∪ A ∪ B)
→ Γ ⊩⟨ l′ ⟩ injl t ≡ injl u ∷ A ∪ B / ∪-intr [∪AB]
injl-cong′ {Γ = Γ} {A} {B} {t} {u} {l} {l′}
[A] [B] [t] [u] [t≡u]
[∪AB]@(noemb (∪ᵣ A₁ B₁ D ⊢F ⊢G A≡A [A]₁ [B]₁)) with
∪-PE-injectivity (whnfRed* (red D) ∪ₙ)
... | PE.refl , PE.refl =
let [inj] = injl′ [A] [B] [t] [∪AB]
[inj'] = injl′ [A] [B] [u] [∪AB]
⊢Γ = wf ⊢F
wk[A] = [A]₁ id ⊢Γ
wk[t≡u] = irrelevanceEqTerm′ (PE.sym (wk-id A)) [A] wk[A] [t≡u]
⊢inj = escapeTerm (∪-intr [∪AB]) [inj]
⊢inj′ = escapeTerm (∪-intr [∪AB]) [inj']
in ∪₁ₜ₌ (injl t) (injl u) (idRedTerm:*: ⊢inj) (idRedTerm:*: ⊢inj′)
(≅-injl-cong ⊢F ⊢G (escapeTermEq [A] [t≡u]))
[inj] [inj'] t u injlₙ injlₙ wk[t≡u]
injl-cong′ [A] [B] [t] [u] [t≡u] (emb 0<1 x) =
injl-cong′ [A] [B] [t] [u] [t≡u] x

injr-cong′ : ∀ {A B t u l l′}
([A] : Γ ⊩⟨ l ⟩ A)
([B] : Γ ⊩⟨ l ⟩ B)
([t] : Γ ⊩⟨ l ⟩ t ∷ B / [B])
([u] : Γ ⊩⟨ l ⟩ u ∷ B / [B])
([t≡u] : Γ ⊩⟨ l ⟩ t ≡ u ∷ B / [B])
([∪AB] : Γ ⊩⟨ l′ ⟩∪ A ∪ B)
→ Γ ⊩⟨ l′ ⟩ injr t ≡ injr u ∷ A ∪ B / ∪-intr [∪AB]
injr-cong′ {Γ = Γ} {A} {B} {t} {u} {l} {l′}
[A] [B] [t] [u] [t≡u]
[∪AB]@(noemb (∪ᵣ A₁ B₁ D ⊢F ⊢G A≡A [A]₁ [B]₁)) with
∪-PE-injectivity (whnfRed* (red D) ∪ₙ)
... | PE.refl , PE.refl =
let [inj] = injr′ [A] [B] [t] [∪AB]
[inj'] = injr′ [A] [B] [u] [∪AB]
⊢Γ = wf ⊢G
wk[B] = [B]₁ id ⊢Γ
wk[t≡u] = irrelevanceEqTerm′ (PE.sym (wk-id B)) [B] wk[B] [t≡u]
⊢inj = escapeTerm (∪-intr [∪AB]) [inj]
⊢inj′ = escapeTerm (∪-intr [∪AB]) [inj']
in ∪₂ₜ₌ (injr t) (injr u) (idRedTerm:*: ⊢inj) (idRedTerm:*: ⊢inj′)
(≅-injr-cong ⊢F ⊢G (escapeTermEq [B] [t≡u]))
[inj] [inj'] t u injrₙ injrₙ wk[t≡u]
injr-cong′ [A] [B] [t] [u] [t≡u] (emb 0<1 x) =
injr-cong′ [A] [B] [t] [u] [t≡u] x

injl-cong″ : ∀ {A B t u l l′}
([A] : Γ ⊩⟨ l ⟩ A)
([B] : Γ ⊩⟨ l ⟩ B)
([t] : Γ ⊩⟨ l ⟩ t ∷ A / [A])
([u] : Γ ⊩⟨ l ⟩ u ∷ A / [A])
([t≡u′] : Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A])
([∪AB] : Γ ⊩⟨ l′ ⟩ A ∪ B)
→ Γ ⊩⟨ l′ ⟩ injl t ≡ injl u ∷ A ∪ B / [∪AB]
injl-cong″ [A] [B] [t] [u] [t≡u] [∪AB] =
let [inj≡] = injl-cong′ [A] [B] [t] [u] [t≡u] (∪-elim [∪AB])
in irrelevanceEqTerm (∪-intr (∪-elim [∪AB])) [∪AB] [inj≡]

injr-cong″ : ∀ {A B t u l l′}
([A] : Γ ⊩⟨ l ⟩ A)
([B] : Γ ⊩⟨ l ⟩ B)
([t] : Γ ⊩⟨ l ⟩ t ∷ B / [B])
([u] : Γ ⊩⟨ l ⟩ u ∷ B / [B])
([t≡u′] : Γ ⊩⟨ l ⟩ t ≡ u ∷ B / [B])
([∪AB] : Γ ⊩⟨ l′ ⟩ A ∪ B)
→ Γ ⊩⟨ l′ ⟩ injr t ≡ injr u ∷ A ∪ B / [∪AB]
injr-cong″ [A] [B] [t] [u] [t≡u] [∪AB] =
let [inj≡] = injr-cong′ [A] [B] [t] [u] [t≡u] (∪-elim [∪AB])
in irrelevanceEqTerm (∪-intr (∪-elim [∪AB])) [∪AB] [inj≡]

injl-congᵛ : ∀ {A B t u l}
([Γ] : ⊩ᵛ Γ)
([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
([B] : Γ ⊩ᵛ⟨ l ⟩ B / [Γ])
([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A])
([u] : Γ ⊩ᵛ⟨ l ⟩ u ∷ A / [Γ] / [A])
([t≡u] : Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A / [Γ] / [A])
→ Γ ⊩ᵛ⟨ l ⟩ injl t ≡ injl u ∷ A ∪ B / [Γ] / ∪ᵛ {F = A} {B} [Γ] [A] [B]
injl-congᵛ {Γ = Γ} {A} {B} {t} {u} [Γ] [A] [B] [t] [u] [t≡u] {Δ = Δ} {σ} ⊢Δ [σ] =
let ⊩σA = proj₁ ([A] ⊢Δ [σ])
⊩σB = proj₁ ([B] ⊢Δ [σ])
⊩σt = proj₁ ([t] ⊢Δ [σ])
⊩σu = proj₁ ([u] ⊢Δ [σ])
σt≡σu = [t≡u] ⊢Δ [σ]
⊩σ∪AB = proj₁ (∪ᵛ {F = A} {B} [Γ] [A] [B] ⊢Δ [σ])
in injl-cong″ ⊩σA ⊩σB ⊩σt ⊩σu σt≡σu ⊩σ∪AB

injr-congᵛ : ∀ {A B t u l}
([Γ] : ⊩ᵛ Γ)
([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
([B] : Γ ⊩ᵛ⟨ l ⟩ B / [Γ])
([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ B / [Γ] / [B])
([u] : Γ ⊩ᵛ⟨ l ⟩ u ∷ B / [Γ] / [B])
([t≡u] : Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ B / [Γ] / [B])
→ Γ ⊩ᵛ⟨ l ⟩ injr t ≡ injr u ∷ A ∪ B / [Γ] / ∪ᵛ {F = A} {B} [Γ] [A] [B]
injr-congᵛ {Γ = Γ} {A} {B} {t} {u} [Γ] [A] [B] [t] [u] [t≡u] {Δ = Δ} {σ} ⊢Δ [σ] =
let ⊩σA = proj₁ ([A] ⊢Δ [σ])
⊩σB = proj₁ ([B] ⊢Δ [σ])
⊩σt = proj₁ ([t] ⊢Δ [σ])
⊩σu = proj₁ ([u] ⊢Δ [σ])
σt≡σu = [t≡u] ⊢Δ [σ]
⊩σ∪AB = proj₁ (∪ᵛ {F = A} {B} [Γ] [A] [B] ⊢Δ [σ])
in injr-cong″ ⊩σA ⊩σB ⊩σt ⊩σu σt≡σu ⊩σ∪AB

injlᵛ : ∀ {A B t l}
([Γ] : ⊩ᵛ Γ)
([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
([B] : Γ ⊩ᵛ⟨ l ⟩ B / [Γ])
([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A])
→ Γ ⊩ᵛ⟨ l ⟩ injl t ∷ A ∪ B / [Γ] / ∪ᵛ {F = A} {B} [Γ] [A] [B]
injlᵛ {Γ = Γ} {A} {B} {t} {l} [Γ] [A] [B] [t] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
let [∪AB] = ∪ᵛ {F = A} {B} [Γ] [A] [B]
⊩σA = proj₁ ([A] ⊢Δ [σ])
⊩σB = proj₁ ([B] ⊢Δ [σ])
⊩σt = proj₁ ([t] ⊢Δ [σ])
⊩σ∪AB = proj₁ ([∪AB] ⊢Δ [σ])

in injl″ ⊩σA ⊩σB ⊩σt ⊩σ∪AB ,
(λ {σ′} [σ′] [σ≡σ′] →
let ⊩σ′A = proj₁ ([A] ⊢Δ [σ′])
σA≡σ′A = proj₂ ([A] ⊢Δ [σ]) [σ′] [σ≡σ′]
⊩σ′t = convTerm₂ ⊩σA ⊩σ′A σA≡σ′A (proj₁ ([t] ⊢Δ [σ′]))
σt≡σ′t = proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′]
in injl-cong″ ⊩σA ⊩σB ⊩σt ⊩σ′t σt≡σ′t ⊩σ∪AB)

injrᵛ : ∀ {A B t l}
([Γ] : ⊩ᵛ Γ)
([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
([B] : Γ ⊩ᵛ⟨ l ⟩ B / [Γ])
([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ B / [Γ] / [B])
→ Γ ⊩ᵛ⟨ l ⟩ injr t ∷ A ∪ B / [Γ] / ∪ᵛ {F = A} {B} [Γ] [A] [B]
injrᵛ {Γ = Γ} {A} {B} {t} {l} [Γ] [A] [B] [t] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
let [∪AB] = ∪ᵛ {F = A} {B} [Γ] [A] [B]
⊩σA = proj₁ ([A] ⊢Δ [σ])
⊩σB = proj₁ ([B] ⊢Δ [σ])
⊩σt = proj₁ ([t] ⊢Δ [σ])
⊩σ∪AB = proj₁ ([∪AB] ⊢Δ [σ])

in injr″ ⊩σA ⊩σB ⊩σt ⊩σ∪AB ,
(λ {σ′} [σ′] [σ≡σ′] →
let ⊩σ′B = proj₁ ([B] ⊢Δ [σ′])
σB≡σ′B = proj₂ ([B] ⊢Δ [σ]) [σ′] [σ≡σ′]
⊩σ′t = convTerm₂ ⊩σB ⊩σ′B σB≡σ′B (proj₁ ([t] ⊢Δ [σ′]))
σt≡σ′t = proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′]
in injr-cong″ ⊩σA ⊩σB ⊩σt ⊩σ′t σt≡σ′t ⊩σ∪AB)
2 changes: 2 additions & 0 deletions Definition/Typed/EqRelInstance.agda
Original file line number Diff line number Diff line change
@@ -49,6 +49,8 @@ eqRelInstance = record {
≅ₜ-Σ-cong = Σ-cong;
≅-∪-cong = ∪-cong;
≅ₜ-∪-cong = ∪-cong;
≅-injl-cong = injl-cong;
≅-injr-cong = injr-cong;
≅ₜ-zerorefl = refl ∘ᶠ zeroⱼ;
≅-suc-cong = suc-cong;
≅-η-eq = λ x x₁ x₂ x₃ x₄ x₅ → η-eq x x₁ x₂ x₅;
14 changes: 14 additions & 0 deletions Definition/Typed/EqualityRelation.agda
Original file line number Diff line number Diff line change
@@ -160,6 +160,20 @@ record EqRelSet : Set₁ where
→ Γ ⊢ G ≅ E ∷ U
→ Γ ⊢ F ∪ G ≅ H ∪ E ∷ U

-- congruence for injl
≅-injl-cong : ∀ {p r F G}
→ Γ ⊢ F -- needed?
→ Γ ⊢ G
→ Γ ⊢ p ≅ r ∷ F
→ Γ ⊢ injl p ≅ injl r ∷ F ∪ G

-- congruence for injr
≅-injr-cong : ∀ {p r F G}
→ Γ ⊢ F
→ Γ ⊢ G -- needed?
→ Γ ⊢ p ≅ r ∷ G
→ Γ ⊢ injr p ≅ injr r ∷ F ∪ G

-- Zero reflexivity
≅ₜ-zerorefl : ⊢ Γ → Γ ⊢ zero ≅ zero ∷ ℕ

8 changes: 8 additions & 0 deletions Definition/Untyped.agda
Original file line number Diff line number Diff line change
@@ -358,6 +358,14 @@ data InjectionL {n : Nat} : Term n → Term n → Set where
data InjectionR {n : Nat} : Term n → Term n → Set where
injrₙ : InjectionR (injr t) t

data InjectionLN {n : Nat} : Term n → Set where
injlₙ : InjectionLN (injl t)
ne : Neutral t → InjectionLN t

data InjectionRN {n : Nat} : Term n → Set where
injrₙ : InjectionRN (injl t)
ne : Neutral t → InjectionRN t

InjectionL-PE-injectivity : InjectionL t a → InjectionL u v → t PE.≡ u → a PE.≡ v
InjectionL-PE-injectivity injlₙ injlₙ PE.refl = PE.refl