module Nomfs where
{-
This file gives a category theoretic treatment to nominal sets and
finitely supported functions. It shows that Nomfs is a cartesian closed
category
-}
open import Basics
open import Perms
open import PermProp
open import Nom
open import NomSet
open import CatDef
-------------------------------------------------------------------------------------------------------------------------
--An example of a finitely supported function
-------------------------------------------------------------------------------------------------------------------------
πA→A : (π : Perm) → Funfs NominalAtom NominalAtom
πA→A π = record { ffun = λ a → PermAct π a
; fsupp = flatten π
; fsuppAx = λ b c b∉π c∉π a →
(PermAct [(b , c)] (PermAct π (PermAct [(b , c)] a))) ≡< (p₁p₂↠ NominalAtom) [(b , c)] π {PermAct [(b , c)] a} >
((PermAct (π ++ [(b , c)]) (PermAct [(b , c)] a)) ≡< sym (ab∉pcom b c π b∉π c∉π {PermAct [(b , c)] a}) >
((PermAct ([(b , c)] ++ π) (PermAct [(b , c)] a)) ≡< sym ((p₁p₂↠ NominalAtom) π [(b , c)] {PermAct [(b , c)] a}) >
((PermAct π (PermAct [(b , c)] (PermAct [(b , c)] a))) ≡< cong (λ w → PermAct π w) ((p₁p₂↠ NominalAtom) [(b , c)] [(b , c)] {a}) >
((PermAct π (PermAct ([(b , c)] ++ [(b , c)]) a)) ≡< cong (λ w → PermAct π w) (bc+bc=ι b c {a}) >
((PermAct π (PermAct ι a)) ≡< cong (λ w → PermAct π w) ((ι↠ NominalAtom) {a}) >
((PermAct π a) ▪))))))
; feqi≈ = λ x₁≡x₂ → cong (λ w → PermAct π w) x₁≡x₂
}
-------------------------------------------------------------------------------------------------------------------------
--An equivariant function is a finitely supported function
-------------------------------------------------------------------------------------------------------------------------
Eq2fs : {X Y : Nominal} → Equivar X Y → Funfs X Y
Eq2fs {X}{Y} F = record { ffun = λ x → (ufun F) x
; fsupp = []
; fsuppAx = λ b c → λ b∉[] c∉[] → λ x →
let y₁ = (ufun F) ((Act X) [(b , c)] x) in let y = (ufun F) x in
let x≈x = ((Act Y) [(b , c)] y₁)
≣< ((Act Y) [(b , c)] ((Act Y) [(b , c)] y)) and y by (≈ₐ Y) as (eq≈ₐ Y) on
((Symm (eq≈ₐ Y)) ((res Y) (λ {w} → P≡≈ [(b , c)] {w}) ((equiv F) [(b , c)] x))) >
(((Act Y) [(b , c)] ((Act Y) [(b , c)] y))
≣< ((Act Y) ([(b , c)] ++ [(b , c)]) y) and y by (≈ₐ Y) as (eq≈ₐ Y) on
((p₁p₂↠ Y) [(b , c)] [(b , c)] {y}) >
(((Act Y) ([(b , c)] ++ [(b , c)]) y)
≣< ((Act Y) ι y) and y by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → bc+bc=ι b c {w}) (≈≡ (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) ▴)))) in x≈x
; feqi≈ = λ x₁≈x₂ → (eqi≈ F) x₁≈x₂
}
-------------------------------------------------------------------------------------------------------------------------------
--composition of finitely supported functions
-------------------------------------------------------------------------------------------------------------------------------
øfs : {X Y Z : Nominal} → (F : Funfs X Y) → (G : Funfs Y Z) → Funfs X Z
øfs {X}{Y}{Z} F G = record { ffun = (ffun G) ∘ (ffun F)
; fsupp = (fsupp F) ++ (fsupp G)
; fsuppAx = λ b c → λ b∉fg → λ c∉fg → λ x → let fs = (fsupp F) in let gs = (fsupp G) in
let b∉f = ∉⊆₁ {fs}{gs} b b∉fg in let c∉f = ∉⊆₁ {fs}{gs} c c∉fg in
let b∉g = ∉⊆₂ {fs}{gs} b b∉fg in let c∉g = ∉⊆₂ {fs}{gs} c c∉fg in
let y₁ = (ffun F) ((Act X) [(b , c)] x) in let y₂ = (Act Y) [(b , c)] ((ffun F) x) in
let fbcx≈bcfx = (y₁ ≣< ((Act Y) ι y₁) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((Symm (eq≈ₐ Y)) ((ι↠ Y) {y₁})) >
(((Act Y) ι y₁)
≣< ((Act Y) ([(b , c)] ++ [(b , c)]) y₁) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((Symm (eq≈ₐ Y)) ((res Y) (λ {w} → bc+bc=ι b c {w}) (≈≡ (eq≈ₐ Y) {y₁}{y₁} refl))) >
(((Act Y) ([(b , c)] ++ [(b , c)]) y₁)
≣< ((Act Y) [(b , c)] ((Act Y) [(b , c)] y₁)) and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((Symm (eq≈ₐ Y)) ((p₁p₂↠ Y) [(b , c)] [(b , c)] {y₁})) >
(((Act Y) [(b , c)] ((Act Y) [(b , c)] y₁))
≣< y₂ and y₂ by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(b , c)] {w}) ((fsuppAx F) b c b∉f c∉f x)) >
(y₂ by (≈ₐ Y) as (eq≈ₐ Y) ▴)))))
in let bgfx = (Act Z [(b , c)] ((ffun G ∘ ffun F) (Act X [(b , c)] x))) in let gfx = ((ffun G ∘ ffun F) x)
in let x≈x = bgfx
≣< (Act Z [(b , c)] ((ffun G) y₂)) and gfx by (≈ₐ Z) as (eq≈ₐ Z) on
((res Z) (λ {w} → P≡≈ [(b , c)] {w}) ((feqi≈ G) fbcx≈bcfx)) >
((Act Z [(b , c)] ((ffun G) y₂))
≣< gfx and gfx by (≈ₐ Z) as (eq≈ₐ Z) on
((fsuppAx G) b c b∉g c∉g ((ffun F) x)) >
(gfx by (≈ₐ Z) as (eq≈ₐ Z) ▴)) in x≈x
; feqi≈ = λ {x₁ x₂} → λ x₁≈x₂ → (feqi≈ G) ((feqi≈ F) x₁≈x₂)
}
-------------------------------------------------------------------------------------------------------------------------------------------
--Nominal Sets and finitely supported functions form a category
------------------------------------------------------------------------------------------------------------------------------------------
NomCatfs : Cat
NomCatfs = record { Obj = Nominal
; _⇒_ = λ X Y → Funfs X Y
; _≈_ = λ {M N} → ≈fs {M}{N}
; isEq = λ {M N} → eq≈fs {M}{N}
; id = λ {N} → Eq2fs (ø1 N)
; _⊚_ = λ MN NO → øfs MN NO
; id1 = λ {M}{N} F → λ x → (Reflex (eq≈ₐ N)) {(ffun F) x}
; id2 = λ {M}{N} G → λ y → (Reflex (eq≈ₐ N)) {(ffun G) y}
; asso = λ {M}{N}{O}{P} f g h → λ x → let w = ((ffun h)((ffun g)((ffun f) x))) in (Reflex (eq≈ₐ P)){w}
; resp = λ {X Y Z} → λ {f g h i} → λ f≈g → λ h≈i → λ x → let y₁ = (ffun f) x in let y₂ = (ffun g) x in let z₁ = (ffun h) y₁ in let z₂ = (ffun i) y₂
in let z₁≈z₂ = z₁ ≣< ((ffun h) y₂) and z₂ by (≈ₐ Z) as (eq≈ₐ Z) on ((feqi≈ h) (f≈g x)) > (((ffun h) y₂) ≣< z₂ and z₂ by (≈ₐ Z) as (eq≈ₐ Z) on (h≈i y₂) > (z₂ by (≈ₐ Z) as (eq≈ₐ Z) ▴)) in z₁≈z₂
}
------------------------------------------------------------------------------------------------------------------------------------------
--This category is cartesian
-----------------------------------------------------------------------------------------------------------------------------------------
Z→ₛX×Y : (X Y Z : Nominal) → (F : Funfs Z X) → (G : Funfs Z Y) → Funfs Z (Prod X Y)
Z→ₛX×Y X Y Z F G = record { ffun = λ z → ((ffun F) z , (ffun G) z)
; fsupp = (fsupp F) ++ (fsupp G)
; fsuppAx = λ b c → λ b∉fg → λ c∉fg → λ x → let fₛ = (fsupp F) in let gₛ = (fsupp G) in
let b∉f = ∉⊆₁ {fₛ}{gₛ} b b∉fg in let c∉f = ∉⊆₁ {fₛ}{gₛ} c c∉fg in let b∉g = ∉⊆₂ {fₛ}{gₛ} b b∉fg in let c∉g = ∉⊆₂ {fₛ}{gₛ} c c∉fg in
(((fsuppAx F) b c b∉f c∉f x) , ((fsuppAx G) b c b∉g c∉g x))
; feqi≈ = λ {z₁ z₂} → λ z₁≈z₂ → ((feqi≈ F) z₁≈z₂ , (feqi≈ G) z₁≈z₂)
}
_Nomₓₛ_ : (X Y : Nominal) → Product {NomCatfs} X Y
X Nomₓₛ Y = record { X×Y = Prod X Y
; π₁ = Eq2fs (Fst X Y)
; π₂ = Eq2fs (Snd X Y)
; 〈_,_〉 = λ {Z} → λ F G → Z→ₛX×Y X Y Z F G
; c₁ = λ {Z} → λ {F} → λ {G} → λ x → (Reflex (eq≈ₐ X)) {(ffun F) x}
; c₂ = λ {Z} → λ {F} → λ {G} → λ y → (Reflex (eq≈ₐ Y)) {(ffun G) y}
; uni = λ {Z} → λ {F G H} → λ HF → λ HG → λ z → (((Symm (eq≈ₐ X)) (HF z)) , ((Symm (eq≈ₐ Y)) (HG z)))
}
TNomfs : Terminal NomCatfs
TNomfs = record { Ter = NomT
; A→T = λ N → Eq2fs (N→T N)
; uni = λ N → λ F → (λ x → refl)
}
CarNomfs : CarCat
CarNomfs = record { Ucat = NomCatfs
; UTer = TNomfs
; UProd = λ X Y → X Nomₓₛ Y
}
------------------------------------------------------------------------------------------------------------------------------------------
--This category is co-cartesian
-----------------------------------------------------------------------------------------------------------------------------------------
X+Y→ₛZ : (X Y Z : Nominal) → (F : Funfs X Z) → (G : Funfs Y Z) → Funfs (Sum X Y) Z
X+Y→ₛZ X Y Z F G = record { ffun = λ {(inl x) → (ffun F) x ;
(inr y) → (ffun G) y }
; fsupp = (fsupp F) ++ (fsupp G)
; fsuppAx = λ b c → λ b∉fg c∉fg → λ { (inl x) → (fsuppAx F) b c (∉⊆₁ {fsupp F}{fsupp G} b b∉fg) (∉⊆₁ {fsupp F}{fsupp G} c c∉fg) x ;
(inr y) → (fsuppAx G) b c (∉⊆₂ {fsupp F}{fsupp G} b b∉fg) (∉⊆₂ {fsupp F}{fsupp G} c c∉fg) y
}
; feqi≈ = λ { {(inl x₁)}{(inl x₂)} → λ x₁≈x₂ → (feqi≈ F) x₁≈x₂ ;
{(inr y₁)}{(inr y₂)} → λ y₁≈y₂ → (feqi≈ G) y₁≈y₂ ;
{(inl x₁)}{(inr y₂)} → λ () ;
{(inr y₁)}{(inl x₂)} → λ () }
}
_Nom₊ₛ_ : (X Y : Nominal) → Coproduct {NomCatfs} X Y
X Nom₊ₛ Y = record { X+Y = Sum X Y
; i₁ = Eq2fs (Fst' X Y)
; i₂ = Eq2fs (Snd' X Y)
; [[_,_]] = λ {Z} → λ F G → X+Y→ₛZ X Y Z F G
; c₁' = λ {Z} → λ {F} → λ {G} → λ x → (Reflex (eq≈ₐ Z)) {(ffun F) x}
; c₂' = λ {Z} → λ {F} → λ {G} → λ y → (Reflex (eq≈ₐ Z)) {(ffun G) y}
; uni' = λ {Z} → λ {F G H} → λ HF → λ HG → λ { (inl x) → (Symm (eq≈ₐ Z)) (HF x) ;
(inr y) → (Symm (eq≈ₐ Z)) (HG y) }
}
INomfs : Initial NomCatfs
INomfs = record { Ini = NomI
; I→A = λ N → Eq2fs (I→N N)
; uni = λ N → λ F → λ ()
}
CoCarNomfs : CoCarCat
CoCarNomfs = record { UCcat = NomCatfs
; UIni = INomfs
; UCoProd = λ X Y → X Nom₊ₛ Y
}
-------------------------------------------------------------------------------------------------------------------------------
--This category is cartesian closed
-------------------------------------------------------------------------------------------------------------------------------
currfs : (X Y Z : Nominal) → (F : Funfs (Prod Z X) Y) → Funfs Z (NomExp X Y)
currfs X Y Z F = record { ffun = λ z → record { ffun = λ x → (ffun F) ( z , x )
; fsupp = (fsupp F) ++ (some_supp Z) z
; fsuppAx = λ b c → λ b∉s → λ c∉s → λ x → let fₛ = (fsupp F) in let zₛ = (some_supp Z) z in let b∉f = ∉⊆₁ {fₛ}{zₛ} b b∉s in let b∉z = ∉⊆₂ {fₛ}{zₛ} b b∉s in
let c∉f = ∉⊆₁ {fₛ}{zₛ} c c∉s in let c∉z = ∉⊆₂ {fₛ}{zₛ} c c∉s in
let zx≈zx = (((Act Y) [ ( b , c ) ] ((ffun F) (z , ((Act X) [ ( b , c ) ] x))))
≣< ((Act Y) [ ( b , c ) ] ((ffun F) (((Act Z) [ ( b , c ) ] z) , ((Act X) [ ( b , c ) ] x)))) and (ffun F (z , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {x} → P≡≈ [ ( b , c ) ] {x}) ((feqi≈ F) (((Symm (eq≈ₐ Z))((suppAx Z) z b c b∉z c∉z)) ,
((Reflex (eq≈ₐ X)){(Act X) [ ( b , c ) ] x })))) >
((Act Y) [ ( b , c ) ] ((ffun F) (((Act Z) [ ( b , c ) ] z) , ((Act X) [ ( b , c ) ] x)))
≣< (ffun F (z , x)) and (ffun F (z , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
((fsuppAx F) b c b∉f c∉f (z , x)) >
((ffun F (z , x)) by (≈ₐ Y) as (eq≈ₐ Y) ▴))) in zx≈zx
; feqi≈ = λ {x₁}{x₂} → λ x₁≈x₂ → (feqi≈ F) ((Reflex (eq≈ₐ Z)) {z} , x₁≈x₂)
}
; fsupp = fsupp F
; fsuppAx = λ b c → λ b∉f c∉f → λ z → λ x → (((Act Y) [(b , c)] ((ffun F) (((Act Z) [(b , c)] z) , ((Act X) [(b , c)] x))))
≣< ((ffun F) (z , x)) and ((ffun F) (z , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
((fsuppAx F) b c b∉f c∉f (z , x)) >
(((ffun F) (z , x)) by (≈ₐ Y) as (eq≈ₐ Y) ▴))
; feqi≈ = λ {z₁}{z₂} → λ z₁≈z₂ → λ x → (feqi≈ F) ( z₁≈z₂ , (Reflex (eq≈ₐ X)) {x})
}
Expfs : (X Y : Nominal) → Exp{CarNomfs} X Y
Expfs X Y = record { Yˣ = NomExp X Y
; app = Eq2fs (appN X Y)
; curr = λ Z → λ F → currfs X Y Z F
; comm = λ Z → λ F → λ zx → (Reflex (eq≈ₐ Y)) {(ffun F) ((proj₁ zx) , (proj₂ zx))}
; univ = λ Z → λ F → λ H → λ FC → λ z → λ x → (Symm (eq≈ₐ Y)) (FC (z , x))
}
NomfsCCC : CCC
NomfsCCC = record { CarC = CarNomfs
; exp = λ X Y → Expfs X Y
}
-------------------------------------------------------------------------------------------------------------------