module FreshCon where
open import Basics
open import Atoms
open import Perms
open import PermProp
open import Nom
open import CatDef
open import FreshNom
open import NameAbst
record spFunfs (X Y : Nominal) : Set where
field
ufs : Funfs (Prod NominalAtom X) Y
confs : (a : Atom) → a ∉ (fsupp ufs) → (x : Aₛ X) → a ∉ (some_supp Y) ((ffun ufs) (a , x))
open spFunfs public
record uFunfs (X Y : Nominal) (F : spFunfs X Y) : Set where
field
uufs : Funfs ([A] X) Y
sufs : (a : Atom) → a ∉ (fsupp (ufs F)) → (x : Aₛ X) → (≈ₐ Y) ((ffun (ufs F)) (a , x)) ((ffun uufs) (a , x))
↑fs : (G : Funfs ([A] X) Y) → (∀ (a : Atom) → a ∉ (fsupp (ufs F)) → (x : Aₛ X) → (≈ₐ Y) ((ffun (ufs F)) (a , x)) ((ffun G) (a , x))) → ≈fs G uufs
a₁→a₃f : (X Y : Nominal)(F : spFunfs X Y)(a₁ a₃ : Atom)(x : Aₛ X) → a₁ ∉ (fsupp (ufs F)) → a₃ ∉ (fsupp (ufs F)) → a₃ ∉ (some_supp X) x → a₃ ∉ (some_supp Y) ((ffun (ufs F)) (a₁ , x))
→ (≈ₐ Y) ((ffun (ufs F)) (a₁ , x)) ((ffun (ufs F)) (a₃ , ((Act X) [(a₃ , a₁)] x)))
a₁→a₃f X Y F a₁ a₃ x a₁∉f a₃∉f a₃∉x a₃∉fx = let a₃a₁x₁ = ((PermAct [(a₃ , a₁)] a₁) , ((Act X) [(a₃ , a₁)] x)) in let a₃x₁ = (a₃ , ((Act X) [(a₃ , a₁)] x)) in
let a₃a₁x₁≈a₃a₁x₁ = a₃a₁x₁ ≣< a₃x₁ and a₃x₁ by (≈ₐ (Prod NominalAtom X)) as (eq≈ₐ (Prod NominalAtom X)) on
((swapabb≡a a₃ a₁) , (≈≡ (eq≈ₐ X) {(Act X) [(a₃ , a₁)] x}{(Act X) [(a₃ , a₁)] x} refl)) >
(a₃x₁ by (≈ₐ (Prod NominalAtom X)) as (eq≈ₐ (Prod NominalAtom X)) ▴) in
let fa₁x = (ffun (ufs F)) (a₁ , x) in let fa₃x = (ffun (ufs F)) (a₃ , ((Act X) [(a₃ , a₁)] x)) in
let final = fa₁x ≣< ((Act Y) [(a₃ , a₁)] fa₁x) and fa₃x by (≈ₐ Y) as (eq≈ₐ Y) on
((Symm (eq≈ₐ Y)) ((suppAx Y) fa₁x a₃ a₁ a₃∉fx ((confs F) a₁ a₁∉f x))) >
(((Act Y) [(a₃ , a₁)] fa₁x)
≣< ((Act Y) [(a₃ , a₁)] ((Act Y) [(a₃ , a₁)] ((ffun (ufs F)) a₃a₁x₁ ))) and fa₃x by (≈ₐ Y) as (eq≈ₐ Y) on
((Symm (eq≈ₐ Y)) ((res Y) (λ {w} → P≡≈ [(a₃ , a₁)] {w}) ((fsuppAx (ufs F)) a₃ a₁ a₃∉f a₁∉f (a₁ , x)))) >
(((Act Y) [(a₃ , a₁)] ((Act Y) [(a₃ , a₁)] ((ffun (ufs F)) a₃a₁x₁ )))
≣< ((Act Y) [(a₃ , a₁)] ((Act Y) [(a₃ , a₁)] ((ffun (ufs F)) a₃x₁))) and fa₃x by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(a₃ , a₁)] {w}) ((res Y) (λ {w} → P≡≈ [(a₃ , a₁)] {w}) ((feqi≈ (ufs F)) a₃a₁x₁≈a₃a₁x₁))) >
(((Act Y) [(a₃ , a₁)] ((Act Y) [(a₃ , a₁)] ((ffun (ufs F)) a₃x₁)))
≣< ((Act Y) ([(a₃ , a₁)] ++ [(a₃ , a₁)]) fa₃x) and fa₃x by (≈ₐ Y) as (eq≈ₐ Y) on
((p₁p₂↠ Y) [(a₃ , a₁)] [(a₃ , a₁)] {fa₃x}) >
(((Act Y) ([(a₃ , a₁)] ++ [(a₃ , a₁)]) fa₃x)
≣< ((Act Y) ι fa₃x) and fa₃x by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → bc+bc=ι a₃ a₁ {w}) (≈≡ (eq≈ₐ Y) {fa₃x}{fa₃x} refl)) >
(((Act Y) ι fa₃x)
≣< fa₃x and fa₃x by (≈ₐ Y) as (eq≈ₐ Y) on
((ι↠ Y) {fa₃x}) >
(fa₃x by (≈ₐ Y) as (eq≈ₐ Y) ▴)))))) in final
a₁x₁≈f : (X Y : Nominal)(F : spFunfs X Y) → (a₁x₁ a₂x₂ : Aₛ ([A] X)) → (≈ₐ ([A] X)) a₁x₁ a₂x₂ → ((proj₁ a₁x₁) ∉ (fsupp (ufs F))) → ((proj₁ a₂x₂) ∉ (fsupp (ufs F))) →
(≈ₐ Y) ((ffun (ufs F)) ((proj₁ a₁x₁) , (proj₂ a₁x₁))) ((ffun (ufs F)) ((proj₁ a₂x₂) , (proj₂ a₂x₂)))
a₁x₁≈f X Y F (a₁ , x₁) (a₂ , x₂) a₁x₁≈a₂x₂ a₁∉f a₂∉f = let fx₁ = (ffun (ufs F)) (a₁ , x₁) in let fx₂ = (ffun (ufs F)) (a₂ , x₂) in
let x₁ₛ = (some_supp X) x₁ in let x₂ₛ = (some_supp X) x₂ in let y₁ₛ = (some_supp Y) fx₁ in let y₂ₛ = (some_supp Y) fx₂ in
let fₛ = fsupp (ufs F) in let ℓ₁ = x₁ₛ ++ x₂ₛ in let ℓ₂ = y₂ₛ ++ ℓ₁ in let ℓ₃ = y₁ₛ ++ ℓ₂ in let ℓ₄ = fₛ ++ ℓ₃ in
let b = outside ℓ₄ in let b∉l₄ = outside∉ ℓ₄ in let b∉f = ∉⊆₁ {fₛ}{ℓ₃} b b∉l₄ in let b∉l₃ = ∉⊆₂ {fₛ}{ℓ₃} b b∉l₄ in
let b∉y₁ = ∉⊆₁ {y₁ₛ}{ℓ₂} b b∉l₃ in let b∉l₂ = ∉⊆₂ {y₁ₛ}{ℓ₂} b b∉l₃ in let b∉y₂ = ∉⊆₁ {y₂ₛ}{ℓ₁} b b∉l₂ in let b∉l₁ = ∉⊆₂ {y₂ₛ}{ℓ₁} b b∉l₂ in
let b∉x₁ = ∉⊆₁ {x₁ₛ}{x₂ₛ} b b∉l₁ in let b∉x₂ = ∉⊆₂ {x₁ₛ}{x₂ₛ} b b∉l₁ in
let a₁a₃ = a₁→a₃f X Y F a₁ b x₁ a₁∉f b∉f b∉x₁ b∉y₁ in let a₂a₃ = a₁→a₃f X Y F a₂ b x₂ a₂∉f b∉f b∉x₂ b∉y₂ in
let a₁a₂a₃ = nna₁≈nna₂ (Some⇒Anyα {X = X} a₁x₁≈a₂x₂ b b∉x₁ b∉x₂) in
let final = fx₁ ≣< ((ffun (ufs F)) (b , ((Act X) [(b , a₁)] x₁))) and fx₂ by (≈ₐ Y) as (eq≈ₐ Y) on a₁a₃ >
(((ffun (ufs F)) (b , ((Act X) [(b , a₁)] x₁)))
≣< ((ffun (ufs F)) (b , ((Act X) [(b , a₂)] x₂))) and fx₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((feqi≈ (ufs F)) ((b ▪) , a₁a₂a₃)) >
(((ffun (ufs F)) (b , ((Act X) [(b , a₂)] x₂)))
≣< fx₂ and fx₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((Symm (eq≈ₐ Y)) a₂a₃) >
(fx₂ by (≈ₐ Y) as (eq≈ₐ Y) ▴))) in final
sp2ufs : (X Y : Nominal) → (F : spFunfs X Y) → uFunfs X Y F
sp2ufs X Y F = record { uufs = record { ffun = λ ax → let (a , x) = ax in let fₛ = (fsupp (ufs F)) in let xₛ = (some_supp X) x in
let fₛxₛ = a :: (fₛ ++ xₛ) in let b = outside fₛxₛ in let bax = (Act X) [(b , a)] x in
(ffun (ufs F)) (b , bax)
; fsupp = (fsupp (ufs F))
; fsuppAx = λ b c b∉f c∉f ax → let (a , x) = ax in let bca = PermAct [(b , c)] a in let bcx = (Act X) [(b , c)] x in let bcxₛ = (some_supp X) bcx in let fₛ = (fsupp (ufs F)) in
let b'ₛ = bca :: (fₛ ++ bcxₛ) in let b' = outside b'ₛ in let b'∉l = outside∉ b'ₛ in let bca≠b' = des≠ b'∉l in let b'∉ll = des∉ b'∉l in
let b'∉f = ∉⊆₁ {fₛ}{bcxₛ} b' b'∉ll in let b'∉bcx = ∉⊆₂ {fₛ}{bcxₛ} b' b'∉ll in let x' = (Act X) [(b' , bca)] bcx in
let y₁ = (ffun (ufs F)) (b' , x') in let yₛ = (some_supp Y) y₁ in let xₛ = (some_supp X) x in
let m₁ = xₛ ++ yₛ in let m₂ = fₛ ++ m₁ in let m₃ = bcxₛ ++ m₂ in let m₄ = b :: (c :: (bca :: m₃)) in
let d = outside m₄ in let d∉l = outside∉ m₄ in let b≠d = des≠ d∉l in let d∉n₁ = des∉ d∉l in
let c≠d = des≠ d∉n₁ in let d∉n₂ = des∉ d∉n₁ in let bca≠d = des≠ d∉n₂ in let d∉n₃ = des∉ d∉n₂ in
let d∉bcx = ∉⊆₁ {bcxₛ}{m₂} d d∉n₃ in let d∉m₂ = ∉⊆₂ {bcxₛ}{m₂} d d∉n₃ in
let d∉f = ∉⊆₁ {fₛ}{m₁} d d∉m₂ in let d∉m₁ = ∉⊆₂ {fₛ}{m₁} d d∉m₂ in
let d∉x = ∉⊆₁ {xₛ}{yₛ} d d∉m₁ in let d∉y₁ = ∉⊆₂ {xₛ}{yₛ} d d∉m₁ in let y₂ = (ffun (ufs F)) (d , ((Act X) [(d , a)] x)) in
let final = ((Act Y) [(b , c)] y₁)
≣< ((Act Y) [(b , c)] ((Act Y) [(d , b')] y₁)) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((Symm (eq≈ₐ Y)) ((res Y) (λ {w} → P≡≈ [(b , c)] {w}) ((suppAx Y) y₁ d b' d∉y₁ ((confs F) b' b'∉f x')))) >
(((Act Y) [(b , c)] ((Act Y) [(d , b')] y₁))
≣< ((Act Y) [(b , c)] ((ffun (ufs F)) ((Act ([A] X)) [(d , b')] (b' , x')))) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(b , c)] {w}) (fsch (Prod NominalAtom X) Y (ufs F) (b' , x') d∉f b'∉f)) >
(((Act Y) [(b , c)] ((ffun (ufs F)) ((Act ([A] X)) [(d , b')] (b' , x'))))
≣< ((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) [(d , b')] x')))) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(b , c)] {w}) ((feqi≈ (ufs F)) ((swapabb≡a d b') , (≈≡ (eq≈ₐ X) {(Act X) [(d , b')] x'}{(Act X) [(d , b')] x'} refl)))) >
(((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) [(d , b')] x'))))
≣< ((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) ([(b' , bca)] ++ [(d , b')]) bcx)))) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(b , c)] {w}) ((feqi≈ (ufs F)) ((d ▪) , ((p₁p₂↠ X) [(d , b')] [(b' , bca)] {bcx})))) >
(((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) ([(b' , bca)] ++ [(d , b')]) bcx))))
≣< ((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) ([(b' , bca)] ++ [(d , b')]) ((Act X) [(d , b')] bcx))))) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(b , c)] {w}) ((feqi≈ (ufs F)) ((d ▪) , ((res X) (λ {w} → P≡≈ ([(b' , bca)] ++ [(d , b')]) {w})
((Symm (eq≈ₐ X)) ((suppAx X) bcx d b' d∉bcx b'∉bcx)))))) >
(((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) ([(b' , bca)] ++ [(d , b')]) ((Act X) [(d , b')] bcx)))))
≣< ((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) ([(d , b')] ++ ([(b' , bca)] ++ [(d , b')])) bcx)))) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(b , c)] {w}) ((feqi≈ (ufs F)) ((d ▪) , ((p₁p₂↠ X) ([(b' , bca)] ++ [(d , b')]) [(d , b')] {bcx})))) >
(((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) ([(d , b')] ++ ([(b' , bca)] ++ [(d , b')])) bcx))))
≣< ((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) [(d , bca)] bcx)))) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(b , c)] {w}) ((feqi≈ (ufs F)) ((d ▪) ,
((Symm (eq≈ₐ X)) ((res X) (λ {w} → ac≈ab+bc+ab d b' bca bca≠d bca≠b' {w}) (≈≡ (eq≈ₐ X) {bcx}{bcx} refl)))))) >
(((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) [(d , bca)] bcx))))
≣< ((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) ([(b , c)] ++ [(d , bca)]) x)))) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(b , c)] {w}) ((feqi≈ (ufs F)) ((d ▪) , ((p₁p₂↠ X) [(d , bca)] [(b , c)] {x})))) >
(((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) ([(b , c)] ++ [(d , bca)]) x))))
≣< ((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) ([(d , a)] ++ [(b , c)]) x)))) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(b , c)] {w}) ((feqi≈ (ufs F)) ((d ▪) , ((res X) (λ {w} →
bπaπ≈πab [(b , c)] d a (a∉as (a∉as a∉[] c≠d) b≠d) {w}) (≈≡ (eq≈ₐ X) {x}{x} refl))))) >
(((Act Y) [(b , c)] ((ffun (ufs F)) (d , ((Act X) ([(d , a)] ++ [(b , c)]) x))))
≣< ((Act Y) [(b , c)] ((ffun (ufs F)) ((PermAct [(b , c)] d) , ((Act X) [(b , c)] ((Act X) [(d , a)] x))))) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(b , c)] {w}) ((feqi≈ (ufs F)) ((sym (swapabc≡c b c d (syma≡b⊥ b≠d) (syma≡b⊥ c≠d))) ,
((Symm (eq≈ₐ X)) ((p₁p₂↠ X) [(b , c)] [(d , a)] {x}))))) >
(((Act Y) [(b , c)] ((ffun (ufs F)) ((PermAct [(b , c)] d) , ((Act X) [(b , c)] ((Act X) [(d , a)] x)))))
≣< y₂ and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((fsuppAx (ufs F)) b c b∉f c∉f (d , ((Act X) [(d , a)] x))) >
(y₂ by (≈ₐ Y) as (eq≈ₐ Y) ▴))))))))))) in
let pₛ = a :: (fₛ ++ xₛ) in let a' = outside pₛ in let a'∉l = des∉ (outside∉ pₛ) in let a'∉x = ∉⊆₂ {fₛ}{xₛ} a' a'∉l in let a'∉f = ∉⊆₁ {fₛ}{xₛ} a' a'∉l in
let y₃ = (ffun (ufs F)) (a' , ((Act X) [(a' , a)] x)) in
let d≈a' = (Trans (eq≈ₐ ([A] X))) ((Symm (eq≈ₐ ([A] X))) (ax≈a'a'ax {X = X} (∉⇒# ([A] X) (a , x) d∉x))) (ax≈a'a'ax {X = X} (∉⇒# ([A] X) (a , x) a'∉x)) in
let ul = a₁x₁≈f X Y F (d , ((Act X) [(d , a)] x)) (a' , ((Act X) [(a' , a)] x)) d≈a' d∉f a'∉f in
let final' = (Trans (eq≈ₐ Y)) final ul in final'
; feqi≈ = λ {a₁x₁}{a₂x₂} a₁x₁≈a₂x₂ → let (a₁ , x₁) = a₁x₁ in let (a₂ , x₂) = a₂x₂ in let x₁ₛ = (some_supp X) x₁ in let x₂ₛ = (some_supp X) x₂ in
let fₛ = (fsupp (ufs F)) in let a₁' = outside (a₁ :: (fₛ ++ x₁ₛ)) in let a₁'∉f = ∉⊆₁ {fₛ}{x₁ₛ} a₁' (des∉ (outside∉ (a₁ :: (fₛ ++ x₁ₛ)))) in
let a₁'∉x₁ = ∉⊆₂ {fₛ}{x₁ₛ} a₁' (des∉ (outside∉ (a₁ :: (fₛ ++ x₁ₛ)))) in let a₂' = outside (a₂ :: (fₛ ++ x₂ₛ)) in
let a₂'∉f = ∉⊆₁ {fₛ}{x₂ₛ} a₂' (des∉ (outside∉ (a₂ :: (fₛ ++ x₂ₛ)))) in let a₂'∉x₂ = ∉⊆₂ {fₛ}{x₂ₛ} a₂' (des∉ (outside∉ (a₂ :: (fₛ ++ x₂ₛ)))) in
let a₁'≈a₂' = (Trans (eq≈ₐ ([A] X)))
((Symm (eq≈ₐ ([A] X))) (ax≈a'a'ax {X = X} (∉⇒# ([A] X) (a₁ , x₁) a₁'∉x₁)))
((Trans (eq≈ₐ ([A] X))) a₁x₁≈a₂x₂ (ax≈a'a'ax {X = X} (∉⇒# ([A] X) (a₂ , x₂) a₂'∉x₂)))
in let a₁'a₁x = (Act X) [(a₁' , a₁)] x₁ in let a₂'a₂x = (Act X) [(a₂' , a₂)] x₂ in
a₁x₁≈f X Y F (a₁' , a₁'a₁x) (a₂' , a₂'a₂x) a₁'≈a₂' a₁'∉f a₂'∉f
}
; sufs = λ a a∉f x → let fₛ = (fsupp (ufs F)) in let xₛ = (some_supp X) x in let cₛ = a :: (fₛ ++ xₛ) in let b = outside cₛ in let b∉fx = des∉ (outside∉ cₛ) in
let b∉f = ∉⊆₁ {fₛ}{xₛ} b b∉fx in let b∉x = ∉⊆₂ {fₛ}{xₛ} b b∉fx in let a≈b = ax≈a'a'ax {X = X} (∉⇒# ([A] X) (a , x) b∉x) in
let bax = (Act X) [(b , a)] x in a₁x₁≈f X Y F (a , x) (b , bax) a≈b a∉f b∉f
; ↑fs = λ G GC ax → let (a , x) = ax in let fₛ = (fsupp (ufs F)) in let xₛ = (some_supp X) x in let cₛ = a :: (fₛ ++ xₛ) in let b = outside cₛ in let b∉fx = des∉ (outside∉ cₛ) in
let b∉f = ∉⊆₁ {fₛ}{xₛ} b b∉fx in let b∉x = ∉⊆₂ {fₛ}{xₛ} b b∉fx in let a≈b = ax≈a'a'ax {X = X} (∉⇒# ([A] X) (a , x) b∉x) in
let bax = (Act X) [(b , a)] x in let fbx = ((ffun (ufs F)) (b , ((Act X) [(b , a)] x))) in
let final = ((ffun G) ax) ≣< ((ffun G) (b , bax)) and fbx by (≈ₐ Y) as (eq≈ₐ Y) on ((feqi≈ G) a≈b) >
(((ffun G) (b , bax)) ≣< fbx and fbx by (≈ₐ Y) as (eq≈ₐ Y) on (Symm (eq≈ₐ Y)) (GC b b∉f bax) >
(fbx by (≈ₐ Y) as (eq≈ₐ Y) ▴)) in final
}
record spEquiv (X Y Z : Nominal) : Set where
field
ueq : Equivar (Prod X (Prod NominalAtom Y)) Z
coneq : (a : Atom)(x : Aₛ X) → a ∉ ((some_supp X) x) → (y : Aₛ Y) → a ∉ (some_supp Z) ((ufun ueq) (x , (a , y)))
open spEquiv public
record uEquiv (X Y Z : Nominal) (F : spEquiv X Y Z) : Set where
field
uueq : Equivar (Prod X ([A] Y)) Z
sueq : (a : Atom)(x : Aₛ X) → a ∉ ((some_supp X) x) → (y : Aₛ Y) → (≈ₐ Z) ((ufun uueq) (x , (a , y))) ((ufun (ueq F)) (x , (a , y)))
↑eq : (G : Equivar (Prod X ([A] Y)) Z) → (∀ (a : Atom)(x : Aₛ X) → a ∉ ((some_supp X) x) → (y : Aₛ Y) → (≈ₐ Z) ((ufun G) (x , (a , y))) ((ufun (ueq F)) (x , (a , y)))) → ≈̬ G uueq
αresseq : (X Y Z : Nominal)(F : spEquiv X Y Z)(x : Aₛ X) → {a₁y₁ a₂y₂ : (Aₛ ([A] Y))} → (proj₁ a₁y₁) ∉ ((some_supp X) x) → (proj₁ a₂y₂) ∉ ((some_supp X) x) → (≈ₐ ([A] Y)) a₁y₁ a₂y₂
→ (≈ₐ Z) ((ufun (ueq F)) (x , ((proj₁ a₁y₁) , (proj₂ a₁y₁)))) ((ufun (ueq F)) (x , ((proj₁ a₂y₂) , (proj₂ a₂y₂))))
αresseq X Y Z F x {a₁y₁} {a₂y₂} a₁∉x a₂∉x a₁y₁≈a₂y₂ = let (a₁ , y₁) = a₁y₁ in let (a₂ , y₂) = a₂y₂ in let fy₁ = (ufun (ueq F)) (x , (a₁ , y₁)) in let fy₂ = (ufun (ueq F)) (x , (a₂ , y₂)) in
let z₁ₛ = (some_supp Z) fy₁ in let z₂ₛ = (some_supp Z) fy₂ in let xₛ = (some_supp X) x in let y₁ₛ = (some_supp Y) y₁ in let y₂ₛ = (some_supp Y) y₂ in
let m₁ = (y₁ₛ ++ y₂ₛ) in let m₂ = xₛ ++ m₁ in let m₃ = z₂ₛ ++ m₂ in let m₄ = z₁ₛ ++ m₃ in let b = outside m₄ in let b∉m₄ = outside∉ m₄ in
let b∉z₁ = ∉⊆₁ {z₁ₛ}{m₃} b b∉m₄ in let b∉m₃ = ∉⊆₂ {z₁ₛ}{m₃} b b∉m₄ in let b∉z₂ = ∉⊆₁ {z₂ₛ}{m₂} b b∉m₃ in let b∉m₂ = ∉⊆₂ {z₂ₛ}{m₂} b b∉m₃ in
let b∉x = ∉⊆₁ {xₛ}{m₁} b b∉m₂ in let b∉m₁ = ∉⊆₂ {xₛ}{m₁} b b∉m₂ in let b∉y₁ = ∉⊆₁ {y₁ₛ}{y₂ₛ} b b∉m₁ in let b∉y₂ = ∉⊆₂ {y₁ₛ}{y₂ₛ} b b∉m₁ in
let ba₁y₁≈ba₂y₂ = nna₁≈nna₂ (Some⇒Anyα {X = Y} a₁y₁≈a₂y₂ b b∉y₁ b∉y₂) in
let final = fy₁
≣< ((Act Z) [(b , a₁)] fy₁) and fy₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((Symm (eq≈ₐ Z)) ((suppAx Z) fy₁ b a₁ b∉z₁ ((coneq F) a₁ x a₁∉x y₁))) >
(((Act Z) [(b , a₁)] fy₁)
≣< ((ufun (ueq F)) (((Act X) [(b , a₁)] x) , (((Act NominalAtom) [(b , a₁)] a₁) , ((Act Y) [(b , a₁)] y₁)))) and fy₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((equiv (ueq F)) [(b , a₁)] (x , (a₁ , y₁))) >
(((ufun (ueq F)) (((Act X) [(b , a₁)] x) , (((Act NominalAtom) [(b , a₁)] a₁) , ((Act Y) [(b , a₁)] y₁))))
≣< ((ufun (ueq F)) (x , (b , ((Act Y) [(b , a₂)] y₂)))) and fy₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((eqi≈ (ueq F)) (((suppAx X) x b a₁ b∉x a₁∉x) , ((swapabb≡a b a₁) , ba₁y₁≈ba₂y₂))) >
(((ufun (ueq F)) (x , (b , ((Act Y) [(b , a₂)] y₂))))
≣< ((ufun (ueq F)) (((Act X) [(b , a₂)] x) , ((PermAct [(b , a₂)] a₂) , ((Act Y) [(b , a₂)] y₂)))) and fy₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((eqi≈ (ueq F)) (((Symm (eq≈ₐ X)) ((suppAx X) x b a₂ b∉x a₂∉x)) , ((sym (swapabb≡a b a₂)) , (≈≡ (eq≈ₐ Y) {(Act Y) [(b , a₂)] y₂}{(Act Y) [(b , a₂)] y₂} refl)))) >
(((ufun (ueq F)) (((Act X) [(b , a₂)] x) , ((PermAct [(b , a₂)] a₂) , ((Act Y) [(b , a₂)] y₂))))
≣< ((Act Z) [(b , a₂)] fy₂) and fy₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((Symm (eq≈ₐ Z)) ((equiv (ueq F)) [(b , a₂)] (x , (a₂ , y₂)))) >
(((Act Z) [(b , a₂)] fy₂)
≣< fy₂ and fy₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((suppAx Z) fy₂ b a₂ b∉z₂ ((coneq F) a₂ x a₂∉x y₂)) >
(fy₂ by (≈ₐ Z) as (eq≈ₐ Z) ▴)))))) in final
sp2ueq : (X Y Z : Nominal)(F : spEquiv X Y Z) → uEquiv X Y Z F
sp2ueq X Y Z F = record { uueq = record { ufun = λ xay → let (x , (a , y)) = xay in let a' = outside (a :: (((some_supp X) x) ++ ((some_supp Y) y))) in (ufun (ueq F)) (x , (a' , ((Act Y) [(a' , a)] y)))
; eqi≈ = λ {x₁a₁y₁}{x₂a₂y₂} x₁a₁y₁≈x₂a₂y₂ → let (x₁ , (a₁ , y₁)) = x₁a₁y₁ in let (x₂ , (a₂ , y₂)) = x₂a₂y₂ in let y₁ₛ = (some_supp Y) y₁ in let y₂ₛ = (some_supp Y) y₂ in
let x₁ₛ = (some_supp X) x₁ in let x₂ₛ = (some_supp X) x₂ in let a'₁ = outside (a₁ :: (x₁ₛ ++ y₁ₛ)) in let a'₂ = outside (a₂ :: (x₂ₛ ++ y₂ₛ)) in
let z₁ = (ufun (ueq F)) (x₁ , (a'₁ , ((Act Y) [(a'₁ , a₁)] y₁))) in let z₂ = (ufun (ueq F)) (x₂ , (a'₂ , ((Act Y) [(a'₂ , a₂)] y₂))) in
let (x₁≈x₂ , a₁y₁≈a₂y₂) = x₁a₁y₁≈x₂a₂y₂ in let a'₁∉l = des∉ (outside∉ (a₁ :: (x₁ₛ ++ y₁ₛ))) in let a'₂∉l = des∉ (outside∉ (a₂ :: (x₂ₛ ++ y₂ₛ))) in
let a'₁∉x₁ = ∉⊆₁ {x₁ₛ}{y₁ₛ} a'₁ a'₁∉l in let a'₁∉y₁ = ∉⊆₂ {x₁ₛ}{y₁ₛ} a'₁ a'₁∉l in
let a'₂∉x₂ = ∉⊆₁ {x₂ₛ}{y₂ₛ} a'₂ a'₂∉l in let a'₂∉y₂ = ∉⊆₂ {x₂ₛ}{y₂ₛ} a'₂ a'₂∉l in
let m₁ = x₁ₛ ++ x₂ₛ in let m₂ = y₂ₛ ++ m₁ in let m₃ = y₁ₛ ++ m₂ in
let b = outside m₃ in let b∉m₃ = outside∉ m₃ in let b∉y₁ = ∉⊆₁ {y₁ₛ}{m₂} b b∉m₃ in let b∉m₂ = ∉⊆₂ {y₁ₛ}{m₂} b b∉m₃ in
let b∉y₂ = ∉⊆₁ {y₂ₛ}{m₁} b b∉m₂ in let b∉m₁ = ∉⊆₂ {y₂ₛ}{m₁} b b∉m₂ in
let b∉x₁ = ∉⊆₁ {x₁ₛ}{x₂ₛ} b b∉m₁ in let b∉x₂ = ∉⊆₂ {x₁ₛ}{x₂ₛ} b b∉m₁ in
let a'₁a₃y₁ = (Trans (eq≈ₐ ([A] Y))) ((Symm (eq≈ₐ ([A] Y))) (ax≈a'a'ax {X = Y} (∉⇒# ([A] Y) (a₁ , y₁) a'₁∉y₁)))
(ax≈a'a'ax {X = Y} (∉⇒# ([A] Y) (a₁ , y₁) b∉y₁)) in
let a'₂a₃y₂ = (Trans (eq≈ₐ ([A] Y))) ((Symm (eq≈ₐ ([A] Y))) (ax≈a'a'ax {X = Y} (∉⇒# ([A] Y) (a₂ , y₂) a'₂∉y₂)))
(ax≈a'a'ax {X = Y} (∉⇒# ([A] Y) (a₂ , y₂) b∉y₂)) in
let a₃a₁y₁≈a₃a₂y₂ = nna₁≈nna₂ (Some⇒Anyα {X = Y} a₁y₁≈a₂y₂ b b∉y₁ b∉y₂) in
let fa₁≈fa₃ = αresseq X Y Z F x₁ a'₁∉x₁ b∉x₁ a'₁a₃y₁ in let fa₂≈fa₃ = αresseq X Y Z F x₂ a'₂∉x₂ b∉x₂ a'₂a₃y₂ in
let final = z₁
≣< ((ufun (ueq F)) (x₁ , (b , ((Act Y) [(b , a₁)] y₁)))) and z₂ by (≈ₐ Z) as (eq≈ₐ Z) on
fa₁≈fa₃ >
(((ufun (ueq F)) (x₁ , (b , ((Act Y) [(b , a₁)] y₁))))
≣< ((ufun (ueq F)) (x₂ , (b , ((Act Y) [(b , a₂)] y₂)))) and z₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((eqi≈ (ueq F)) (x₁≈x₂ , ((b ▪) , a₃a₁y₁≈a₃a₂y₂))) >
(((ufun (ueq F)) (x₂ , (b , ((Act Y) [(b , a₂)] y₂))))
≣< z₂ and z₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((Symm (eq≈ₐ Z)) fa₂≈fa₃) >
(z₂ by (≈ₐ Z) as (eq≈ₐ Z) ▴))) in final
; equiv = λ π xay → let (x , (a , y)) = xay in let πa = PermAct π a in let πx = (Act X) π x in let πy = (Act Y) π y in let xₛ = (some_supp X) x in
let πxₛ = (some_supp X) πx in let yₛ = (some_supp Y) y in let πyₛ = (some_supp Y) πy in let πₛ = flatten π in
let a' = outside (a :: (xₛ ++ yₛ)) in let a'∉l = des∉ (outside∉ (a :: (xₛ ++ yₛ))) in let a'' = outside (πa :: (πxₛ ++ πyₛ)) in
let a''∉l = des∉ (outside∉ (πa :: (πxₛ ++ πyₛ))) in let a'∉x = ∉⊆₁ {xₛ}{yₛ} a' a'∉l in let a'∉y = ∉⊆₂ {xₛ}{yₛ} a' a'∉l in
let a''∉πx = ∉⊆₁ {πxₛ}{πyₛ} a'' a''∉l in let a''∉πy = ∉⊆₂ {πxₛ}{πyₛ} a'' a''∉l in
let m₁ = xₛ ++ yₛ in let m₂ = πyₛ ++ m₁ in let m₃ = πxₛ ++ m₂ in let m₄ = πₛ ++ m₃ in
let b = outside m₄ in let b∉m₄ = outside∉ m₄ in let b∉π = ∉⊆₁ {πₛ}{m₃} b b∉m₄ in
let b∉m₃ = ∉⊆₂ {πₛ}{m₃} b b∉m₄ in let b∉πx = ∉⊆₁ {πxₛ}{m₂} b b∉m₃ in let b∉m₂ = ∉⊆₂ {πxₛ}{m₂} b b∉m₃ in
let b∉πy = ∉⊆₁ {πyₛ}{m₁} b b∉m₂ in let b∉m₁ = ∉⊆₂ {πyₛ}{m₁} b b∉m₂ in let b∉x = ∉⊆₁ {xₛ}{yₛ} b b∉m₁ in
let b∉y = ∉⊆₂ {xₛ}{yₛ} b b∉m₁ in let z₁ = (ufun (ueq F)) (x , (a' , ((Act Y) [(a' , a)] y))) in let z₂ = (ufun (ueq F)) (πx , (a'' , ((Act Y) [(a'' , πa)] πy)))
in let a'by = (Trans (eq≈ₐ ([A] Y))) ((Symm (eq≈ₐ ([A] Y))) (ax≈a'a'ax {X = Y} (∉⇒# ([A] Y) (a , y) a'∉y)))
(ax≈a'a'ax {X = Y} (∉⇒# ([A] Y) (a , y) b∉y)) in
let a''bπy = (Trans (eq≈ₐ ([A] Y))) ((Symm (eq≈ₐ ([A] Y))) (ax≈a'a'ax {X = Y} (∉⇒# ([A] Y) (πa , πy) a''∉πy)))
(ax≈a'a'ax {X = Y} (∉⇒# ([A] Y) (πa , πy) b∉πy)) in
let fa≈fb = αresseq X Y Z F x a'∉x b∉x a'by in let fπa≈fb = αresseq X Y Z F πx a''∉πx b∉πx a''bπy in
let final = ((Act Z) π z₁)
≣< ((Act Z) π ((ufun (ueq F)) (x , (b , ((Act Y) [(b , a)] y))))) and z₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((res Z) (λ {w} → P≡≈ π {w}) fa≈fb) >
(((Act Z) π ((ufun (ueq F)) (x , (b , ((Act Y) [(b , a)] y)))))
≣< ((ufun (ueq F)) (πx , ((PermAct π b) , ((Act Y) π ((Act Y) [(b , a)] y))))) and z₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((equiv (ueq F)) π (x , (b , ((Act Y) [(b , a)] y)))) >
(((ufun (ueq F)) (πx , ((PermAct π b) , ((Act Y) π ((Act Y) [(b , a)] y)))))
≣< ((ufun (ueq F)) (πx , (b , ((Act Y) ([(b , a)] ++ π) y)))) and z₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((eqi≈ (ueq F)) ((≈≡ (eq≈ₐ X) {πx}{πx} refl) , ((pa≡a π b b∉π) , ((p₁p₂↠ Y) π [(b , a)] {y})))) >
(((ufun (ueq F)) (πx , (b , ((Act Y) ([(b , a)] ++ π) y))))
≣< ((ufun (ueq F)) (πx , (b , ((Act Y) (π ++ [(b , πa)]) y)))) and z₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((eqi≈ (ueq F)) ((≈≡ (eq≈ₐ X) {πx}{πx} refl) , ((b ▪) , ((Symm (eq≈ₐ Y)) ((res Y) (λ {w} → bπaπ≈πab π b a b∉π)
(≈≡ (eq≈ₐ Y) {y}{y} refl)))))) >
(((ufun (ueq F)) (πx , (b , ((Act Y) (π ++ [(b , πa)]) y))))
≣< ((ufun (ueq F)) (πx , (b , ((Act Y) [(b , πa)] πy)))) and z₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((eqi≈ (ueq F)) ((≈≡ (eq≈ₐ X) {πx}{πx} refl) , ((b ▪) , ((Symm (eq≈ₐ Y)) ((p₁p₂↠ Y) [(b , πa)] π {y}))))) >
(((ufun (ueq F)) (πx , (b , ((Act Y) [(b , πa)] πy))))
≣< z₂ and z₂ by (≈ₐ Z) as (eq≈ₐ Z) on
((Symm (eq≈ₐ Z)) fπa≈fb) >
(z₂ by (≈ₐ Z) as (eq≈ₐ Z) ▴)))))) in final
}
; sueq = λ a x a∉x y → let xₛ = (some_supp X) x in let yₛ = (some_supp Y) y in let cₛ = a :: (xₛ ++ yₛ) in let a' = outside cₛ in let a'∉l = des∉ (outside∉ cₛ) in
let a'∉x = ∉⊆₁ {xₛ}{yₛ} a' a'∉l in let a'∉y = ∉⊆₂ {xₛ}{yₛ} a' a'∉l in let a≈a' = ax≈a'a'ax {X = Y} (∉⇒# ([A] Y) (a , y) a'∉y) in
(Symm (eq≈ₐ Z)) (αresseq X Y Z F x a∉x a'∉x a≈a')
; ↑eq = λ G Con xay → let (x , (a , y)) = xay in let xₛ = (some_supp X) x in let yₛ = (some_supp Y) y in let cₛ = (a :: (xₛ ++ yₛ)) in let a' = (outside cₛ) in
let a'∉l = (des∉ (outside∉ cₛ)) in let a'∉x = ∉⊆₁ {xₛ}{yₛ} a' a'∉l in let a'∉y = ∉⊆₂ {xₛ}{yₛ} a' a'∉l in
let a≈a' = ax≈a'a'ax {X = Y} (∉⇒# ([A] Y) (a , y) a'∉y) in
let gay≈ga'y = (eqi≈ G) ((≈≡ (eq≈ₐ X) {x}{x} refl) , a≈a') in (Trans (eq≈ₐ Z)) gay≈ga'y (Con a' x a'∉x ((Act Y) [(a' , a)] y))
}