module NameAbst where
open import Basics
open import Atoms
open import Perms
open import PermProp
open import Nom
open import CatDef
open import FreshNom
record NewName {X : Nominal} (a₁x₁ : Atom × (Aₛ X)) (a₂x₂ : Atom × (Aₛ X)) : Set where
constructor NName
field
nn : Atom
nn∉x₁ : nn ∉ (some_supp X) (proj₂ a₁x₁)
nn∉x₂ : nn ∉ (some_supp X) (proj₂ a₂x₂)
nna₁≈nna₂ : (≈ₐ X) ((Act X) [ (nn , (proj₁ a₁x₁)) ] (proj₂ a₁x₁)) ((Act X) [ (nn , (proj₁ a₂x₂)) ] (proj₂ a₂x₂))
open NewName public
α : (X : Nominal) → (Atom × (Aₛ X)) → (Atom × (Aₛ X)) → Set
α X (a₁ , x₁) (a₂ , x₂) = NewName {X} (a₁ , x₁) (a₂ , x₂)
∉ℓ₁ℓ₂ : (aℓ₁ aℓ₂ : List Atom) → (b : Atom) → b ∉ aℓ₁ → b ∉ aℓ₂ → b ∉ (aℓ₁ ++ aℓ₂)
∉ℓ₁ℓ₂ [] aℓ₂ b b∉ℓ₁ b∉ℓ₂ = b∉ℓ₂
∉ℓ₁ℓ₂ (x :: xs) aℓ₂ b (a∉as b∉xs b≠x) b∉ℓ₂ = a∉as (∉ℓ₁ℓ₂ xs aℓ₂ b b∉xs b∉ℓ₂) b≠x
∉comm : (aℓ₁ aℓ₂ : List Atom) → (b : Atom) → (b ∉ (aℓ₁ ++ aℓ₂)) → b ∉ (aℓ₂ ++ aℓ₁)
∉comm aℓ₁ aℓ₂ b b∉ℓ₁ℓ₂ = ∉ℓ₁ℓ₂ aℓ₂ aℓ₁ b (∉⊆₂ {aℓ₁}{aℓ₂} b b∉ℓ₁ℓ₂) (∉⊆₁ {aℓ₁}{aℓ₂} b b∉ℓ₁ℓ₂)
Some/Anyα : {X : Nominal} → (x₁ x₂ : Aₛ X) → (a₁ a₂ : Atom) → (b : Atom) → b ∉ (some_supp X) x₁ → b ∉ (some_supp X) x₂ → (≈ₐ X)((Act X) [(b , a₁)] x₁)((Act X)[(b , a₂)] x₂)
→ (c : Atom) → c ∉ (some_supp X) x₁ → c ∉ (some_supp X) x₂ → (≈ₐ X)((Act X) [(c , a₁)] x₁)((Act X)[(c , a₂)] x₂)
Some/Anyα {X} x₁ x₂ a₁ a₂ b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ with AtEqDec a₁ c | AtEqDec a₂ c
Some/Anyα {X} x₁ x₂ .c .c b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | yes refl | yes refl =
(((Act X) [(c , c)] x₁)
≣< ((Act X) ι x₁) and ((Act X) [(c , c)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (aa≈ι c) {x}) (≈≡ (eq≈ₐ X) {x₁}{x₁} refl)) >
(((Act X) ι x₁)
≣< x₁ and ((Act X) [(c , c)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((ι↠ X) {x₁}) >
(x₁
≣< ((Act X) [(b , c)] x₁) and ((Act X) [(c , c)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((suppAx X) x₁ b c b∉x₁ c∉x₁)) >
(((Act X) [(b , c)] x₁)
≣< ((Act X) [(b , c)] x₂) and ((Act X) [(c , c)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
ba₁x₁≈ba₂x₂ >
(((Act X) [(b , c)] x₂)
≣< x₂ and ((Act X) [(c , c)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((suppAx X) x₂ b c b∉x₂ c∉x₂) >
(x₂
≣< ((Act X) ι x₂) and ((Act X) [(c , c)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) (ι↠ X {x₂})) >
(((Act X) ι x₂)
≣< ((Act X) [(c , c)] x₂) and ((Act X) [(c , c)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → (aa≈ι c) {x})(≈≡ (eq≈ₐ X) {x₂}{x₂} refl))) >
(((Act X) [(c , c)] x₂) by (≈ₐ X) as (eq≈ₐ X) ▴))))))))
Some/Anyα {X} x₁ x₂ .c a₂ b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | yes refl | no a₂≠c with AtEqDec a₂ b
Some/Anyα {X} x₁ x₂ .c .b b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | yes refl | no a₂≠c | yes refl =
(((Act X) [(c , c)] x₁)
≣< ((Act X) ι x₁) and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (aa≈ι c) {x}) (≈≡ (eq≈ₐ X) {x₁}{x₁} refl)) >
(((Act X) ι x₁)
≣< x₁ and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((ι↠ X) {x₁}) >
(x₁
≣< ((Act X) [(b , c)] x₁) and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((suppAx X) x₁ b c b∉x₁ c∉x₁)) >
(((Act X) [(b , c)] x₁)
≣< ((Act X) [(b , b)] x₂) and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
ba₁x₁≈ba₂x₂ >
(((Act X) [(b , b)] x₂)
≣< ((Act X) ι x₂) and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (aa≈ι b) {x}) (≈≡ (eq≈ₐ X) {x₂}{x₂} refl)) >
(((Act X) ι x₂)
≣< x₂ and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((ι↠ X) {x₂}) >
(x₂
≣< ((Act X) [(c , b)] x₂) and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((suppAx X) x₂ c b c∉x₂ b∉x₂)) >
(((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) ▴))))))))
Some/Anyα {X} x₁ x₂ .c a₂ b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | yes refl | no a₂≠c | no a₂≠b =
(((Act X) [(c , c)] x₁)
≣< ((Act X) ι x₁) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (aa≈ι c) {x}) (≈≡ (eq≈ₐ X) {x₁}{x₁} refl)) >
(((Act X) ι x₁)
≣< ((Act X) ([(b , c)] ++ [(c , b)]) x₁) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X))((res X) (λ {x} → (bc+cb=ι b c) {x}) (≈≡ (eq≈ₐ X) {x₁}{x₁} refl))) >
(((Act X) ([(b , c)] ++ [(c , b)]) x₁)
≣< ((Act X) [(c , b)] ((Act X) [(b , c)] x₁)) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((p₁p₂↠ X) [(c , b)] [(b , c)] {x₁})) >
(((Act X) [(c , b)] ((Act X) [(b , c)] x₁))
≣< ((Act X) [(c , b)] ((Act X) [(b , a₂)] x₂)) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (P≡≈ [(c , b)]) {x}) ba₁x₁≈ba₂x₂) >
(((Act X) [(c , b)] ((Act X) [(b , a₂)] x₂))
≣< ((Act X) ([(b , a₂)] ++ [(c , b)]) x₂) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) [(c , b)] [(b , a₂)] {x₂}) >
(((Act X) ([(b , a₂)] ++ [(c , b)]) x₂)
≣< ((Act X) ([(b , a₂)] ++ [(c , b)]) ((Act X) [(c , b)] x₂)) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (P≡≈ ([(b , a₂)] ++ [(c , b)]) {x})) ((Symm (eq≈ₐ X)) ((suppAx X) x₂ c b c∉x₂ b∉x₂))) >
(((Act X) ([(b , a₂)] ++ [(c , b)]) ((Act X) [(c , b)] x₂))
≣< ((Act X) ([(c , b)] ++ ([(b , a₂)] ++ [(c , b)])) x₂) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) ([(b , a₂)] ++ [(c , b)]) [(c , b)] {x₂}) >
(((Act X) ([(c , b)] ++ ([(b , a₂)] ++ [(c , b)])) x₂)
≣< ((Act X) [(c , a₂)] x₂) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → (ac≈ab+bc+ab c b a₂ a₂≠c a₂≠b) {x}) (≈≡ (eq≈ₐ X) {x₂}{x₂} refl))) >
(((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) ▴)))))))))
Some/Anyα {X} x₁ x₂ a₁ .c b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | no a₁≠c | yes refl with AtEqDec a₁ b
Some/Anyα {X} x₁ x₂ .b .c b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | no a₁≠c | yes refl | yes refl = (Symm (eq≈ₐ X))
(((Act X) [(c , c)] x₂)
≣< ((Act X) ι x₂) and ((Act X) [(c , b)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (aa≈ι c) {x}) (≈≡ (eq≈ₐ X) {x₂}{x₂} refl)) >
(((Act X) ι x₂)
≣< x₂ and ((Act X) [(c , b)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((ι↠ X) {x₂}) >
(x₂
≣< ((Act X) [(b , c)] x₂) and ((Act X) [(c , b)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((suppAx X) x₂ b c b∉x₂ c∉x₂)) >
(((Act X) [(b , c)] x₂)
≣< ((Act X) [(b , b)] x₁) and ((Act X) [(c , b)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ba₁x₁≈ba₂x₂) >
(((Act X) [(b , b)] x₁)
≣< ((Act X) ι x₁) and ((Act X) [(c , b)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (aa≈ι b) {x}) (≈≡ (eq≈ₐ X) {x₁}{x₁} refl)) >
(((Act X) ι x₁)
≣< x₁ and ((Act X) [(c , b)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((ι↠ X) {x₁}) >
(x₁
≣< ((Act X) [(c , b)] x₁) and ((Act X) [(c , b)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((suppAx X) x₁ c b c∉x₁ b∉x₁)) >
(((Act X) [(c , b)] x₁) by (≈ₐ X) as (eq≈ₐ X) ▴))))))))
Some/Anyα {X} x₁ x₂ a₁ .c b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | no a₁≠c | yes refl | no a₁≠b = (Symm (eq≈ₐ X))
(((Act X) [(c , c)] x₂)
≣< ((Act X) ι x₂) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (aa≈ι c) {x}) (≈≡ (eq≈ₐ X) {x₂}{x₂} refl)) >
(((Act X) ι x₂)
≣< ((Act X) ([(b , c)] ++ [(c , b)]) x₂) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X))((res X) (λ {x} → (bc+cb=ι b c) {x}) (≈≡ (eq≈ₐ X) {x₂}{x₂} refl))) >
(((Act X) ([(b , c)] ++ [(c , b)]) x₂)
≣< ((Act X) [(c , b)] ((Act X) [(b , c)] x₂)) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((p₁p₂↠ X) [(c , b)] [(b , c)] {x₂})) >
(((Act X) [(c , b)] ((Act X) [(b , c)] x₂))
≣< ((Act X) [(c , b)] ((Act X) [(b , a₁)] x₁)) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → (P≡≈ [(c , b)]) {x}) ba₁x₁≈ba₂x₂)) >
(((Act X) [(c , b)] ((Act X) [(b , a₁)] x₁))
≣< ((Act X) ([(b , a₁)] ++ [(c , b)]) x₁) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) [(c , b)] [(b , a₁)] {x₁}) >
(((Act X) ([(b , a₁)] ++ [(c , b)]) x₁)
≣< ((Act X) ([(b , a₁)] ++ [(c , b)]) ((Act X) [(c , b)] x₁)) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (P≡≈ ([(b , a₁)] ++ [(c , b)]) {x})) ((Symm (eq≈ₐ X)) ((suppAx X) x₁ c b c∉x₁ b∉x₁))) >
(((Act X) ([(b , a₁)] ++ [(c , b)]) ((Act X) [(c , b)] x₁))
≣< ((Act X) ([(c , b)] ++ ([(b , a₁)] ++ [(c , b)])) x₁) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) ([(b , a₁)] ++ [(c , b)]) [(c , b)] {x₁}) >
(((Act X) ([(c , b)] ++ ([(b , a₁)] ++ [(c , b)])) x₁)
≣< ((Act X) [(c , a₁)] x₁) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → (ac≈ab+bc+ab c b a₁ a₁≠c a₁≠b) {x}) (≈≡ (eq≈ₐ X) {x₁}{x₁} refl))) >
(((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) ▴)))))))))
Some/Anyα {X} x₁ x₂ a₁ a₂ b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | no a₁≠c | no a₂≠c with AtEqDec a₁ b | AtEqDec a₂ b
Some/Anyα {X} x₁ x₂ .b .b b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | no a₁≠c | no a₂≠c | yes refl | yes refl =
(((Act X) [(c , b)] x₁)
≣< x₁ and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((suppAx X) x₁ c b c∉x₁ b∉x₁) >
(x₁
≣< ((Act X) ι x₁) and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((ι↠ X) {x₁})) >
(((Act X) ι x₁)
≣< ((Act X) [(b , b)] x₁) and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → aa≈ι b {x}) (≈≡ (eq≈ₐ X) {x₁}{x₁} refl))) >
(((Act X) [(b , b)] x₁)
≣< ((Act X) [(b , b)] x₂) and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
ba₁x₁≈ba₂x₂ >
(((Act X) [(b , b)] x₂)
≣< ((Act X) ι x₂) and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → aa≈ι b {x}) (≈≡ (eq≈ₐ X) {x₂}{x₂} refl)) >
(((Act X) ι x₂)
≣< x₂ and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((ι↠ X) {x₂}) >
(x₂
≣< ((Act X) [(c , b)] x₂) and ((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((suppAx X) x₂ c b c∉x₂ b∉x₂)) >
(((Act X) [(c , b)] x₂) by (≈ₐ X) as (eq≈ₐ X) ▴))))))))
Some/Anyα {X} x₁ x₂ .b a₂ b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | no a₁≠c | no a₂≠c | yes refl | no a₂≠b =
(((Act X) [(c , b)] x₁)
≣< ((Act X) [(c , b)] ((Act X) ι x₁)) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → P≡≈ [(c , b)] {x}) ((ι↠ X) {x₁}))) >
(((Act X) [(c , b)] ((Act X) ι x₁))
≣< ((Act X) [(c , b)] ((Act X) [(b , b)] x₁)) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → P≡≈ [(c , b)] {x}) ((res X) (λ {x} → aa≈ι b {x}) (≈≡ (eq≈ₐ X) {x₁}{x₁} refl)))) >
(((Act X) [(c , b)] ((Act X) [(b , b)] x₁))
≣< ((Act X) [(c , b)] ((Act X) [(b , a₂)] x₂)) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → P≡≈ [(c , b)] {x}) ba₁x₁≈ba₂x₂) >
(((Act X) [(c , b)] ((Act X) [(b , a₂)] x₂))
≣< ((Act X) ([(b , a₂)] ++ [(c , b)]) x₂) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) [(c , b)] [(b , a₂)] {x₂}) >
(((Act X) ([(b , a₂)] ++ [(c , b)]) x₂)
≣< ((Act X) ([(b , a₂)] ++ [(c , b)]) ((Act X) [(c , b)] x₂)) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → P≡≈ ([(b , a₂)] ++ [(c , b)]) {x}) ((suppAx X) x₂ c b c∉x₂ b∉x₂))) >
(((Act X) ([(b , a₂)] ++ [(c , b)]) ((Act X) [(c , b)] x₂))
≣< ((Act X) ([(c , b)] ++ ([(b , a₂)] ++ [(c , b)])) x₂) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) ([(b , a₂)] ++ [(c , b)]) [(c , b)] {x₂}) >
(((Act X) ([(c , b)] ++ ([(b , a₂)] ++ [(c , b)])) x₂)
≣< ((Act X) [(c , a₂)] x₂) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → (ac≈ab+bc+ab c b a₂ a₂≠c a₂≠b) {x}) (≈≡ (eq≈ₐ X) {x₂} {x₂} refl))) >
(((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) ▴))))))))
Some/Anyα {X} x₁ x₂ a₁ .b b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | no a₁≠c | no a₂≠c | no a₁≠b | yes refl = (Symm (eq≈ₐ X))
(((Act X) [(c , b)] x₂)
≣< ((Act X) [(c , b)] ((Act X) ι x₂)) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → P≡≈ [(c , b)] {x}) ((ι↠ X) {x₂}))) >
(((Act X) [(c , b)] ((Act X) ι x₂))
≣< ((Act X) [(c , b)] ((Act X) [(b , b)] x₂)) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → P≡≈ [(c , b)] {x}) ((res X) (λ {x} → aa≈ι b {x}) (≈≡ (eq≈ₐ X) {x₂}{x₂} refl)))) >
(((Act X) [(c , b)] ((Act X) [(b , b)] x₂))
≣< ((Act X) [(c , b)] ((Act X) [(b , a₁)] x₁)) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → P≡≈ [(c , b)] {x}) ba₁x₁≈ba₂x₂)) >
(((Act X) [(c , b)] ((Act X) [(b , a₁)] x₁))
≣< ((Act X) ([(b , a₁)] ++ [(c , b)]) x₁) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) [(c , b)] [(b , a₁)] {x₁}) >
(((Act X) ([(b , a₁)] ++ [(c , b)]) x₁)
≣< ((Act X) ([(b , a₁)] ++ [(c , b)]) ((Act X) [(c , b)] x₁)) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → P≡≈ ([(b , a₁)] ++ [(c , b)]) {x}) ((suppAx X) x₁ c b c∉x₁ b∉x₁))) >
(((Act X) ([(b , a₁)] ++ [(c , b)]) ((Act X) [(c , b)] x₁))
≣< ((Act X) ([(c , b)] ++ ([(b , a₁)] ++ [(c , b)])) x₁) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) ([(b , a₁)] ++ [(c , b)]) [(c , b)] {x₁}) >
(((Act X) ([(c , b)] ++ ([(b , a₁)] ++ [(c , b)])) x₁)
≣< ((Act X) [(c , a₁)] x₁) and ((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → (ac≈ab+bc+ab c b a₁ a₁≠c a₁≠b) {x}) (≈≡ (eq≈ₐ X) {x₁} {x₁} refl))) >
(((Act X) [(c , a₁)] x₁) by (≈ₐ X) as (eq≈ₐ X) ▴))))))))
Some/Anyα {X} x₁ x₂ a₁ a₂ b b∉x₁ b∉x₂ ba₁x₁≈ba₂x₂ c c∉x₁ c∉x₂ | no a₁≠c | no a₂≠c | no a₁≠b | no a₂≠b =
(((Act X) [(c , a₁)] x₁)
≣< ((Act X)([(c , b)] ++ ([(b , a₁)] ++ [(c , b)])) x₁) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (ac≈ab+bc+ab c b a₁ a₁≠c a₁≠b) {x}) (≈≡ (eq≈ₐ X) {x₁}{x₁} refl)) >
(((Act X)([(c , b)] ++ ([(b , a₁)] ++ [(c , b)])) x₁)
≣< ((Act X) ([(b , a₁)] ++ [(c , b)]) ((Act X) [(c , b)] x₁)) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((p₁p₂↠ X) ([(b , a₁)] ++ [(c , b)]) [(c , b)] {x₁})) >
(((Act X) ([(b , a₁)] ++ [(c , b)]) ((Act X) [(c , b)] x₁))
≣< ((Act X) ([(b , a₁)] ++ [(c , b)]) x₁) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (P≡≈ ([(b , a₁)] ++ [(c , b)])) {x}) ((suppAx X) x₁ c b c∉x₁ b∉x₁)) >
(((Act X) ([(b , a₁)] ++ [(c , b)]) x₁)
≣< ((Act X) [(c , b)] ((Act X) [(b , a₁)] x₁)) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((p₁p₂↠ X) [(c , b)] [(b , a₁)] {x₁})) >
(((Act X) [(c , b)] ((Act X) [(b , a₁)] x₁))
≣< ((Act X) [(c , b)] ((Act X) [(b , a₂)] x₂)) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (P≡≈ [(c , b)]) {x}) ba₁x₁≈ba₂x₂) >
(((Act X) [(c , b)] ((Act X) [(b , a₂)] x₂))
≣< ((Act X) ([(b , a₂)] ++ [(c , b)]) x₂) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) [(c , b)] [(b , a₂)] {x₂}) >
(((Act X) ([(b , a₂)] ++ [(c , b)]) x₂)
≣< ((Act X) ([(b , a₂)] ++ [(c , b)]) ((Act X) [(c , b)] x₂)) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (P≡≈ ([(b , a₂)] ++ [(c , b)])) {x}) ((Symm (eq≈ₐ X)) ((suppAx X) x₂ c b c∉x₂ b∉x₂))) >
(((Act X) ([(b , a₂)] ++ [(c , b)]) ((Act X) [(c , b)] x₂))
≣< ((Act X) ([(c , b)] ++ ([(b , a₂)] ++ [(c , b)])) x₂) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) ([(b , a₂)] ++ [(c , b)]) [(c , b)] {x₂}) >
(((Act X) ([(c , b)] ++ ([(b , a₂)] ++ [(c , b)])) x₂)
≣< ((Act X) [(c , a₂)] x₂) and ((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X))((res X) (λ {x} → (ac≈ab+bc+ab c b a₂ a₂≠c a₂≠b) {x}) (≈≡ (eq≈ₐ X) {x₂}{x₂} refl))) >
(((Act X) [(c , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) ▴))))))))))
Some⇒Anyα : {X : Nominal}{a₁x₁ : Atom × (Aₛ X)}{a₂x₂ : Atom × (Aₛ X)} → (NN : NewName {X} a₁x₁ a₂x₂)
→ (c : Atom) → (c ∉ ((some_supp X) (proj₂ a₁x₁))) → (c ∉ ((some_supp X) (proj₂ a₂x₂))) → NewName {X} a₁x₁ a₂x₂
Some⇒Anyα {X} {a₁x₁}{a₂x₂} NN c c∉x₁ c∉x₂ = NName c c∉x₁ c∉x₂ (Some/Anyα {X} (proj₂ a₁x₁) (proj₂ a₂x₂) (proj₁ a₁x₁) (proj₁ a₂x₂) (nn NN) (nn∉x₁ NN) (nn∉x₂ NN) (nna₁≈nna₂ NN) c c∉x₁ c∉x₂)
∉⟶≠ : (a b : Atom) → (a ∉ [ b ]) → b ≠ a
∉⟶≠ a b (a∉as a∉[] b≠a) = b≠a
α≈ : (X : Nominal) → isEquivalence (Atom × (Aₛ X)) (α X)
α≈ X = record { Reflex = λ {ax} → let sup = ((some_supp X) (proj₂ ax))
in let b = outside sup
in NName b (outside∉ sup) (outside∉ sup) ((Reflex (eq≈ₐ X)) {(Act X) [ (b , (proj₁ ax)) ] (proj₂ ax)})
; Symm = λ a₁x₁≈a₂x₂ → NName (nn a₁x₁≈a₂x₂)
(nn∉x₂ a₁x₁≈a₂x₂)
(nn∉x₁ a₁x₁≈a₂x₂)
((Symm (eq≈ₐ X)) (nna₁≈nna₂ a₁x₁≈a₂x₂))
; Trans = λ {a₁x₁} {a₂x₂} {a₃x₃} → λ a₁x₁≈a₂x₂ a₂x₂≈a₃x₃ →
let csup = ((some_supp X) (proj₂ a₁x₁)) ++ (((some_supp X) (proj₂ a₂x₂)) ++ ((some_supp X) (proj₂ a₃x₃)))
in let b = outside csup
in let b∉x = outside∉ csup
in let b∉x₁ = (∉⊆₁ {(some_supp X) (proj₂ a₁x₁)}{((some_supp X) (proj₂ a₂x₂)) ++ ((some_supp X) (proj₂ a₃x₃))} b b∉x)
in let b∉x₂ = (∉⊆₁ {(some_supp X) (proj₂ a₂x₂)}{(some_supp X) (proj₂ a₃x₃)} b (∉⊆₂ {(some_supp X) (proj₂ a₁x₁)}{((some_supp X) (proj₂ a₂x₂)) ++ ((some_supp X) (proj₂ a₃x₃))} b b∉x))
in let b∉x₃ = (∉⊆₂ {(some_supp X) (proj₂ a₂x₂)}{(some_supp X) (proj₂ a₃x₃)} b (∉⊆₂ {(some_supp X) (proj₂ a₁x₁)}{((some_supp X) (proj₂ a₂x₂)) ++ ((some_supp X) (proj₂ a₃x₃))} b b∉x))
in let x₁≈x₂ = (nna₁≈nna₂ (Some⇒Anyα {X = X} a₁x₁≈a₂x₂ b b∉x₁ b∉x₂))
in let x₂≈x₃ = (nna₁≈nna₂ (Some⇒Anyα {X = X} a₂x₂≈a₃x₃ b b∉x₂ b∉x₃))
in NName b b∉x₁ b∉x₃ ((Trans (eq≈ₐ X)) x₁≈x₂ x₂≈x₃)
}
≈α : (X : Nominal) → (x₁ x₂ : Aₛ X) → (a₁ a₂ : Atom) → a₁ ≡ a₂ → (≈ₐ X) x₁ x₂ → α X (a₁ , x₁) (a₂ , x₂)
≈α X x₁ x₂ a .a refl x₁≈x₂ = let csup = ((some_supp X) x₁) ++ ((some_supp X) x₂)
in let b = outside csup
in let b∉x = outside∉ csup
in let b∉x₁ = ∉⊆₁ {(some_supp X) x₁}{(some_supp X) x₂} b b∉x
in let b∉x₂ = ∉⊆₂ {(some_supp X) x₁}{(some_supp X) x₂} b b∉x
in let bax₁≈bax₂ = (res X) (λ {x} → (P≡≈ [(b , a)]){x}) x₁≈x₂
in NName b b∉x₁ b∉x₂ bax₁≈bax₂
unch : {X : Nominal} → (x : Aₛ X) → (a b c d : Atom) → b ∉ (some_supp X) x → c ∉ (some_supp X) x → d ∉ (some_supp X) x → (≈ₐ X) ((Act X) [(d , (PermAct [(b , c)] a))] x) ((Act X) [(d , a)] x)
unch {X} x a b c d b∉x c∉x d∉x with AtEqDec a b | AtEqDec a c
unch {X} x .b b c d b∉x c∉x d∉x | yes refl | _ =
(((Act X) [(d , c)] x)
≣< x and ((Act X) [(d , b)] x) by (≈ₐ X) as (eq≈ₐ X) on
((suppAx X) x d c d∉x c∉x) >
(x
≣< ((Act X) [(d , b)] x) and ((Act X) [(d , b)] x) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((suppAx X) x d b d∉x b∉x)) >
(((Act X) [(d , b)] x) by (≈ₐ X) as (eq≈ₐ X) ▴)))
unch {X} x .c b c d b∉x c∉x d∉x | no _ | yes refl =
(((Act X) [(d , b)] x)
≣< x and ((Act X) [(d , c)] x) by (≈ₐ X) as (eq≈ₐ X) on
((suppAx X) x d b d∉x b∉x) >
(x
≣< ((Act X) [(d , c)] x) and ((Act X) [(d , c)] x) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((suppAx X) x d c d∉x c∉x)) >
(((Act X) [(d , c)] x) by (≈ₐ X) as (eq≈ₐ X) ▴)))
unch {X} x a b c d b∉x c∉x d∉x | no a≠b | no a≠c = (Reflex (eq≈ₐ X)) {(Act X) [(d , a)] x}
[A]_ : (X : Nominal) → Nominal
[A] X = record { Aₛ = Atom × (Aₛ X)
; ≈ₐ = α X
; eq≈ₐ = α≈ X
; Act = λ π → λ ax → ((PermAct π (proj₁ ax)) , ((Act X) π (proj₂ ax)))
; res = λ {π₁}{π₂}{a₁x₁}{a₂x₂} → λ π₁≈π₂ → λ a₁x₁≈a₂x₂ →
let c5 = ((some_supp X) ((Act X) π₁ (proj₂ a₁x₁))) ++ ((some_supp X) ((Act X) π₂ (proj₂ a₂x₂)))
in let c4 = ((some_supp X) (proj₂ a₂x₂)) ++ c5
in let c3 = ((some_supp X) (proj₂ a₁x₁)) ++ c4
in let c2 = (flatten π₂) ++ c3
in let c1 = (flatten π₁) ++ c2
in let b = outside c1
in let b∉c = outside∉ c1
in let b∉π₁ = ∉⊆₁ {flatten π₁}{c2} b b∉c
in let b∉π₂ = ∉⊆₁ {flatten π₂}{c3} b (∉⊆₂ {flatten π₁}{c2} b b∉c)
in let b∉x₁ = ∉⊆₁ {(some_supp X) (proj₂ a₁x₁)}{c4} b (∉⊆₂ {flatten π₂}{c3} b (∉⊆₂ {flatten π₁}{c2} b b∉c))
in let b∉x₂ = ∉⊆₁ {(some_supp X) (proj₂ a₂x₂)}{c5} b (∉⊆₂ {(some_supp X) (proj₂ a₁x₁)}{c4} b (∉⊆₂ {flatten π₂}{c3} b (∉⊆₂ {flatten π₁}{c2} b b∉c)))
in let b∉π₁x₁ = ∉⊆₁ {(some_supp X) ((Act X) π₁ (proj₂ a₁x₁))}{(some_supp X) ((Act X) π₂ (proj₂ a₂x₂))} b
(∉⊆₂ {(some_supp X) (proj₂ a₂x₂)}{c5} b (∉⊆₂ {(some_supp X) (proj₂ a₁x₁)}{c4} b (∉⊆₂ {flatten π₂}{c3} b (∉⊆₂ {flatten π₁}{c2} b b∉c))))
in let b∉π₂x₂ = ∉⊆₂ {(some_supp X) ((Act X) π₁ (proj₂ a₁x₁))}{(some_supp X) ((Act X) π₂ (proj₂ a₂x₂))} b
(∉⊆₂ {(some_supp X) (proj₂ a₂x₂)}{c5} b (∉⊆₂ {(some_supp X) (proj₂ a₁x₁)}{c4} b (∉⊆₂ {flatten π₂}{c3} b (∉⊆₂ {flatten π₁}{c2} b b∉c))))
in let x₁≈x₂ = (nna₁≈nna₂ (Some⇒Anyα {X = X} a₁x₁≈a₂x₂ b b∉x₁ b∉x₂))
in
let π₁x₁≈π₂x₂ = (((Act X) [(b , (PermAct π₁ (proj₁ a₁x₁)))] ((Act X) π₁ (proj₂ a₁x₁)))
≣< ((Act X) [((PermAct π₁ (proj₁ a₁x₁)) , b)] ((Act X) π₁ (proj₂ a₁x₁)))
and ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (ab=ba b (PermAct π₁ (proj₁ a₁x₁))) {x}) (≈≡ (eq≈ₐ X) {(Act X) π₁ (proj₂ a₁x₁)} {(Act X) π₁ (proj₂ a₁x₁)} refl)) >
(((Act X) [((PermAct π₁ (proj₁ a₁x₁)) , b)] ((Act X) π₁ (proj₂ a₁x₁)))
≣< ((Act X) (π₁ ++ [((PermAct π₁ (proj₁ a₁x₁)) , b)]) (proj₂ a₁x₁))
and ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) [((PermAct π₁ (proj₁ a₁x₁)) , b)] π₁ {proj₂ a₁x₁}) >
(((Act X) (π₁ ++ [((PermAct π₁ (proj₁ a₁x₁)) , b)]) (proj₂ a₁x₁))
≣< ((Act X) ([ ((proj₁ a₁x₁) , b)] ++ π₁) (proj₂ a₁x₁))
and ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (πabπ≈πab π₁ (proj₁ a₁x₁) b b∉π₁) {x})(≈≡ (eq≈ₐ X) {proj₂ a₁x₁}{proj₂ a₁x₁} refl)) >
(((Act X) ([ ((proj₁ a₁x₁) , b)] ++ π₁) (proj₂ a₁x₁))
≣< ((Act X) π₁ ((Act X) [((proj₁ a₁x₁) , b)] (proj₂ a₁x₁)))
and ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X))((p₁p₂↠ X) π₁ [((proj₁ a₁x₁) , b)] {proj₂ a₁x₁})) >
(((Act X) π₁ ((Act X) [((proj₁ a₁x₁) , b)] (proj₂ a₁x₁)))
≣< ((Act X) π₁ ((Act X) [(b , (proj₁ a₁x₁))] (proj₂ a₁x₁)))
and ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) on
((res X)(λ {x} → P≡≈ π₁ {x})((res X)(λ {x} → ab=ba (proj₁ a₁x₁) b {x})
(≈≡ (eq≈ₐ X) {proj₂ a₁x₁}{proj₂ a₁x₁} refl))) >
(((Act X) π₁ ((Act X) [(b , (proj₁ a₁x₁))] (proj₂ a₁x₁)))
≣< ((Act X) π₂ ((Act X) [(b , (proj₁ a₂x₂))] (proj₂ a₂x₂)))
and ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → π₁≈π₂ {x}) x₁≈x₂) >
(((Act X) π₂ ((Act X) [(b , (proj₁ a₂x₂))] (proj₂ a₂x₂)))
≣< ((Act X) π₂ ((Act X) [((proj₁ a₂x₂) , b)] (proj₂ a₂x₂)))
and ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) on
((res X)(λ {x} → P≡≈ π₂ {x})((res X)(λ {x} → ab=ba b (proj₁ a₂x₂) {x})(≈≡ (eq≈ₐ X) {proj₂ a₂x₂}{proj₂ a₂x₂} refl))) >
(((Act X) π₂ ((Act X) [((proj₁ a₂x₂) , b)] (proj₂ a₂x₂)))
≣< ((Act X) ([((proj₁ a₂x₂) , b)] ++ π₂) (proj₂ a₂x₂))
and ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) π₂ [((proj₁ a₂x₂) , b)] {proj₂ a₂x₂}) >
(((Act X) ([((proj₁ a₂x₂) , b)] ++ π₂) (proj₂ a₂x₂))
≣< ((Act X) ( π₂ ++ [((PermAct π₂ (proj₁ a₂x₂)) , b)]) (proj₂ a₂x₂))
and ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X))((res X) (πabπ≈πab π₂ (proj₁ a₂x₂) b
b∉π₂)(≈≡ (eq≈ₐ X) {proj₂ a₂x₂}{proj₂ a₂x₂} refl))) >
(((Act X) ( π₂ ++ [((PermAct π₂ (proj₁ a₂x₂)) , b)]) (proj₂ a₂x₂))
≣< ((Act X) [((PermAct π₂ (proj₁ a₂x₂)) , b)] ((Act X) π₂ (proj₂ a₂x₂)))
and ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X))((p₁p₂↠ X) [((PermAct π₂ (proj₁ a₂x₂)) , b)] π₂ {proj₂ a₂x₂})) >
(((Act X) [((PermAct π₂ (proj₁ a₂x₂)) , b)] ((Act X) π₂ (proj₂ a₂x₂)))
≣< ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂)))
and ((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (ab=ba (PermAct π₂ (proj₁ a₂x₂)) b) {x})
(≈≡ (eq≈ₐ X) {(Act X) π₂ (proj₂ a₂x₂)}{(Act X) π₂ (proj₂ a₂x₂)} refl)) >
(((Act X) [(b , (PermAct π₂ (proj₁ a₂x₂)))] ((Act X) π₂ (proj₂ a₂x₂))) by (≈ₐ X) as (eq≈ₐ X) ▴))))))))))))
in NName b b∉π₁x₁ b∉π₂x₂ π₁x₁≈π₂x₂
; p₁p₂↠ = λ π₁ π₂ → λ {ax} → ≈α X ((Act X) π₁ (Act X π₂ (proj₂ ax))) ((Act X) (π₂ ++ π₁) (proj₂ ax)) (PermAct π₁ (PermAct π₂ (proj₁ ax))) (PermAct (π₂ ++ π₁) (proj₁ ax))
((p₁p₂↠ NominalAtom) π₁ π₂ {proj₁ ax}) ((p₁p₂↠ X) π₁ π₂ {proj₂ ax})
; ι↠ = λ {ax} → ≈α X ((Act X) ι (proj₂ ax)) (proj₂ ax) (PermAct ι (proj₁ ax)) (proj₁ ax) ((ι↠ NominalAtom) {proj₁ ax}) ((ι↠ X) {proj₂ ax})
; some_supp = λ ax → (some_supp X) (proj₂ ax)
; suppAx = λ ax → λ b c b∉x c∉x →
let csup = ((some_supp X) (proj₂ ax)) ++ ((some_supp X)((Act X) [(b , c)] (proj₂ ax)))
in let d = outside csup
in let d∉xx = outside∉ csup
in let d∉x = ∉⊆₁ {(some_supp X) (proj₂ ax)}{(some_supp X)((Act X) [(b , c)] (proj₂ ax))} d d∉xx
in let d∉x' = ∉⊆₂ {(some_supp X) (proj₂ ax)}{(some_supp X)((Act X) [(b , c)] (proj₂ ax))} d d∉xx
in let x≈x = (Symm (eq≈ₐ X)) (((Act X) [(d , (proj₁ ax))] (proj₂ ax))
≣< ((Act X) [(d , (PermAct [(b , c)] (proj₁ ax)))] (proj₂ ax)) and ((Act X) [(d , (PermAct [(b , c)] (proj₁ ax)))] ((Act X) [(b , c)] (proj₂ ax))) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) (unch {X} (proj₂ ax) (proj₁ ax) b c d b∉x c∉x d∉x)) >
(((Act X) [(d , (PermAct [(b , c)] (proj₁ ax)))] (proj₂ ax))
≣< ((Act X) [(d , (PermAct [(b , c)] (proj₁ ax)))] ((Act X) [(b , c)] (proj₂ ax))) and ((Act X) [(d , (PermAct [(b , c)] (proj₁ ax)))] ((Act X) [(b , c)] (proj₂ ax))) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → P≡≈ [(d , (PermAct [(b , c)] (proj₁ ax)))] {x}) ((suppAx X) (proj₂ ax) b c b∉x c∉x))) >
(((Act X) [(d , (PermAct [(b , c)] (proj₁ ax)))] ((Act X) [(b , c)] (proj₂ ax))) by (≈ₐ X) as (eq≈ₐ X) ▴)))
in NName d d∉x' d∉x x≈x
}
[A]f : (X Y : Nominal) → (F : Equivar X Y) → Equivar ([A] X) ([A] Y)
[A]f X Y F = record { ufun = λ ax → ((proj₁ ax) , ((ufun F) (proj₂ ax)))
; eqi≈ = λ {a₁x₁} {a₂x₂} → λ a₁x₁≈a₂x₂ →
let x₁ = proj₂ a₁x₁
in let x₂ = proj₂ a₂x₂
in let a₁ = proj₁ a₁x₁
in let a₂ = proj₁ a₂x₂
in let c3 = (some_supp X) x₁ ++ ((some_supp X) x₂)
in let c2 = (some_supp Y) ((ufun F) x₂) ++ c3
in let c1 = (some_supp Y) ((ufun F) x₁) ++ c2
in let b = outside c1
in let b∉c = outside∉ c1
in let b∉x₁ = ∉⊆₁ {(some_supp X) x₁}{(some_supp X) x₂} b (∉⊆₂ {(some_supp Y) ((ufun F) x₂)}{c3} b (∉⊆₂ {(some_supp Y) ((ufun F) x₁)}{c2} b b∉c))
in let b∉x₂ = ∉⊆₂ {(some_supp X) x₁}{(some_supp X) x₂} b (∉⊆₂ {(some_supp Y) ((ufun F) x₂)}{c3} b (∉⊆₂ {(some_supp Y) ((ufun F) x₁)}{c2} b b∉c))
in let b∉fx₁ = ∉⊆₁ {(some_supp Y) ((ufun F) x₁)}{c2} b b∉c
in let b∉fx₂ = ∉⊆₁ {(some_supp Y) ((ufun F) x₂)}{c3} b (∉⊆₂ {(some_supp Y) ((ufun F) x₁)}{c2} b b∉c)
in let ba₁a₂ = (nna₁≈nna₂ (Some⇒Anyα {X = X} a₁x₁≈a₂x₂ b b∉x₁ b∉x₂))
in let fx₁≈fx₂ = ( ((Act Y) [ (b , a₁) ] (ufun F x₁))
≣< ((ufun F) ((Act X) [ (b , a₁) ] x₁))
and ((Act Y) [ (b , a₂) ] (ufun F x₂))
by (≈ₐ Y) as (eq≈ₐ Y) on
((equiv F) [ (b , a₁) ] x₁) >
( ((ufun F) ((Act X) [ (b , a₁) ] x₁))
≣< ((ufun F) ((Act X) [ (b , a₂) ] x₂))
and ((Act Y) [ (b , a₂) ] (ufun F x₂))
by (≈ₐ Y) as (eq≈ₐ Y) on ((eqi≈ F) ba₁a₂) >
( ((ufun F) ((Act X) [ (b , a₂) ] x₂))
≣< ((Act Y) [ (b , a₂) ] (ufun F x₂))
and ((Act Y) [ (b , a₂) ] (ufun F x₂))
by (≈ₐ Y) as (eq≈ₐ Y) on
(Symm (eq≈ₐ Y))((equiv F) [ (b , a₂) ] x₂) >
( ((Act Y) [ (b , a₂) ] (ufun F x₂)) by (≈ₐ Y) as (eq≈ₐ Y) ▴))))
in NName b b∉fx₁ b∉fx₂ fx₁≈fx₂
; equiv = λ π → λ ax → ≈α Y ((Act Y) π ((ufun F) (proj₂ ax))) ((ufun F) ((Act X) π (proj₂ ax))) (PermAct π (proj₁ ax)) (PermAct π (proj₁ ax)) refl ((equiv F) π (proj₂ ax))
}
NomAbs : Functor NomCat NomCat
NomAbs = record { onObj = λ X → [A] X
; onMor = λ X Y → λ F → [A]f X Y F
; res≈ = λ X Y → λ F G → λ F≈G → λ ax → ≈α Y ((ufun F)(proj₂ ax)) ((ufun G)(proj₂ ax)) (proj₁ ax) (proj₁ ax) refl (F≈G (proj₂ ax))
; onId = λ X → λ ax → ≈α X (proj₂ ax) (proj₂ ax) (proj₁ ax) (proj₁ ax) refl ((Reflex (eq≈ₐ X)){proj₂ ax})
; onComp = λ X Y Z → λ F G → λ ax → ≈α Z (((ufun G) ∘ (ufun F))(proj₂ ax)) (((ufun G) ∘ (ufun F))(proj₂ ax)) (proj₁ ax) (proj₁ ax) refl (Reflex (eq≈ₐ Z){((ufun G) ∘ (ufun F))(proj₂ ax)})
}
bby≈y : {Y : Nominal} → (y : Aₛ Y) → (b : Atom) → (≈ₐ Y) ((Act Y) [(b , b)] y) y
bby≈y {Y} y b = (((Act Y) [(b , b)] y) ≣< ((Act Y) ι y) and y by (≈ₐ Y) as (eq≈ₐ Y) on ((res Y) (λ {x} → aa≈ι b {x}) (≈≡ (eq≈ₐ Y) {y}{y} refl)) >
(((Act Y) ι y) ≣< y and y by (≈ₐ Y) as (eq≈ₐ Y) on ((ι↠ Y) {y}) > (y by (≈ₐ Y) as (eq≈ₐ Y) ▴)))
∉⇒# : {b : Atom} → (X : Nominal) → (x : Aₛ X) → b ∉ (some_supp X) x → # {X} b x
∉⇒# {b} X x b∉x = fresh b b∉x (bby≈y {Y = X} x b)
ax₁≈ax₂ : {X : Nominal}{ax₁ : (Aₛ ([A] X))}{ax₂ : (Aₛ ([A] X))} → (proj₁ ax₁ ≡ proj₁ ax₂) → NewName {X} ax₁ ax₂ → (≈ₐ X) (proj₂ ax₁) (proj₂ ax₂)
ax₁≈ax₂ {X}{(a , x₁)}{(.a , x₂)} refl NN = let b = (nn NN) in let ax₁≈x₂ = (nna₁≈nna₂ NN)
in let x≈x = (x₁
≣< ((Act X) ι x₁) and x₂ by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X))((ι↠ X) {x₁})) >
(((Act X) ι x₁)
≣< ((Act X) ([(b , a)] ++ [(b , a)]) x₁) and x₂ by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {x} → bc+bc=ι b a {x}) (≈≡ (eq≈ₐ X) {x₁}{x₁} refl))) >
(((Act X) ([(b , a)] ++ [(b , a)]) x₁)
≣< ((Act X) [(b , a)] ((Act X) [(b , a)] x₁)) and x₂ by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((p₁p₂↠ X) [(b , a)] [(b , a)] {x₁})) >
(((Act X) [(b , a)] ((Act X) [(b , a)] x₁))
≣< ((Act X) [(b , a)] ((Act X) [(b , a)] x₂)) and x₂ by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → P≡≈ [(b , a)] {x}) ax₁≈x₂) >
(((Act X) [(b , a)] ((Act X) [(b , a)] x₂))
≣< ((Act X) ([(b , a)] ++ [(b , a)]) x₂) and x₂ by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) [(b , a)] [(b , a)] {x₂}) >
(((Act X) ([(b , a)] ++ [(b , a)]) x₂)
≣< ((Act X) ι x₂) and x₂ by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → bc+bc=ι b a {x}) (≈≡ (eq≈ₐ X) {x₂} {x₂} refl)) >
(((Act X) ι x₂)
≣< x₂ and x₂ by (≈ₐ X) as (eq≈ₐ X) on
((ι↠ X) {x₂}) >
(x₂ by (≈ₐ X) as (eq≈ₐ X) ▴))))))))
in x≈x
a'bx≈x : {X : Nominal}{ax : (Aₛ ([A] X))}{a' b : Atom} → (a'#ax : # {[A] X} a' ax) → b ∉ (some_supp X) (proj₂ ax) → (proj₁ ax) ≠ b → (proj₁ ax) ≠ a' → (≈ₐ X) ((Act X) [(a' , b)] (proj₂ ax)) (proj₂ ax)
a'bx≈x {X}{(a , x)}{a'}{b} a'#ax b∉x a≠b a≠a' = let a'bx≈ax = fixed (Some⇒any {X = [A] X} a'#ax b b∉x)
in ax₁≈ax₂ {X = X} (swapabc≡c a' b a a≠a' a≠b) a'bx≈ax
ax≈a'a'ax : {X : Nominal}{ax : (Aₛ ([A] X))}{a' : Atom} → (a'#ax : # {[A] X} a' ax) → NewName {X} ax (a' , ((Act X) [(a' , (proj₁ ax))] (proj₂ ax)))
ax≈a'a'ax {X}{(a , x)}{a'} a'#ax with AtEqDec a a'
ax≈a'a'ax {X} {(a , x)}{.a} a'#ax | yes refl = let x≈aax = (x ≣< ((Act X) ι x) and ((Act X) [(a , a)] x) by (≈ₐ X) as (eq≈ₐ X) on ((Symm (eq≈ₐ X))((ι↠ X) {x})) >
(((Act X) ι x) ≣< ((Act X) [(a , a)] x) and ((Act X) [(a , a)] x) by (≈ₐ X) as (eq≈ₐ X) on ((Symm (eq≈ₐ X)) ((res X) (λ {x} → aa≈ι a {x}) (≈≡ (eq≈ₐ X) {x}{x} refl))) >
(((Act X) [(a , a)] x) by (≈ₐ X) as (eq≈ₐ X) ▴)))
in ≈α X x ((Act X) [(a , a)] x) a a refl x≈aax
ax≈a'a'ax {X} {(a , x)} {a'} a'#ax | no a≠a' = let csup = [ a ] ++ (((some_supp X) x) ++ ((some_supp X) ((Act X) [(a' , a)] x)))
in let b = outside csup
in let b∉c = outside∉ csup
in let a≠b = ∉⟶≠ b a (∉⊆₁ {[ a ]}{((some_supp X) x) ++ ((some_supp X) ((Act X) [(a' , a)] x))} b b∉c)
in let b∉x = ∉⊆₁ {(some_supp X) x}{(some_supp X) ((Act X) [(a' , a)] x)} b (∉⊆₂ {[ a ]}{((some_supp X) x) ++ ((some_supp X) ((Act X) [(a' , a)] x))} b b∉c)
in let b∉a'ax = ∉⊆₂ {(some_supp X) x}{(some_supp X) ((Act X) [(a' , a)] x)} b (∉⊆₂ {[ a ]}{((some_supp X) x) ++ ((some_supp X) ((Act X) [(a' , a)] x))} b b∉c)
in let a'bx = a'bx≈x {X = X} a'#ax b∉x a≠b a≠a'
in let x≈a'ax = (((Act X) [(b , a)] x)
≣< ((Act X) ([(b , a')] ++ ([(a' , a)] ++ [(b , a')])) x) and ((Act X) [(b , a')] ((Act X) [(a' , a)] x)) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → ac≈ab+bc+ab b a' a a≠b a≠a' {x}) (≈≡ (eq≈ₐ X) {x}{x} refl)) >
(((Act X) ([(b , a')] ++ ([(a' , a)] ++ [(b , a')])) x)
≣< ((Act X) ([(a' , a)] ++ [(b , a')]) ((Act X) [(b , a')] x)) and ((Act X) [(b , a')] ((Act X) [(a' , a)] x)) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((p₁p₂↠ X) ([(a' , a)] ++ [(b , a')]) [(b , a')] {x})) >
(((Act X) ([(a' , a)] ++ [(b , a')]) ((Act X) [(b , a')] x))
≣< ((Act X) ([(a' , a)] ++ [(b , a')]) ((Act X) [(a' , b)] x)) and ((Act X) [(b , a')] ((Act X) [(a' , a)] x)) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → P≡≈ ([(a' , a)] ++ [(b , a')]) {x}) ((res X) (λ {x} → ab=ba b a' {x}) (≈≡ (eq≈ₐ X) {x} {x} refl))) >
(((Act X) ([(a' , a)] ++ [(b , a')]) ((Act X) [(a' , b)] x))
≣< ((Act X) ([(a' , a)] ++ [(b , a')]) x) and ((Act X) [(b , a')] ((Act X) [(a' , a)] x)) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → P≡≈ ([(a' , a)] ++ [(b , a')]) {x}) (a'bx≈x {X = X} a'#ax b∉x a≠b a≠a')) >
(((Act X) ([(a' , a)] ++ [(b , a')]) x)
≣< ((Act X) [(b , a')] ((Act X) [(a' , a)] x)) and ((Act X) [(b , a')] ((Act X) [(a' , a)] x)) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((p₁p₂↠ X) [(b , a')] [(a' , a)] {x})) >
(((Act X) [(b , a')] ((Act X) [(a' , a)] x)) by (≈ₐ X) as (eq≈ₐ X) ▴))))))
in NName b b∉x b∉a'ax x≈a'ax
fresh[A] : {X : Nominal}{a₁x₁ a₂x₂ : (Aₛ ([A] X))} → ((proj₁ a₁x₁) ∉ ((some_supp ([A] X)) a₁x₁)) → ((proj₁ a₂x₂) ∉ ((some_supp ([A] X)) a₂x₂)) → (≈ₐ ([A] X)) a₁x₁ a₂x₂ → (≈ₐ X) (proj₂ a₁x₁) (proj₂ a₂x₂)
fresh[A] {X} {(a₁ , x₁)} {(a₂ , x₂)} a₁∉x₁ a₂∉x₂ a₁x₁≈a₂x₂ = let x₁ₛ = (some_supp X) x₁ in let x₂ₛ = (some_supp X) x₂ in let xₛ = x₁ₛ ++ x₂ₛ in let b = outside xₛ in
let b∉x₁₂ = outside∉ xₛ in let b∉x₁ = ∉⊆₁ {x₁ₛ}{x₂ₛ} b b∉x₁₂ in let b∉x₂ = ∉⊆₂ {x₁ₛ}{x₂ₛ} b b∉x₁₂ in
let a₁bx₁ = ax≈a'a'ax {X = X} (∉⇒# ([A] X) (a₁ , x₁) b∉x₁) in let a₂bx₂ = ax≈a'a'ax {X = X} (∉⇒# ([A] X) (a₂ , x₂) b∉x₂) in
let bx₁x₂ = (Trans (eq≈ₐ ([A] X))) ((Symm (eq≈ₐ ([A] X))) a₁bx₁) ((Trans (eq≈ₐ ([A] X))) a₁x₁≈a₂x₂ a₂bx₂) in
let ba₁x₁≈ba₂x₂ = ax₁≈ax₂ {X = X} (b ▪) bx₁x₂ in
let x₁≈x₂ = (x₁ ≣< ((Act X) [(b , a₁)] x₁) and x₂ by (≈ₐ X) as (eq≈ₐ X) on ((Symm (eq≈ₐ X)) ((suppAx X) x₁ b a₁ b∉x₁ a₁∉x₁)) >
(((Act X) [(b , a₁)] x₁) ≣< ((Act X) [(b , a₂)] x₂) and x₂ by (≈ₐ X) as (eq≈ₐ X) on ba₁x₁≈ba₂x₂ >
(((Act X) [(b , a₂)] x₂) ≣< x₂ and x₂ by (≈ₐ X) as (eq≈ₐ X) on ((suppAx X) x₂ b a₂ b∉x₂ a₂∉x₂) >
(x₂ by (≈ₐ X) as (eq≈ₐ X) ▴)))) in x₁≈x₂