module NameAbst where

{-
This file contains the definition and basic properties of name abstraction.
It also defines the name abstraction functor.
-}

open import Basics
open import Atoms
open import Perms
open import PermProp
open import Nom
open import CatDef
open import FreshNom

--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
--(a₁ , x₁) ≈ (a₂ , x₂) definition
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

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 

------------------------------------------------------------------------------------------------------------------------------
--equivalence relation
------------------------------------------------------------------------------------------------------------------------------

α : (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 theorem
-------------------------------------------------------------------------------------------------------------------------------

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₃)
                        }

---------------------------------------------------------------------------------------------------------------------
--a₁ ≡ a₂ ∧ x₁ ≈ x₂ ⇒ (a₁ , x₁) ≈ (a₂ , 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} 

------------------------------------------------------------------------------------------------------------------------------
--Name abstraction functor on objects
------------------------------------------------------------------------------------------------------------------------------

[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
                          } 


------------------------------------------------------------------------------------------------------------------------------------------
--Name abstraction functor on morphisms
------------------------------------------------------------------------------------------------------------------------------------------

[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))
                               } 
 

---------------------------------------------------------------------------------------------------------------------------------------
--Name Abstraction functor
---------------------------------------------------------------------------------------------------------------------------------------

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)})
                              } 

--------------------------------------------------------------------------------------------------------------------------------------------
--Properties of Name Abstraction
-------------------------------------------------------------------------------------------------------------------------------------------

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)

------------------------------------------------------------------------------------------------------------------------------
--(a , x₁) ≈ (a , x₂) ⇒ x₁ ≈ x₂
------------------------------------------------------------------------------------------------------------------------------

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


---------------------------------------------------------------------------------------------------------------------------------------------------
--(a , x) ≈ (a' , (a' a) x) , provided a' # x
---------------------------------------------------------------------------------------------------------------------------------------------------
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 


-------------------------------------------------------------------------------------------------------------------------------------------------------------------
--(a₁ , x₁) ≈ (a₂ , x₂) and a₁ # x₁ , a₂ # x₂ ⇒ x₁ ≈ x₂
-------------------------------------------------------------------------------------------------------------------------------------------------------------------

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₂    
----------------------------------------------------------------------------------------------------------------------------------------------------------------------