module AbsProp where
{-
This file proves some of the properties of name abstraction.
-}
open import Basics
open import Atoms
open import Perms
open import PermProp
open import Nom
open import CatDef
open import FreshNom
open import NameAbst
------------------------------------------------------------------------------------------------------------------
--[A] (X₁ + X₂) ≅ [A] X₁ + [A] X₂
-----------------------------------------------------------------------------------------------------------------
ColimRes : (X₁ X₂ : Nominal) → Iso {NomCat} ([A] (Sum X₁ X₂)) (Sum ([A] X₁) ([A] X₂))
ColimRes X₁ X₂ = record { liso = record { ufun = λ { (a , inl x₁) → inl (a , x₁)
; (a , inr x₂) → inr (a , x₂)
}
; eqi≈ = λ { {(a₁ , inl x₁)}{(a₁' , inl x₁')} → λ a₁x₁≈a₁'x₁' → NName (nn a₁x₁≈a₁'x₁') (nn∉x₁ a₁x₁≈a₁'x₁') (nn∉x₂ a₁x₁≈a₁'x₁') (nna₁≈nna₂ a₁x₁≈a₁'x₁')
; {(a₂ , inr x₂)}{(a₂' , inr x₂')} → λ a₂x₂≈a₂'x₂' → NName (nn a₂x₂≈a₂'x₂') (nn∉x₁ a₂x₂≈a₂'x₂') (nn∉x₂ a₂x₂≈a₂'x₂') (nna₁≈nna₂ a₂x₂≈a₂'x₂')
; {(a₁ , inl x₁)}{(a₂ , inr x₂)} → λ x₁≈x₂ → (nna₁≈nna₂ x₁≈x₂)
; {(a₂ , inr x₂)}{(a₁ , inl x₁)} → λ x₂≈x₁ → (nna₁≈nna₂ x₂≈x₁)
}
; equiv = λ π → λ { (a , inl x₁) → (Reflex (eq≈ₐ (Sum ([A] X₁) ([A] X₂)))) { inl ((PermAct π a) , ((Act X₁) π x₁)) }
; (a , inr x₂) → (Reflex (eq≈ₐ (Sum ([A] X₁) ([A] X₂)))) { inr ((PermAct π a) , ((Act X₂) π x₂)) }
}
}
; riso = record { ufun = λ { (inl (a , x₁)) → (a , inl x₁)
; (inr (a , x₂)) → (a , inr x₂)
}
; eqi≈ = λ { {(inl (a₁ , x₁))}{(inl (a₁' , x₁'))} → λ a₁x₁≈a₁'x₁' → NName (nn a₁x₁≈a₁'x₁') (nn∉x₁ a₁x₁≈a₁'x₁') (nn∉x₂ a₁x₁≈a₁'x₁') (nna₁≈nna₂ a₁x₁≈a₁'x₁')
; {(inr (a₂ , x₂))}{(inr (a₂' , x₂'))} → λ a₂x₂≈a₂'x₂' → NName (nn a₂x₂≈a₂'x₂') (nn∉x₁ a₂x₂≈a₂'x₂') (nn∉x₂ a₂x₂≈a₂'x₂') (nna₁≈nna₂ a₂x₂≈a₂'x₂')
; {(inl (a₁ , x₁))}{(inr (a₂ , x₂))} → λ ()
; {(inr (a₂ , x₂))}{(inl (a₁ , x₁))} → λ ()
}
; equiv = λ π → λ { (inl (a , x₁)) → (Reflex (eq≈ₐ ([A] (Sum X₁ X₂)))) {((PermAct π a) , (inl ((Act X₁) π x₁)))}
; (inr (a , x₂)) → (Reflex (eq≈ₐ ([A] (Sum X₁ X₂)))) {((PermAct π a) , (inr ((Act X₂) π x₂)))}
}
}
; idisl = λ { (a , inl x₁) → (Reflex (eq≈ₐ ([A] (Sum X₁ X₂)))) {(a , inl x₁)}
; (a , inr x₂) → (Reflex (eq≈ₐ ([A] (Sum X₁ X₂)))) {(a , inr x₂)}
}
; idisr = λ { (inl (a , x₁)) → (Reflex (eq≈ₐ (Sum ([A] X₁) ([A] X₂)))) {(inl (a , x₁))}
; (inr (a , x₂)) → (Reflex (eq≈ₐ (Sum ([A] X₁) ([A] X₂)))) {(inr (a , x₂))}
}
}
----------------------------------------------------------------------------------------------------------------------------------------
--[A] (X₁ × X₂) ≅ [A] X₁ × [A] X₂
----------------------------------------------------------------------------------------------------------------------------------------
LimRes : (X₁ X₂ : Nominal) → Iso {NomCat} ([A] (Prod X₁ X₂)) (Prod ([A] X₁) ([A] X₂))
LimRes X₁ X₂ = record { liso = record { ufun = λ ax₁x₂ → let a = (proj₁ ax₁x₂) in let x₁x₂ = (proj₂ ax₁x₂) in let x₁ = (proj₁ x₁x₂) in let x₂ = (proj₂ x₁x₂) in ((a , x₁) , (a , x₂))
; eqi≈ = λ {ax₁x₂}{a'x₁x₂} x≈x' → let a = (proj₁ ax₁x₂) in let x₁x₂ = (proj₂ ax₁x₂) in let x₁ = (proj₁ x₁x₂) in let x₂ = (proj₂ x₁x₂) in
let a' = (proj₁ a'x₁x₂) in let x₁x₂' = (proj₂ a'x₁x₂) in let x₁' = (proj₁ x₁x₂') in let x₂' = (proj₂ x₁x₂') in
let b = (nn x≈x') in let b∉x₁x₂ = (nn∉x₁ x≈x') in let b∉x₁x₂' = (nn∉x₂ x≈x') in let baa' = (nna₁≈nna₂ x≈x') in
let x₁ₛ = (some_supp X₁) x₁ in let x₁ₛ' = (some_supp X₁) x₁' in let x₂ₛ = (some_supp X₂) x₂ in let x₂ₛ' = (some_supp X₂) x₂' in
let b∉x₁ = ∉⊆₁ {x₁ₛ}{x₂ₛ} b b∉x₁x₂ in let b∉x₂ = ∉⊆₂ {x₁ₛ}{x₂ₛ} b b∉x₁x₂ in
let b∉x₁' = ∉⊆₁ {x₁ₛ'}{x₂ₛ'} b b∉x₁x₂' in let b∉x₂' = ∉⊆₂ {x₁ₛ'}{x₂ₛ'} b b∉x₁x₂' in
((NName b b∉x₁ b∉x₁' (proj₁ baa')) , (NName b b∉x₂ b∉x₂' (proj₂ baa')))
; equiv = λ π axx → let a = (proj₁ axx) in let xx = (proj₂ axx) in let x₁ = (proj₁ xx) in let x₂ = (proj₂ xx) in let πa = PermAct π a in
let πx₁ = (Act X₁) π x₁ in let πx₂ = (Act X₂) π x₂ in let πx₁≈πx₁ = ≈α X₁ πx₁ πx₁ πa πa refl (≈≡ (eq≈ₐ X₁) {πx₁}{πx₁} refl) in
let πx₂≈πx₂ = ≈α X₂ πx₂ πx₂ πa πa refl (≈≡ (eq≈ₐ X₂) {πx₂}{πx₂} refl) in (πx₁≈πx₁ , πx₂≈πx₂)
}
; riso = record { ufun = λ a₁x₁a₂x₂ → let a₁x₁ = (proj₁ a₁x₁a₂x₂) in let a₂x₂ = (proj₂ a₁x₁a₂x₂) in
let a₁ = (proj₁ a₁x₁) in let x₁ = (proj₂ a₁x₁) in let a₂ = (proj₁ a₂x₂) in let x₂ = (proj₂ a₂x₂) in
let b = outside (a₁ :: (a₂ :: (((some_supp X₁) x₁) ++ ((some_supp X₂) x₂)))) in (b , (((Act X₁) [(b , a₁)] x₁) , ((Act X₂) [(b , a₂)] x₂)))
; eqi≈ = λ {a₁x₁a₂x₂}{a₁x₁a₂x₂'} a₁x₁a₂x₂≈a₁x₁a₂x₂' → let ((a₁ , x₁) , (a₂ , x₂)) = a₁x₁a₂x₂ in let ((a₁' , x₁') , (a₂' , x₂')) = a₁x₁a₂x₂' in
let x₁ₛ = (some_supp X₁) x₁ in let x₂ₛ = (some_supp X₂) x₂ in let x₁ₛ' = (some_supp X₁) x₁' in let x₂ₛ' = (some_supp X₂) x₂' in
let xₛ = (x₁ₛ ++ x₂ₛ) in let xₛ' = (x₁ₛ' ++ x₂ₛ') in let axₛ = (a₁ :: (a₂ :: xₛ)) in let axₛ' = (a₁' :: (a₂' :: xₛ')) in
let b = outside axₛ in let b∉l = outside∉ axₛ in
let a₁≠b = des≠ b∉l in let b∉x₁₂ₛ = des∉ b∉l in let a₂≠b = des≠ b∉x₁₂ₛ in let b∉x₁₂ = des∉ b∉x₁₂ₛ in
let b∉x₁ = ∉⊆₁ {x₁ₛ}{x₂ₛ} b b∉x₁₂ in let b∉x₂ = ∉⊆₂ {x₁ₛ}{x₂ₛ} b b∉x₁₂ in
let b' = outside axₛ' in let b'∉l = outside∉ axₛ' in
let a₁'≠b' = des≠ b'∉l in let b'∉x₁₂ₛ = des∉ b'∉l in let a₂'≠b' = des≠ b'∉x₁₂ₛ in let b'∉x₁₂' = des∉ b'∉x₁₂ₛ in
let b'∉x₁' = ∉⊆₁ {x₁ₛ'}{x₂ₛ'} b' b'∉x₁₂' in let b'∉x₂' = ∉⊆₂ {x₁ₛ'}{x₂ₛ'} b' b'∉x₁₂' in
let ba₁x₁ = ((Act X₁) [(b , a₁)] x₁) in let ba₂x₂ = ((Act X₂) [(b , a₂)] x₂) in let ba₁x₁' = ((Act X₁) [(b' , a₁')] x₁') in let ba₂x₂' = ((Act X₂) [(b' , a₂')] x₂') in
let fx₁ₛ = (some_supp X₁) ba₁x₁ in let fx₂ₛ = (some_supp X₂) ba₂x₂ in let fx₁ₛ' = (some_supp X₁) ba₁x₁' in let fx₂ₛ' = (some_supp X₂) ba₂x₂' in
let fxₛ = fx₁ₛ ++ fx₂ₛ in let fxₛ' = fx₁ₛ' ++ fx₂ₛ' in let fₛ = fxₛ ++ fxₛ' in let uₛ = xₛ ++ xₛ' in let vₛ = uₛ ++ fₛ in let wₛ = (a₁ :: (a₂ :: (a₁' :: (a₂' :: vₛ)))) in
let c = outside wₛ in let c∉ll = outside∉ wₛ in
let a₁≠c = des≠ c∉ll in let c∉l₃ = des∉ c∉ll in let a₂≠c = des≠ c∉l₃ in
let c∉l₂ = des∉ c∉l₃ in let a₁'≠c = des≠ c∉l₂ in let c∉l₁ = des∉ c∉l₂ in let a₂'≠c = des≠ c∉l₁ in let c∉l = des∉ c∉l₁ in
let c∉uₛ = ∉⊆₁ {uₛ}{fₛ} c c∉l in let c∉fₛ = ∉⊆₂ {uₛ}{fₛ} c c∉l in let c∉xₛ = ∉⊆₁ {xₛ}{xₛ'} c c∉uₛ in let c∉xₛ' = ∉⊆₂ {xₛ}{xₛ'} c c∉uₛ in
let c∉fxₛ = ∉⊆₁ {fxₛ}{fxₛ'} c c∉fₛ in let c∉fxₛ' = ∉⊆₂ {fxₛ}{fxₛ'} c c∉fₛ in let c∉x₁ = ∉⊆₁ {x₁ₛ}{x₂ₛ} c c∉xₛ in let c∉x₂ = ∉⊆₂ {x₁ₛ}{x₂ₛ} c c∉xₛ in
let c∉x₁' = ∉⊆₁ {x₁ₛ'}{x₂ₛ'} c c∉xₛ' in let c∉x₂' = ∉⊆₂ {x₁ₛ'}{x₂ₛ'} c c∉xₛ' in
let (a₁x₁≈a₁x₁' , a₂x₂≈a₂x₂') = a₁x₁a₂x₂≈a₁x₁a₂x₂' in
let ca₁≈ca₁' = (nna₁≈nna₂ (Some⇒Anyα {X = X₁} a₁x₁≈a₁x₁' c c∉x₁ c∉x₁')) in
let ca₂≈ca₂' = (nna₁≈nna₂ (Some⇒Anyα {X = X₂} a₂x₂≈a₂x₂' c c∉x₂ c∉x₂')) in
let cx₁≈cx₁' = ((Act X₁) [(c , b)] ba₁x₁)
≣< ((Act X₁) ([(b , a₁)] ++ [(c , b)]) x₁) and ((Act X₁) [(c , b')] ba₁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 , b')] ba₁x₁') by (≈ₐ X₁) as (eq≈ₐ X₁) on
((res X₁) (λ {w} → P≡≈ ([(b , a₁)] ++ [(c , b)]) {w}) ((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 , b')] ba₁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 , b')] ba₁x₁') by (≈ₐ X₁) as (eq≈ₐ X₁) on
((Symm (eq≈ₐ X₁)) ((res X₁) (λ {w} → ac≈ab+bc+ab c b a₁ a₁≠c a₁≠b {w}) (≈≡ (eq≈ₐ X₁) {x₁}{x₁} refl))) >
(((Act X₁) [(c , a₁)] x₁)
≣< ((Act X₁) [(c , a₁')] x₁') and ((Act X₁) [(c , b')] ba₁x₁') by (≈ₐ X₁) as (eq≈ₐ X₁) on
ca₁≈ca₁' >
(((Act X₁) [(c , a₁')] x₁')
≣< ((Act X₁) ([(c , b')] ++ ([(b' , a₁')] ++ [(c , b')])) x₁') and ((Act X₁) [(c , b')] ba₁x₁') by (≈ₐ X₁) as (eq≈ₐ X₁) on
((res X₁) (λ {w} → ac≈ab+bc+ab c b' a₁' a₁'≠c a₁'≠b' {w}) (≈≡ (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 , b')] ba₁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 , b')] ba₁x₁') by (≈ₐ X₁) as (eq≈ₐ X₁) on
((res X₁) (λ {w} → P≡≈ ([(b' , a₁')] ++ [(c , b')]) {w}) ((suppAx X₁) x₁' c b' c∉x₁' b'∉x₁')) >
(((Act X₁) ([(b' , a₁')] ++ [(c , b')]) x₁')
≣< ((Act X₁) [(c , b')] ba₁x₁') and ((Act X₁) [(c , b')] ba₁x₁') by (≈ₐ X₁) as (eq≈ₐ X₁) on
((Symm (eq≈ₐ X₁)) ((p₁p₂↠ X₁) [(c , b')] [(b' , a₁')] {x₁'})) >
(((Act X₁) [(c , b')] ba₁x₁') by (≈ₐ X₁) as (eq≈ₐ X₁) ▴))))))))) in
let cx₂≈cx₂' = ((Act X₂) [(c , b)] ba₂x₂)
≣< ((Act X₂) ([(b , a₂)] ++ [(c , b)]) x₂) and ((Act X₂) [(c , b')] ba₂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 , b')] ba₂x₂') by (≈ₐ X₂) as (eq≈ₐ X₂) on
((res X₂) (λ {w} → P≡≈ ([(b , a₂)] ++ [(c , b)]) {w}) ((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 , b')] ba₂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 , b')] ba₂x₂') by (≈ₐ X₂) as (eq≈ₐ X₂) on
((Symm (eq≈ₐ X₂)) ((res X₂) (λ {w} → ac≈ab+bc+ab c b a₂ a₂≠c a₂≠b {w}) (≈≡ (eq≈ₐ X₂) {x₂}{x₂} refl))) >
(((Act X₂) [(c , a₂)] x₂)
≣< ((Act X₂) [(c , a₂')] x₂') and ((Act X₂) [(c , b')] ba₂x₂') by (≈ₐ X₂) as (eq≈ₐ X₂) on
ca₂≈ca₂' >
(((Act X₂) [(c , a₂')] x₂')
≣< ((Act X₂) ([(c , b')] ++ ([(b' , a₂')] ++ [(c , b')])) x₂') and ((Act X₂) [(c , b')] ba₂x₂') by (≈ₐ X₂) as (eq≈ₐ X₂) on
((res X₂) (λ {w} → ac≈ab+bc+ab c b' a₂' a₂'≠c a₂'≠b' {w}) (≈≡ (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 , b')] ba₂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 , b')] ba₂x₂') by (≈ₐ X₂) as (eq≈ₐ X₂) on
((res X₂) (λ {w} → P≡≈ ([(b' , a₂')] ++ [(c , b')]) {w}) ((suppAx X₂) x₂' c b' c∉x₂' b'∉x₂')) >
(((Act X₂) ([(b' , a₂')] ++ [(c , b')]) x₂')
≣< ((Act X₂) [(c , b')] ba₂x₂') and ((Act X₂) [(c , b')] ba₂x₂') by (≈ₐ X₂) as (eq≈ₐ X₂) on
((Symm (eq≈ₐ X₂)) ((p₁p₂↠ X₂) [(c , b')] [(b' , a₂')] {x₂'})) >
(((Act X₂) [(c , b')] ba₂x₂') by (≈ₐ X₂) as (eq≈ₐ X₂) ▴))))))))) in NName c c∉fxₛ c∉fxₛ' (cx₁≈cx₁' , cx₂≈cx₂')
; equiv = λ π a₁x₁a₂x₂ → let ((a₁ , x₁) , (a₂ , x₂)) = a₁x₁a₂x₂ in let ((πa₁ , πx₁) , (πa₂ , πx₂)) = (Act (Prod ([A] X₁) ([A] X₂))) π a₁x₁a₂x₂ in
let x₁ₛ = (some_supp X₁) x₁ in let x₂ₛ = (some_supp X₂) x₂ in let πx₁ₛ = (some_supp X₁) πx₁ in let πx₂ₛ = (some_supp X₂) πx₂ in
let uₛ = x₁ₛ ++ x₂ₛ in let vₛ = (a₁ :: (a₂ :: uₛ)) in let πuₛ = πx₁ₛ ++ πx₂ₛ in let πvₛ = (πa₁ :: (πa₂ :: πuₛ)) in
let b = outside vₛ in let b' = outside πvₛ in let b∉l = outside∉ vₛ in let b'∉l = outside∉ πvₛ in let πb = (PermAct π b) in
let a₁≠b = des≠ b∉l in let b∉l₁ = des∉ b∉l in let a₂≠b = des≠ b∉l₁ in let b∉x₁₂ = des∉ b∉l₁ in
let b∉x₁ = ∉⊆₁ {x₁ₛ}{x₂ₛ} b b∉x₁₂ in let b∉x₂ = ∉⊆₂ {x₁ₛ}{x₂ₛ} b b∉x₁₂ in
let πa₁≠b' = des≠ b'∉l in let b'∉l₁ = des∉ b'∉l in let πa₂≠b' = des≠ b'∉l₁ in let b'∉πx₁₂ = des∉ b'∉l₁ in
let b'∉πx₁ = ∉⊆₁ {πx₁ₛ}{πx₂ₛ} b' b'∉πx₁₂ in let b'∉πx₂ = ∉⊆₂ {πx₁ₛ}{πx₂ₛ} b' b'∉πx₁₂ in
let πba₁x₁ = (Act X₁) π ((Act X₁) [(b , a₁)] x₁) in let πba₂x₂ = (Act X₂) π ((Act X₂) [(b , a₂)] x₂) in
let b'πa₁πx₁ = (Act X₁) [(b' , πa₁)] πx₁ in let b'πa₂πx₂ = (Act X₂) [(b' , πa₂)] πx₂ in
let t₁ = ((some_supp X₁) πba₁x₁) ++ ((some_supp X₂) πba₂x₂) in let t₂ = ((some_supp X₁) b'πa₁πx₁) ++ ((some_supp X₂) b'πa₂πx₂) in
let tₛ = t₁ ++ t₂ in let m₁ₛ = πuₛ ++ tₛ in let m₂ₛ = uₛ ++ m₁ₛ in let m₃ₛ = (flatten π) ++ m₂ₛ in let m₄ₛ = (a₁ :: (a₂ :: (πa₁ :: (πa₂ :: m₃ₛ)))) in
let c = outside m₄ₛ in let c∉l = outside∉ m₄ₛ in
let a₁≠c = des≠ c∉l in let c∉l₁ = des∉ c∉l in let a₂≠c = des≠ c∉l₁ in let c∉l₂ = des∉ c∉l₁ in let πa₁≠c = des≠ c∉l₂ in let c∉l₃ = des∉ c∉l₂ in
let πa₂≠c = des≠ c∉l₃ in let c∉l₄ = des∉ c∉l₃ in let c∉π = ∉⊆₁ {flatten π}{m₂ₛ} c c∉l₄ in let c∉m₂ₛ = ∉⊆₂ {flatten π}{m₂ₛ} c c∉l₄ in
let c∉uₛ = ∉⊆₁ {uₛ}{m₁ₛ} c c∉m₂ₛ in let c∉x₁ = ∉⊆₁ {x₁ₛ}{x₂ₛ} c c∉uₛ in let c∉x₂ = ∉⊆₂ {x₁ₛ}{x₂ₛ} c c∉uₛ in
let c∉m₁ₛ = ∉⊆₂ {uₛ}{m₁ₛ} c c∉m₂ₛ in
let c∉πuₛ = ∉⊆₁ {πuₛ}{tₛ} c c∉m₁ₛ in let c∉πx₁ = ∉⊆₁ {πx₁ₛ}{πx₂ₛ} c c∉πuₛ in let c∉πx₂ = ∉⊆₂ {πx₁ₛ}{πx₂ₛ} c c∉πuₛ in
let c∉tₛ = ∉⊆₂ {πuₛ}{tₛ} c c∉m₁ₛ in let c∉t₁ = ∉⊆₁ {t₁}{t₂} c c∉tₛ in let c∉t₂ = ∉⊆₂ {t₁}{t₂} c c∉tₛ in
let πca₁x₁ = ((Act X₁) π ((Act X₁) [(c , a₁)] x₁)) in let πca₂x₂ = ((Act X₂) π ((Act X₂) [(c , a₂)] x₂)) in
let prf₁₁ = ((Act X₁) [(c , πb)] πba₁x₁)
≣< ((Act X₁) (π ++ [(c , πb)]) ((Act X₁) [(b , a₁)] x₁)) and πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((p₁p₂↠ X₁) [(c , πb)] π {(Act X₁) [(b , a₁)] x₁}) >
(((Act X₁) (π ++ [(c , πb)]) ((Act X₁) [(b , a₁)] x₁))
≣< ((Act X₁) ([(c , b)] ++ π) ((Act X₁) [(b , a₁)] x₁)) and πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((res X₁) (λ {w} → bπaπ≈πab π c b c∉π {w}) (≈≡ (eq≈ₐ X₁) {(Act X₁) [(b , a₁)] x₁} {(Act X₁) [(b , a₁)] x₁} refl)) >
(((Act X₁) ([(c , b)] ++ π) ((Act X₁) [(b , a₁)] x₁))
≣< ((Act X₁) π ((Act X₁) [(c , b)] ((Act X₁) [(b , a₁)] x₁))) and πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((Symm (eq≈ₐ X₁)) ((p₁p₂↠ X₁) π [(c , b)] {(Act X₁) [(b , a₁)] x₁})) >
(((Act X₁) π ((Act X₁) [(c , b)] ((Act X₁) [(b , a₁)] x₁)))
≣< ((Act X₁) π ((Act X₁) ([(b , a₁)] ++ [(c , b)]) x₁)) and πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((res X₁) (λ {w} → P≡≈ π {w}) ((p₁p₂↠ X₁) [(c , b)] [(b , a₁)] {x₁})) >
(((Act X₁) π ((Act X₁) ([(b , a₁)] ++ [(c , b)]) x₁))
≣< ((Act X₁) π ((Act X₁) ([(b , a₁)] ++ [(c , b)]) ((Act X₁) [(c , b)] x₁))) and πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((res X₁) (λ {w} → P≡≈ π {w}) ((res X₁) (λ {w} → P≡≈ ([(b , a₁)] ++ [(c , b)]) {w}) ((Symm (eq≈ₐ X₁)) ((suppAx X₁) x₁ c b c∉x₁ b∉x₁)))) >
(((Act X₁) π ((Act X₁) ([(b , a₁)] ++ [(c , b)]) ((Act X₁) [(c , b)] x₁)))
≣< ((Act X₁) π ((Act X₁) ([(c , b)] ++ ([(b , a₁)] ++ [(c , b)])) x₁)) and πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((res X₁) (λ {w} → P≡≈ π {w}) ((p₁p₂↠ X₁) ([(b , a₁)] ++ [(c , b)]) [(c , b)] {x₁})) >
(((Act X₁) π ((Act X₁) ([(c , b)] ++ ([(b , a₁)] ++ [(c , b)])) x₁))
≣< πca₁x₁ and πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((res X₁) (λ {w} → P≡≈ π {w}) ((Symm (eq≈ₐ X₁)) ((res X₁) (λ {w} → ac≈ab+bc+ab c b a₁ a₁≠c a₁≠b {w}) (≈≡ (eq≈ₐ X₁) {x₁}{x₁} refl)))) >
(πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) ▴))))))) in
let prf₁₂ = ((Act X₁) [(c , b')] b'πa₁πx₁)
≣< ((Act X₁) ([(b' , πa₁)] ++ [(c , b')]) πx₁) and πca₁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 πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((Symm (eq≈ₐ X₁)) ((res X₁) (λ {w} → P≡≈ ([(b' , πa₁)] ++ [(c , b')]) {w}) ((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 πca₁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 πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((Symm (eq≈ₐ X₁)) ((res X₁) (λ {w} → ac≈ab+bc+ab c b' πa₁ πa₁≠c πa₁≠b' {w}) (≈≡ (eq≈ₐ X₁) {πx₁}{πx₁} refl))) >
(((Act X₁) [(c , πa₁)] πx₁)
≣< ((Act X₁) (π ++ [(c , πa₁)]) x₁) and πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((p₁p₂↠ X₁) [(c , πa₁)] π {x₁}) >
(((Act X₁) (π ++ [(c , πa₁)]) x₁)
≣< ((Act X₁) ([(c , a₁)] ++ π) x₁) and πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((res X₁) (λ {w} → bπaπ≈πab π c a₁ c∉π) (≈≡ (eq≈ₐ X₁) {x₁}{x₁} refl)) >
(((Act X₁) ([(c , a₁)] ++ π) x₁)
≣< πca₁x₁ and πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) on
((Symm (eq≈ₐ X₁)) ((p₁p₂↠ X₁) π [(c , a₁)] {x₁})) >
(πca₁x₁ by (≈ₐ X₁) as (eq≈ₐ X₁) ▴))))))) in
let prf₁ = (Trans (eq≈ₐ X₁)) prf₁₁ ((Symm (eq≈ₐ X₁)) prf₁₂) in
let prf₂₁ = ((Act X₂) [(c , πb)] πba₂x₂)
≣< ((Act X₂) (π ++ [(c , πb)]) ((Act X₂) [(b , a₂)] x₂)) and πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((p₁p₂↠ X₂) [(c , πb)] π {(Act X₂) [(b , a₂)] x₂}) >
(((Act X₂) (π ++ [(c , πb)]) ((Act X₂) [(b , a₂)] x₂))
≣< ((Act X₂) ([(c , b)] ++ π) ((Act X₂) [(b , a₂)] x₂)) and πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((res X₂) (λ {w} → bπaπ≈πab π c b c∉π {w}) (≈≡ (eq≈ₐ X₂) {(Act X₂) [(b , a₂)] x₂} {(Act X₂) [(b , a₂)] x₂} refl)) >
(((Act X₂) ([(c , b)] ++ π) ((Act X₂) [(b , a₂)] x₂))
≣< ((Act X₂) π ((Act X₂) [(c , b)] ((Act X₂) [(b , a₂)] x₂))) and πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((Symm (eq≈ₐ X₂)) ((p₁p₂↠ X₂) π [(c , b)] {(Act X₂) [(b , a₂)] x₂})) >
(((Act X₂) π ((Act X₂) [(c , b)] ((Act X₂) [(b , a₂)] x₂)))
≣< ((Act X₂) π ((Act X₂) ([(b , a₂)] ++ [(c , b)]) x₂)) and πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((res X₂) (λ {w} → P≡≈ π {w}) ((p₁p₂↠ X₂) [(c , b)] [(b , a₂)] {x₂})) >
(((Act X₂) π ((Act X₂) ([(b , a₂)] ++ [(c , b)]) x₂))
≣< ((Act X₂) π ((Act X₂) ([(b , a₂)] ++ [(c , b)]) ((Act X₂) [(c , b)] x₂))) and πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((res X₂) (λ {w} → P≡≈ π {w}) ((res X₂) (λ {w} → P≡≈ ([(b , a₂)] ++ [(c , b)]) {w}) ((Symm (eq≈ₐ X₂)) ((suppAx X₂) x₂ c b c∉x₂ b∉x₂)))) >
(((Act X₂) π ((Act X₂) ([(b , a₂)] ++ [(c , b)]) ((Act X₂) [(c , b)] x₂)))
≣< ((Act X₂) π ((Act X₂) ([(c , b)] ++ ([(b , a₂)] ++ [(c , b)])) x₂)) and πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((res X₂) (λ {w} → P≡≈ π {w}) ((p₁p₂↠ X₂) ([(b , a₂)] ++ [(c , b)]) [(c , b)] {x₂})) >
(((Act X₂) π ((Act X₂) ([(c , b)] ++ ([(b , a₂)] ++ [(c , b)])) x₂))
≣< πca₂x₂ and πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((res X₂) (λ {w} → P≡≈ π {w}) ((Symm (eq≈ₐ X₂)) ((res X₂) (λ {w} → ac≈ab+bc+ab c b a₂ a₂≠c a₂≠b {w}) (≈≡ (eq≈ₐ X₂) {x₂}{x₂} refl)))) >
(πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) ▴))))))) in
let prf₂₂ = ((Act X₂) [(c , b')] b'πa₂πx₂)
≣< ((Act X₂) ([(b' , πa₂)] ++ [(c , b')]) πx₂) and πca₂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 πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((Symm (eq≈ₐ X₂)) ((res X₂) (λ {w} → P≡≈ ([(b' , πa₂)] ++ [(c , b')]) {w}) ((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 πca₂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 πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((Symm (eq≈ₐ X₂)) ((res X₂) (λ {w} → ac≈ab+bc+ab c b' πa₂ πa₂≠c πa₂≠b' {w}) (≈≡ (eq≈ₐ X₂) {πx₂}{πx₂} refl))) >
(((Act X₂) [(c , πa₂)] πx₂)
≣< ((Act X₂) (π ++ [(c , πa₂)]) x₂) and πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((p₁p₂↠ X₂) [(c , πa₂)] π {x₂}) >
(((Act X₂) (π ++ [(c , πa₂)]) x₂)
≣< ((Act X₂) ([(c , a₂)] ++ π) x₂) and πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((res X₂) (λ {w} → bπaπ≈πab π c a₂ c∉π) (≈≡ (eq≈ₐ X₂) {x₂}{x₂} refl)) >
(((Act X₂) ([(c , a₂)] ++ π) x₂)
≣< πca₂x₂ and πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) on
((Symm (eq≈ₐ X₂)) ((p₁p₂↠ X₂) π [(c , a₂)] {x₂})) >
(πca₂x₂ by (≈ₐ X₂) as (eq≈ₐ X₂) ▴))))))) in
let prf₂ = (Trans (eq≈ₐ X₂)) prf₂₁ ((Symm (eq≈ₐ X₂)) prf₂₂) in NName c c∉t₁ c∉t₂ (prf₁ , prf₂)
}
; idisl = λ ax₁x₂ → let (a , (x₁ , x₂)) = ax₁x₂ in let xₛ = (some_supp X₁) x₁ ++ (some_supp X₂) x₂ in let csup = (a :: (a :: xₛ)) in
let b = outside csup in let b∉x₁₂ = des∉ (des∉ (outside∉ csup)) in let b#x₁₂ = ∉⇒# ([A] (Prod X₁ X₂)) ax₁x₂ b∉x₁₂ in
let ax≈ax = (Symm (eq≈ₐ ([A] (Prod X₁ X₂)))) (ax≈a'a'ax {X = (Prod X₁ X₂)} b#x₁₂) in ax≈ax
; idisr = λ a₁x₁a₂x₂ → let ((a₁ , x₁) , (a₂ , x₂)) = a₁x₁a₂x₂ in let x₁ₛ = (some_supp X₁) x₁ in let x₂ₛ = (some_supp X₂) x₂ in let xₛ = a₁ :: (a₂ :: (x₁ₛ ++ x₂ₛ)) in
let b = outside xₛ in let b∉x₁₂ = des∉ (des∉ (outside∉ xₛ)) in let b∉x₁ = ∉⊆₁ {x₁ₛ}{x₂ₛ} b b∉x₁₂ in let b∉x₂ = ∉⊆₂ {x₁ₛ}{x₂ₛ} b b∉x₁₂ in
let b#x₁ = ∉⇒# ([A] X₁) (a₁ , x₁) b∉x₁ in let b#x₂ = ∉⇒# ([A] X₂) (a₂ , x₂) b∉x₂ in let x₁≈x₁ = (Symm (eq≈ₐ ([A] X₁))) (ax≈a'a'ax {X = X₁} b#x₁) in
let x₂≈x₂ = (Symm (eq≈ₐ ([A] X₂))) (ax≈a'a'ax {X = X₂} b#x₂) in (x₁≈x₁ , x₂≈x₂)
}
----------------------------------------------------------------------------------------------------------------------------------
--([A] X) * A ≅ A × X
----------------------------------------------------------------------------------------------------------------------------------
*[]× : (X : Nominal) → Iso {NomCat} (([A] X) *A) (Prod NominalAtom X)
*[]× X = record { liso = record { ufun = λ axa → let a' = (Aelem axa) in let ax = (Xelem axa) in let a = proj₁ ax in let x = proj₂ ax in (a' , ((Act X) [(a' , a)] x))
; eqi≈ = λ {a'ax₁}{a'ax₂} a'x₁≈a'x₂ → let a₁≡a₂ = (proj₂ a'x₁≈a'x₂) in let x₁≈x₂ = (proj₁ a'x₁≈a'x₂) in let a'#ax₁ = (freshCon a'ax₁) in
let a'#ax₂ = (freshCon a'ax₂) in let pax₁ = ax≈a'a'ax {X = X} a'#ax₁ in let pax₂ = ax≈a'a'ax {X = X} a'#ax₂ in
let pax₁x₂ = (Trans (eq≈ₐ ([A] X))) ((Symm (eq≈ₐ ([A] X))) pax₁) ((Trans (eq≈ₐ ([A] X))) x₁≈x₂ pax₂) in
let px₁x₂ = ax₁≈ax₂ {X = X} a₁≡a₂ pax₁x₂ in (a₁≡a₂ , px₁x₂)
; equiv = λ π a'ax → let a' = (Aelem a'ax) in let ax = (Xelem a'ax) in let a = proj₁ ax in let x = proj₂ ax in
let πa' = (PermAct π a') in let πa = (PermAct π a) in let πx = ((Act X) π x) in let πa'ax = ((Act X) [(πa' , πa)] πx) in
let πx≈πx = ((Act X) π ((Act X) [(a' , a)] x))
≣< ((Act X) ([(a' , a)] ++ π) x) and πa'ax by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) π [(a' , a)] {x}) >
(((Act X) ([(a' , a)] ++ π) x)
≣< ((Act X) (π ++ [(πa' , πa)]) x) and πa'ax by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (λ {w} → π+πab≈abπ π a' a {w}) (≈≡ (eq≈ₐ X) {x}{x} refl))) >
(((Act X) (π ++ [(πa' , πa)]) x)
≣< πa'ax and πa'ax by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((p₁p₂↠ X) [(πa' , πa)] π {x})) >
(πa'ax by (≈ₐ X) as (eq≈ₐ X) ▴))) in ((πa' ▪) , πx≈πx)
}
; riso = record { ufun = λ ax → let a = (proj₁ ax) in let x = (proj₂ ax) in let xₛ = (some_supp X) x in let b = outside xₛ in let b∉x = outside∉ xₛ in let b#x = ∉⇒# ([A] X) (a , x) b∉x in
let b#ax = ax≈a'a'ax {X = X} b#x in let bax = ((Act X) [(b , a)] x) in let abx = ((Act X) [(a , b)] x) in
let baab = ≈α X abx bax (PermAct [(a , b)] a) b (swapaba≡b a b) ((res X) (λ {w} → ab=ba a b {w}) (≈≡ (eq≈ₐ X) {x} {x} refl)) in
let a#ax = (Trans (eq≈ₐ ([A] X))) baab ((Symm (eq≈ₐ ([A] X))) b#ax) in SP (a , x) a (fresh b b∉x a#ax)
; eqi≈ = λ {ax₁}{ax₂} ax₁≈ax₂ → let a≡a = (proj₁ ax₁≈ax₂) in let x₁≈x₂ = (proj₂ ax₁≈ax₂) in let ax₁x₂ = ≈α X (proj₂ ax₁) (proj₂ ax₂) (proj₁ ax₁) (proj₁ ax₂) a≡a x₁≈x₂
in (ax₁x₂ , a≡a)
; equiv = λ π ax → let a = (proj₁ ax) in let x = (proj₂ ax) in let πa = (PermAct π a) in let πx = ((Act X) π x) in let πax≈πax = ≈α X πx πx πa πa refl (≈≡ (eq≈ₐ X) {πx}{πx} refl)
in (πax≈πax , (πa ▪))
}
; idisl = λ a'ax → let a' = (Aelem a'ax) in let ax = (Xelem a'ax) in let a = (proj₁ ax) in let x = (proj₂ ax) in let a'#ax = (freshCon a'ax) in
let aa'x = ((Symm (eq≈ₐ ([A] X))) (ax≈a'a'ax {X = X} a'#ax)) in (aa'x , (a' ▪))
; idisr = λ ax → let a = (proj₁ ax) in let x = (proj₂ ax) in
let aax≈x = ((Act X) [(a , a)] x)
≣< ((Act X) ι x) and x by (≈ₐ X) as (eq≈ₐ X) on ((res X) (λ {w} → aa≈ι a {w}) (≈≡ (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 ((a ▪) , aax≈x)
}
---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------