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 {  = 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
                                  }

-------------------------------------------------------------------------------------------------------------------