module Nom where

{-
This file provides a category theoretic treatment to nominal sets and
equivariant functions. It shows that Nom is a topos.
-}

open import Basics
open import Atoms
open import Perms
open import CatDef
open import PermProp


--------------------------------------------------------------------------------------------------
--Definition Nominal Set
--------------------------------------------------------------------------------------------------

record Nominal : Set₁ where
  field 
    Aₛ : Set
    ≈ₐ : Rel Aₛ
    eq≈ₐ : isEquivalence Aₛ ≈ₐ
    Act : Perm  Aₛ  Aₛ
    res : Act Preserves₂ pEquiv  ≈ₐ  ≈ₐ
    p₁p₂↠ : p₁p₂Act {Perm}{Aₛ}{_++_}{≈ₐ}{Act}
    ι↠ : ιAct {Perm}{Aₛ}{≈ₐ}{Act} ι

    some_supp : Aₛ  List Atom
    suppAx : (a : Aₛ)  (b c : Atom)  (b  some_supp a)  (c  some_supp a)  ≈ₐ (Act [ (b , c) ] a)  a

open Nominal public

--------------------------------------------------------------------------------------------------------
--Definition Equivariant functions
--------------------------------------------------------------------------------------------------------

record Equivar (X Y : Nominal) : Set where
   field 
      ufun :  Aₛ X  Aₛ Y
      eqi≈ : ufun Preserves (≈ₐ X)  (≈ₐ Y)
      equiv : (p : Perm)  (x : Aₛ X)  (≈ₐ Y) ((Act Y) p (ufun x)) (ufun ((Act X) p x)) 

open Equivar public

--------------------------------------------------------------------------------------------------------
--Definition finitely supported functions
--------------------------------------------------------------------------------------------------------

record Funfs (X Y : Nominal) : Set where
   field 
      ffun :  Aₛ X  Aₛ Y
      fsupp : List Atom
      fsuppAx : (b c : Atom)  (b  fsupp)  (c  fsupp)  (∀ (x : (Aₛ X))  (≈ₐ Y) ((Act Y) [ ( b , c ) ] (ffun ((Act X) [ ( b , c ) ] x))) (ffun x)) 
      feqi≈ : ffun Preserves (≈ₐ X)  (≈ₐ Y)
      
open Funfs public

fsch : {a b : Atom} (X Y : Nominal)  (F : Funfs X Y)  (x : Aₛ X)  a  (fsupp F)  b  (fsupp F)  (≈ₐ Y) ((Act Y) [(a , b)] ((ffun F) x)) ((ffun F) ((Act X) [(a , b)] x)) 
fsch {a}{b} X Y F x a∉f b∉f = let abfx = ((Act Y) [(a , b)] ((ffun F) x)) in let fabx = ((ffun F) ((Act X) [(a , b)] x)) in
                                       let final = fabx 
                                                             ≣< ((Act Y) ι fabx) and abfx by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                           ((Symm (eq≈ₐ Y)) ((ι↠ Y) {fabx})) >
                                                       (((Act Y) ι fabx) 
                                                             ≣< ((Act Y) ([(a , b)] ++ [(a , b)]) fabx) and abfx by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                           ((Symm (eq≈ₐ Y)) ((res Y)  {w}  bc+bc=ι a b {w}) (≈≡ (eq≈ₐ Y) {fabx}{fabx} refl))) >
                                                       (((Act Y) ([(a , b)] ++ [(a , b)]) fabx)
                                                             ≣< ((Act Y) [(a , b)] ((Act Y) [(a , b)] fabx)) and abfx by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                   ((Symm (eq≈ₐ Y)) ((p₁p₂↠ Y) [(a , b)] [(a , b)] {fabx})) >
                                                       (((Act Y) [(a , b)] ((Act Y) [(a , b)] fabx))
                                                             ≣< abfx and abfx by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                  ((res Y)  {w}  P≡≈ [(a , b)] {w}) ((fsuppAx F) a b a∉f b∉f x)) >
                                                       (abfx by (≈ₐ Y) as (eq≈ₐ Y) )))) in (Symm (eq≈ₐ Y)) final


-------------------------------------------------------------------------------------------------------------------
--equivalence relation on finitely supported functions
------------------------------------------------------------------------------------------------------------------

≈fs : {X Y : Nominal}  (Rel (Funfs X Y))
≈fs {X} {Y} = λ F G  (∀ x  (≈ₐ Y) ((ffun F) x) ((ffun G) x))


eq≈fs : {X Y : Nominal}  isEquivalence (Funfs X Y) (≈fs {X} {Y})
eq≈fs {X}{Y} = record { Reflex = λ {F}  λ x  (Reflex (eq≈ₐ Y)) {(ffun F) x}
                                       ; Symm = λ {F G}  λ F≈G  λ x  (Symm (eq≈ₐ Y)) (F≈G x)
                                       ; Trans = λ {F G H}  λ F≈G  λ G≈H  λ x  (Trans (eq≈ₐ Y)) (F≈G x) (G≈H x)  
                                       }


---------------------------------------------------------------------------------------------------------------------------
--Examples of Nominal Sets
---------------------------------------------------------------------------------------------------------------------------

----------------------------------------------------------------------------------------------------------------------------
--Atom is a Nominal Set
----------------------------------------------------------------------------------------------------------------------------

bc∉suppa : (a b c : Atom)  b  (supp a)  c  (supp a)  swap (b , c) a  a
bc∉suppa a b c (a∉as a∉[] a≠b) (a∉as a∉[] a≠c) = swapabc≡c b c a a≠b a≠c 

NominalAtom : Nominal
NominalAtom = record { Aₛ = Atom
                                       ; ≈ₐ = _≡_
                                       ; eq≈ₐ = aEquiv≡ Atom
                                       ; Act = PermAct
                                       ; res = λ {π₁ π₂ a₁ a₂}  λ π₁≈π₂  λ a₁≡a₂  (PermAct π₁ a₁ ≡< cong  w  PermAct π₁ w) a₁≡a₂ > (PermAct π₁ a₂ ≡< π₁≈π₂ {a₂} > (PermAct π₂ a₂)  ))
                                       ; p₁p₂↠ = λ p₁ p₂   {x}  sym (p₁++p₂≡p₂p₁ {x} p₂ p₁))
                                       ; ι↠ = λ {x}  refl

                                       ; some_supp = supp
                                       ; suppAx = λ a   b c   b≠a c≠a  bc∉suppa a b c b≠a c≠a))
                                       }

-------------------------------------------------------------------------------------------------------------------------
--Boolean is a discrete Nominal Set
-------------------------------------------------------------------------------------------------------------------------

𝔹Nom : Nominal
𝔹Nom = record { Aₛ = 𝔹
                           ; ≈ₐ = _≡_
                           ; eq≈ₐ = aEquiv≡ 𝔹
                           ; Act = λ π  λ b  b
                          ; res = λ π₁≈π₂  λ b≡b  b≡b
                          ; p₁p₂↠ = λ p₁ p₂  λ {b}  (Reflex (aEquiv≡ 𝔹)) {b}
                          ; ι↠ = λ {b}  (Reflex (aEquiv≡ 𝔹)) {b}
                          ; some_supp = λ b  []
                          ; suppAx = λ b  λ _ _ _ _  (Reflex (aEquiv≡ 𝔹)) {b}
                          }                          


------------------------------------------------------------------------------------------------------------------------------
                                --NOMINAL SETS & EQUIVARIANT FUNCTIONS CATEGORY
------------------------------------------------------------------------------------------------------------------------------

-----------------------------------------------------------------------------------------------------------------------
--equivalence relation on equivariant functions
-----------------------------------------------------------------------------------------------------------------------

≈̬ : {X Y : Nominal}  Rel (Equivar X Y)
≈̬ {X}{Y} = λ F G  (∀ x  (≈ₐ Y) ((ufun F) x) ((ufun G) x))

vEq :  {X Y}  isEquivalence (Equivar X Y) (≈̬ {X}{Y})
vEq {X}{Y} = record { Reflex = λ {F}   x  (Reflex (eq≈ₐ Y)) {(ufun F) x})
                                   ; Symm = λ {F G}  λ F≈G   x  (Symm (eq≈ₐ Y)) (F≈G x))
                                   ; Trans = λ {F G H}  λ F≈G  λ G≈H   x  (Trans (eq≈ₐ Y)) (F≈G x) (G≈H x))
                                   }

----------------------------------------------------------------------------------------------------------------
--composition of equivariant functions
----------------------------------------------------------------------------------------------------------------

ø : {X Y Z : Nominal}  (F : Equivar X Y)  (G : Equivar Y Z)  Equivar X Z
ø {X}{Y}{Z} F G = record { ufun = (ufun G)  (ufun F)
                        ; eqi≈ = λ {x₁ x₂}  λ x₁≈x₂  (eqi≈ G) ((eqi≈ F) x₁≈x₂)  
                        ; equiv = λ p x  let pgfx =  (Act Z) p (((ufun G)  (ufun F)) x) in 
                                                   let x≈x =  ((((ufun G)  (ufun F)) ((Act X) p x)) 
                                                                                                 ≣< ((ufun G) ((Act Y) p ((ufun F) x))) and pgfx by (≈ₐ Z) as (eq≈ₐ Z) on ((eqi≈ G) ((Symm (eq≈ₐ Y)) ( (equiv F) p x ) )) > 
                                                                      (((ufun G) ((Act Y) p ((ufun F) x))) 
                                                                                                 ≣< pgfx and pgfx by (≈ₐ Z) as (eq≈ₐ Z) on ((Symm (eq≈ₐ Z)) ((equiv G) p ((ufun F) x))) > 
                                                                      (pgfx by (≈ₐ Z) as (eq≈ₐ Z) ))) in (Symm (eq≈ₐ Z)) x≈x 
                       }

----------------------------------------------------------------------------------------------------------------
--identity equivariant function
----------------------------------------------------------------------------------------------------------------

ø1 : (X : Nominal)  Equivar X X
ø1 X = record { ufun = λ x  x
                        ; eqi≈ = λ x₁≈x₂  x₁≈x₂
                        ; equiv = λ p x  (Reflex (eq≈ₐ X)) {(Act X) p x} 
                        }

----------------------------------------------------------------------------------------------------------------
--identity axioms
----------------------------------------------------------------------------------------------------------------

idl : {X Y : Nominal}  (F : Equivar X Y)  ≈̬ (ø (ø1 X) F) F
idl {X}{Y} F = λ x  (Reflex (eq≈ₐ Y)) {(ufun F) x}

idr : {X Y : Nominal}  (G : Equivar X Y)  ≈̬ (ø G (ø1 Y)) G
idr {X}{Y} G = λ x  (Reflex (eq≈ₐ Y)) {(ufun G) x}

----------------------------------------------------------------------------------------------------------------
--associativity axiom
----------------------------------------------------------------------------------------------------------------

assoEq : {X Y Z W : Nominal}  (F : Equivar X Y)  (G : Equivar Y Z)   (H : Equivar Z W)  ≈̬ (ø (ø F G) H) (ø F (ø G H))
assoEq {X}{Y}{Z}{W} F G H = λ x  (Reflex (eq≈ₐ W)) {(((ufun H)  (ufun G))  (ufun F)) x}

-------------------------------------------------------------------------------------------------------------------
--Nominal Sets and Equivariant functions category
-------------------------------------------------------------------------------------------------------------------

NomCat : Cat 
NomCat = record { Obj = Nominal
                               ; _⇒_ = λ X Y  Equivar X Y
                               ; _≈_ = λ {M N}  ≈̬ {M}{N}
                               ; isEq = λ {M N}  vEq {M}{N}
                               ; id = λ {N}  ø1 N
                               ; _⊚_ = λ MN NO  ø MN NO
                               ; id1 = λ F  idl F
                               ; id2 = λ G  idr G
                               ; asso = λ f g h  assoEq f g h
                               ; resp = λ {X Y Z}  λ {f g h i}  λ f≈g  λ h≈i   x  let igx = ((ufun i)  (ufun g)) x in 
                                                                                                                          let hf≈ig = ( ((ufun h)  (ufun f)) x  
                                                                                                                                                         ≣< (((ufun h)  (ufun g)) x) and igx by (≈ₐ Z) as (eq≈ₐ Z) on ((eqi≈ h) (f≈g x)) > 
                                                                                                                                           ( ((ufun h)  (ufun g)) x 
                                                                                                                                                         ≣< igx and igx by (≈ₐ Z) as (eq≈ₐ Z) on (h≈i ((ufun g) x)) > 
                                                                                                                                           ( igx by (≈ₐ Z) as (eq≈ₐ Z)  ))) in hf≈ig)

                              }

-----------------------------------------------------------------------------------------------------------------------
--Terminal Object
-----------------------------------------------------------------------------------------------------------------------

NomT : Nominal
NomT = record { Aₛ = 
                          ; ≈ₐ = _≡_
                          ; eq≈ₐ = record { Reflex = λ {i}  refl
                                                     ; Symm = λ {i j}  λ i≈j  sym (i≈j)
                                                     ; Trans = λ {i j k}  λ i≈j  λ j≈k  i ≡< i≈j > j≈k
                                                     }
                          ; Act = λ p a  One
                          ; res = λ {π₁ π₂ a₁ a₂}  λ π₁≈π₂  λ a₁≡a₂  refl
                          ; p₁p₂↠ = λ p₁ p₂   {a}  refl)
                          ; ι↠ = λ {a}  refl
                          ; some_supp = λ a  []
                          ; suppAx = λ a  λ b c  λ b∉a c∉a  refl
                          }

-----------------------------------------------------------------------------------------------------------------------
--Unique morphism to terminal object
-----------------------------------------------------------------------------------------------------------------------

N→T : (N : Nominal)  (Equivar N NomT)
N→T N = record { ufun = λ n  One
                           ; eqi≈ = λ {n₁ n₂}  λ n₁≈n₂  refl
                           ; equiv = λ p  λ n  refl
                           }

TNominal : Terminal NomCat
TNominal = record { Ter = NomT
                                ; A→T = λ N  N→T N
                                ; uni = λ N  λ F   x  refl)
                                }

--------------------------------------------------------------------------------------------------------------------------
--Initial object
-------------------------------------------------------------------------------------------------------------------------

NomI : Nominal
NomI = record { Aₛ = 
                          ; ≈ₐ = _≡_
                          ; eq≈ₐ = record { Reflex = λ {i}  refl
                                                     ; Symm = λ {i j}  λ i≈j  sym (i≈j)
                                                     ; Trans = λ {i j k}  λ i≈j  λ j≈k  i ≡< i≈j > j≈k 
                                                     }
                          ; Act = λ p  λ a  a
                          ; res = λ {π₁} {π₂}  λ { { () } }
                          ; p₁p₂↠ = λ p₁ p₂  refl
                          ; ι↠ = refl
                          ; some_supp = λ ()
                          ; suppAx = λ ()
                          }

-------------------------------------------------------------------------------------------------------------------
--Unique morphism from initial object
-------------------------------------------------------------------------------------------------------------------

I→N : (N : Nominal)  (Equivar NomI N)
I→N N = record { ufun = λ ()
                           ; eqi≈ = λ {i₁ i₂}  λ i₁≈i₂  ≈≡ (eq≈ₐ N) (cong  ()) i₁≈i₂)  
                           ; equiv = λ p  λ ()
                           }

INominal : Initial NomCat
INominal = record { Ini = NomI
                                ; I→A = λ N  I→N N
                                ; uni = λ N  λ F  λ ()
                                }

------------------------------------------------------------------------------------------------------------------------------------
                                                  --CARTESIAN CATEGORY
------------------------------------------------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------------------------------------
--Product
-----------------------------------------------------------------------------------------------------------------------

Prod : (X Y : Nominal)  Nominal
Prod X Y = record { Aₛ = (Aₛ X) × (Aₛ Y)
                              ; ≈ₐ = λ p₁ p₂  (((≈ₐ X) (proj₁ p₁) (proj₁ p₂)) × ((≈ₐ Y) (proj₂ p₁) (proj₂ p₂)))
                              ; eq≈ₐ = record { Reflex = λ {p₁}  ((Reflex (eq≈ₐ X)) {proj₁ p₁} , (Reflex (eq≈ₐ Y)) {proj₂ p₁})
                                                         ; Symm = λ {p₁ p₂}  λ p₁≈p₂  ((Symm (eq≈ₐ X)) (proj₁ p₁≈p₂) , (Symm (eq≈ₐ Y)) (proj₂ p₁≈p₂))
                                                         ; Trans = λ {p₁ p₂ p₃}  λ p₁≈p₂  λ p₂≈p₃  ((Trans (eq≈ₐ X)) (proj₁ p₁≈p₂) (proj₁ p₂≈p₃) , (Trans (eq≈ₐ Y)) (proj₂ p₁≈p₂) (proj₂ p₂≈p₃))
                                                         }
                              ; Act = λ π  λ p  ((Act X) π (proj₁ p) , (Act Y) π (proj₂ p))
                              ; res = λ {π₁ π₂ p₁ p₂}  λ π₁≈π₂  λ p₁≈p₂  ((res X) {π₁} {π₂} {proj₁ p₁} {proj₁ p₂} π₁≈π₂ (proj₁ p₁≈p₂) , (res Y) {π₁}{π₂}{proj₂ p₁}{proj₂ p₂} π₁≈π₂ (proj₂ p₁≈p₂))
                              ; p₁p₂↠ = λ π π'   {p}  (((p₁p₂↠ X) π π' {proj₁ p}) , ((p₁p₂↠ Y) π π' {proj₂ p})))
                              ; ι↠ = λ {p}  ((ι↠ X) {proj₁ p} , (ι↠ Y) {proj₂ p})
                              ; some_supp = λ p  ((some_supp X) (proj₁ p)) ++ ((some_supp Y) (proj₂ p))
                              ; suppAx = λ p  λ b c  λ b∉p  λ c∉p  ((suppAx X) (proj₁ p) b c (∉⊆₁ b b∉p) (∉⊆₁ c c∉p) , 
                                                (suppAx Y) (proj₂ p) b c (∉⊆₂ {(some_supp X) (proj₁ p)}{(some_supp Y) (proj₂ p)} b b∉p) (∉⊆₂ {(some_supp X) (proj₁ p)}{(some_supp Y) (proj₂ p)} c c∉p))  
                              }


-----------------------------------------------------------------------------------------------------------------------------
--Projection morphism
-----------------------------------------------------------------------------------------------------------------------------
                              
Fst : (X Y : Nominal)  Equivar (Prod X Y) X
Fst X Y = record { ufun = λ p  (proj₁ p)
                           ; eqi≈ = λ {p₁ p₂}  λ p₁≈p₂  (proj₁ p₁≈p₂)
                           ; equiv = λ π  λ p  (Reflex (eq≈ₐ X)) {(Act X) π (proj₁ p)}
                           }

Snd : (X Y : Nominal)  Equivar (Prod X Y) Y
Snd X Y = record { ufun = λ p  (proj₂ p)
                           ; eqi≈ = λ {p₁ p₂}  λ p₁≈p₂  (proj₂ p₁≈p₂)
                           ; equiv = λ π  λ p  (Reflex (eq≈ₐ Y)) {(Act Y) π (proj₂ p)}
                           }

-----------------------------------------------------------------------------------------------------------------------------
--Unique morphism
-----------------------------------------------------------------------------------------------------------------------------

Z→X×Y : (X Y Z : Nominal)  (F : Equivar Z X)  (G : Equivar Z Y)  Equivar Z (Prod X Y)
Z→X×Y X Y Z F G = record { ufun = λ z  ((ufun F) z , (ufun G) z)
                                            ;  eqi≈ = λ {z₁ z₂}  λ z₁≈z₂  ((eqi≈ F) z₁≈z₂ , (eqi≈ G) z₁≈z₂)
                                            ; equiv = λ π  λ z  ((equiv F) π z , (equiv G) π z)
                                            }

Com₁ : (X Y Z : Nominal)  (F : Equivar Z X)  (G : Equivar Z Y)  ≈̬ {Z}{X}(ø (Z→X×Y X Y Z F G) (Fst X Y)) F
Com₁ X Y Z F G = λ z  (Reflex (eq≈ₐ X)) {(ufun F) z}


Com₂ : (X Y Z : Nominal)  (F : Equivar Z X)  (G : Equivar Z Y)  ≈̬ {Z}{Y}(ø (Z→X×Y X Y Z F G) (Snd X Y)) G
Com₂ X Y Z F G = λ z  (isEquivalence.Reflex (eq≈ₐ Y)) {(ufun G) z}

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

_Nomₓ_ : (X Y : Nominal)  Product {NomCat} X Y
X Nomₓ Y = record { X×Y = Prod X Y
                                ; π₁ = Fst X Y
                                ; π₂ = Snd X Y
                                ; 〈_,_〉 = λ {Z}  λ F G  Z→X×Y X Y Z F G
                                ; c₁ = λ {Z}  λ {F}  λ {G}   Com₁ X Y Z F G
                                ; c₂ = λ {Z}  λ {F}  λ {G}   Com₂ X Y Z F G
                                ; uni = λ {Z}  λ {F G H}  λ HF  λ HG   z  ((Symm (eq≈ₐ X)) (HF z) , (Symm (eq≈ₐ Y)) (HG z)))
                                }

--------------------------------------------------------------------------------------------------------------------------------
--Cartesian category
--------------------------------------------------------------------------------------------------------------------------------

CarNom : CarCat
CarNom = record { Ucat = NomCat
                               ; UTer =  TNominal
                               ; UProd = λ X Y  X Nomₓ Y
                              }



-------------------------------------------------------------------------------------------------------------------------------------------------------
                                             --COCARTESIAN CATEGORY
-------------------------------------------------------------------------------------------------------------------------------------------------------

-------------------------------------------------------------------------------------------------------------------------------------
--Sum object
-----------------------------------------------------------------------------------------------------------------------------------

Sum : (X Y : Nominal)  Nominal
Sum X Y = record { Aₛ = (Aₛ X)  (Aₛ Y)
                              ; ≈ₐ = λ {(inl x₁) (inl x₂)  (≈ₐ X) x₁ x₂ ;
                                              (inr y₁) (inr y₂)  (≈ₐ Y) y₁ y₂ ;
                                              (inl x₁) (inr y₂)   ;
                                              (inr y₁) (inl x₂)   }
                              ; eq≈ₐ =  record { Reflex = λ { {inl x}  (Reflex (eq≈ₐ X)) {x} ;
                                                                               {inr y}  (Reflex (eq≈ₐ Y)) {y} }
                                                         ; Symm = λ { {(inl x₁)} {(inl x₂)}  λ x₁≈x₂  (Symm (eq≈ₐ X))  x₁≈x₂ ;
                                                                                {(inr y₁)} {(inr y₂)}  λ y₁≈y₂  (Symm (eq≈ₐ Y)) y₁≈y₂ ;
                                                                                {(inl x₁)} {(inr y₂)}  λ () ;
                                                                                {(inr y₁)} {(inl x₂)}  λ () }
                                                         ; Trans = λ { {(inl x₁)} {(inl x₂)} {(inl x₃)}  λ x₁≈x₂  λ x₂≈x₃  (Trans (eq≈ₐ X)) x₁≈x₂ x₂≈x₃ ;
                                                                              {(inr y₁)} {(inr y₂)} {(inr y₃)}  λ y₁≈y₂  λ y₂≈y₃  (Trans (eq≈ₐ Y)) y₁≈y₂ y₂≈y₃ ;
                                                                              {(inl x₁)} {(inl x₂)} {(inr y₃)}  λ x₁≈x₂  λ () ;
                                                                              {(inl x₁)} {(inr y₂)} {(inl x₃)}  λ () ;
                                                                              {(inl x₁)} {(inr y₂)} {(inr y₃)}  λ () ;
                                                                              {(inr y₁)} {(inl x₂)} {(inl x₃)}  λ () ;
                                                                              {(inr y₁)} {(inl x₂)} {(inr y₃)}  λ () ;
                                                                              {(inr y₁)} {(inr y₂)} {(inl x₃)}  λ y₁≈y₂  λ () } }
                              ; Act =  λ π  λ { (inl x)  inl ((Act X) π x) ;
                                                          (inr y)  inr ((Act Y) π y) }
                              ; res = λ {π₁}{π₂}  λ { {inl x₁} {inl x₂}  λ π₁≈π₂  λ x₁≈x₂  (res X) {π₁}{π₂}{x₁}{x₂} π₁≈π₂ x₁≈x₂ ;
                                                                     {inr y₁} {inr y₂}  λ π₁≈π₂  λ y₁≈y₂  (res Y) {π₁}{π₂}{y₁}{y₂} π₁≈π₂ y₁≈y₂ ;
                                                                     {inl x₁} {inr y₂}  λ π₁≈π₂  λ () ;
                                                                     {inr y₁} {inl x₂}  λ π₁≈π₂  λ () }
                              ; p₁p₂↠ = λ π π'  λ  { {inl x}  ((p₁p₂↠ X) π π' {x}) ;
                                                                  {inr y}  ((p₁p₂↠ Y) π π' {y}) }
                              ; ι↠ = λ { {inl x}  (ι↠ X) {x} ;
                                              {inr y}  (ι↠ Y) {y} }
                              ; some_supp = λ { (inl x)  (some_supp X) x ;
                                                             (inr y)  (some_supp Y) y }
                              ; suppAx = λ { (inl x)  λ b c  λ b∉x  λ c∉x  (suppAx X) x b c b∉x c∉x ; 
                                                      (inr y)  λ b c  λ b∉y  λ c∉y  (suppAx Y) y b c b∉y c∉y }  
                              }

-----------------------------------------------------------------------------------------------------------------------------
--injection morphisms
-----------------------------------------------------------------------------------------------------------------------------

Fst' : (X Y : Nominal)  Equivar X (Sum X Y) 
Fst' X Y = record { ufun = λ x  (inl x)
                           ; eqi≈ = λ {x₁ x₂}  λ x₁≈x₂  x₁≈x₂
                           ; equiv = λ π  λ x  (Reflex (eq≈ₐ (Sum X Y))) {inl ((Act X) π x)}
                           }

Snd' : (X Y : Nominal)  Equivar Y (Sum X Y)
Snd' X Y = record { ufun = λ y  (inr y)
                           ; eqi≈ = λ {y₁ y₂}  λ y₁≈y₂  y₁≈y₂ 
                           ; equiv = λ π  λ y  (Reflex (eq≈ₐ (Sum X Y))) {inr ((Act Y) π y)}
                           }

-------------------------------------------------------------------------------------------------------------------------
--unique morphism
------------------------------------------------------------------------------------------------------------------------

X+Y→Z : (X Y Z : Nominal)  (F : Equivar X Z)  (G : Equivar Y Z)  Equivar (Sum X Y) Z
X+Y→Z X Y Z F G = record { ufun = λ {(inl x)  (ufun F) x ;
                                                               (inr y)  (ufun G) y }
                                            ;  eqi≈ = λ { {(inl x₁)}{(inl x₂)}  λ x₁≈x₂  (eqi≈ F) x₁≈x₂ ;
                                                                {(inr y₁)}{(inr y₂)}  λ y₁≈y₂  (eqi≈ G) y₁≈y₂ ;
                                                                {(inl x₁)}{(inr y₂)}  λ () ;
                                                                {(inr y₁)}{(inl x₂)}  λ () }
                                            ; equiv = λ π  λ { (inl x)  (equiv F) π x ;
                                                                          (inr y)  (equiv G) π y }
                                            }


Com₁' : (X Y Z : Nominal)  (F : Equivar X Z)  (G : Equivar Y Z)  ≈̬ {X}{Z}(ø (Fst' X Y) (X+Y→Z X Y Z F G)) F
Com₁' X Y Z F G = λ x  (Reflex (eq≈ₐ Z)) {(ufun F) x}


Com₂' : (X Y Z : Nominal)  (F : Equivar X Z)  (G : Equivar Y Z)  ≈̬ {Y}{Z}(ø (Snd' X Y) (X+Y→Z X Y Z F G)) G
Com₂' X Y Z F G = λ y  (Reflex (eq≈ₐ Z)) {(ufun G) y}

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


_Nom₊_ : (X Y : Nominal)  Coproduct {NomCat} X Y
X Nom₊ Y = record { X+Y = Sum X Y
                                ; i₁ = Fst' X Y
                                ; i₂ = Snd' X Y
                                ; [[_,_]] = λ {Z}  λ F G  X+Y→Z X Y Z F G
                                ; c₁' = λ {Z}  λ {F}  λ {G}   Com₁' X Y Z F G
                                ; c₂' = λ {Z}  λ {F}  λ {G}   Com₂' X Y Z F G
                                ; uni' = λ {Z}  λ {F G H}  λ HF  λ HG  λ { (inl x)  (Symm (eq≈ₐ Z)) (HF x) ;
                                                                                                            (inr y)  (Symm (eq≈ₐ Z)) (HG y) }
                                }

------------------------------------------------------------------------------------------------------------------------
--Co-cartesian category
------------------------------------------------------------------------------------------------------------------------

CoCarNom : CoCarCat
CoCarNom = record { UCcat = NomCat
                                  ; UIni = INominal
                                  ; UCoProd = λ X Y  X Nom₊ Y
                                  }



-------------------------------------------------------------------------------------------------------------------------------
                                               --CARTESIAN CLOSED CATEGORY
-------------------------------------------------------------------------------------------------------------------------------

-------------------------------------------------------------------------------------------------------------------------------
                                               --EXPONENTIAL OBJECT
-------------------------------------------------------------------------------------------------------------------------------

----------------------------------------------------------------------------------------------------------------------------------
--action on finitely supported functions
----------------------------------------------------------------------------------------------------------------------------------

fAct : {X Y : Nominal}  Perm  (F : Funfs X Y)  (Funfs X Y)
fAct {X}{Y} π F = record { ffun = λ x  (Act Y) π ((ffun F) ((Act X) (invPerm π) x))
                                         ; fsupp = (fsupp F) ++ (flatten π)
                                         ; fsuppAx = λ b c  λ b∉s  λ c∉s   x  (Symm (eq≈ₐ Y))  
                                 ((Act Y) π ((ffun F) ((Act X) (invPerm π) x)) 
                                                                                                ≣< ((Act Y) π ((Act Y) [ ( b , c ) ] ((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x))))) 
                                                                                                and (((Act Y) [ ( b , c ) ] ((Act Y) π ((ffun F) ((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x))))))
                                                                                                by (≈ₐ Y) as (eq≈ₐ Y) on 
                                                                                                                                                                                            ((res Y) {π} {π}{(ffun F) ((Act X) (invPerm π) x)}{(Act Y) [ ( b , c ) ] 
                                                                                                                                                                                            ((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x)))}(P≡≈ π)
                                                                                                                                                                                            ((Symm (eq≈ₐ Y)) ((fsuppAx F) b c (∉⊆₁ {fsupp F}{flatten π} b b∉s) 
                                                                                                                                                                                            (∉⊆₁ {fsupp F}{flatten π} c c∉s) ((Act X) (invPerm π) x)))) >
           ((Act Y) π ((Act Y) [ ( b , c ) ] ((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x))))                                      
                                                                                               ≣< ((Act Y) ([ ( b , c ) ] ++ π)  ((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x)))) 
                                                                                               and (((Act Y) [ ( b , c ) ] ((Act Y) π ((ffun F) ((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x)))))) 
                                                                                               by (≈ₐ Y) as (eq≈ₐ Y) on 
                                                                                                                                                                                           ((p₁p₂↠ Y) π [ ( b , c ) ] {(ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x))}) >
           ((Act Y) ( [ ( b , c ) ] ++ π) ((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x)))                                          
                                                                                               ≣< ((Act Y) (π ++ [ ( b , c ) ])  ((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x)))) 
                                                                                               and (((Act Y) [ ( b , c ) ] ((Act Y) π ((ffun F) ((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x)))))) 
                                                                                               by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                                                                             (res Y) { [ ( b , c ) ] ++ π }{π ++  [ ( b , c ) ] }
                                                                                                                                                                                             {((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x)))}
                                                                                                                                                                                             {((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x)))}
                                                                                                                                                                                                  (ab∉pcom b c π (∉⊆₂ {fsupp F}{flatten π} b b∉s) 
                                                                                                                                                                                                  (∉⊆₂ {fsupp F}{flatten π} c c∉s)) (≈≡ (eq≈ₐ Y) 
                                                                                                                                                                                              {((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x)))}
                                                                                                                                                                                              {((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x)))} refl) >
         ((Act Y) (π ++ [ ( b , c ) ]) ((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x)))                                              
                                                                                              ≣< ((Act Y) [ ( b , c ) ] ((Act Y) π ((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x)))))
                                                                                               and (((Act Y) [ ( b , c ) ] ((Act Y) π ((ffun F) ((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x)))))) 
                                                                                               by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                                                                        (Symm (eq≈ₐ Y)) ((p₁p₂↠ Y) [ ( b , c ) ] π 
                                                                                                                                                                                        {(ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x))}) >
         ((Act Y) [ ( b , c ) ] ((Act Y) π ((ffun F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x))))                                         
                                                                                             ≣< 
                                                         (((Act Y) [ ( b , c ) ] ((Act Y) π ((ffun F) ((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x))))))
                                                         and (((Act Y) [ ( b , c ) ] ((Act Y) π ((ffun F) ((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x)))))) 
                                                         by (≈ₐ Y) as (eq≈ₐ Y) on                                
                                                         ((res Y)  {x}  P≡≈ [ ( b , c ) ] {x}) ((res Y) (P≡≈ π) ((feqi≈ F) ((Act X) [ ( b , c ) ] ((Act X) (invPerm π) x)                               
                                                                                                                                                   ≣<  ((Act X) ((invPerm π) ++ [ ( b , c ) ] ) x)
                                                                                                                                                   and ((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x))
                                                                                                                                                   by (≈ₐ X) as (eq≈ₐ X) on
                                                                                                                                                                      (p₁p₂↠ X) [ ( b , c) ] (invPerm π) {x} > 
                                                         ((Act X) ((invPerm π) ++ [ ( b , c ) ] ) x                                                                                                             
                                                                                                                                                   ≣< ((Act X) ([ ( b , c ) ] ++ (invPerm π)) x)
                                                                                                                                                   and ((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x))
                                                                                                                                                   by (≈ₐ X) as (eq≈ₐ X) on
                                                                                                                                                                       (res X) {(invPerm π) ++ [ ( b , c ) ]}
                                                                                                                                                                       {[ ( b , c ) ] ++ (invPerm π)}{x}{x}
                                                                                                                                                                       (++⁻¹ [ ( b , c ) ] π (ab∉pcom b c π (∉⊆₂ {fsupp F}{flatten π} b b∉s) 
                                                                                                                                                                       (∉⊆₂ {fsupp F}{flatten π} c c∉s))) (≈≡ (eq≈ₐ X) {x}{x} refl) >
                                                        ((Act X) ([ ( b , c ) ] ++ (invPerm π)) x                                                                                                               
                                                                                                                                                   ≣< ((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x)) 
                                                                                                                                                   and ((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x))
                                                                                                                                                   by (≈ₐ X) as (eq≈ₐ X) on
                                                                                                                                                                                                                                               (Symm (eq≈ₐ X)) ((p₁p₂↠ X) (invPerm π) 
                                                                                                                                                                                                                                               [ ( b , c ) ] {x}) >
                                                        (((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x) by (≈ₐ X) as (eq≈ₐ X) ))))))))                >
        (((Act Y) [ ( b , c ) ] ((Act Y) π ((ffun F) ((Act X) (invPerm π) ((Act X) [ ( b , c ) ] x))))) by (≈ₐ Y) as (eq≈ₐ Y) ))))))) 
 

                                        ; feqi≈ = λ {x₁ x₂}  λ x₁≈x₂  (res Y) (P≡≈ π) ((feqi≈ F) ((res X) (P≡≈ (invPerm π)) x₁≈x₂))
                                       } 


-----------------------------------------------------------------------------------------------------------------------------------------------------
--action preserves equivalence relation
-----------------------------------------------------------------------------------------------------------------------------------------------------


fActRes : (X Y : Nominal)  fAct Preserves₂ pEquiv  (≈fs {X} {Y})   (≈fs {X} {Y})
fActRes X Y = λ {π₁ π₂ F G}  λ π₁≈π₂  λ F≈G  λ x  (((Act Y) π₁ ((ffun F) ((Act X) (invPerm π₁) x))) 
                                                                                                    ≣<  ((Act Y) π₂ ((ffun F) ((Act X) (invPerm π₁) x)))
                                                                                                           and ((Act Y) π₂ ((ffun G) ((Act X) (invPerm π₂) x)))
                                                                                                           by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                           ((res Y) π₁≈π₂ (≈≡ (eq≈ₐ Y) {(ffun F) ((Act X) (invPerm π₁) x)}{(ffun F) ((Act X) (invPerm π₁) x)} refl)) >
                                                                                      (((Act Y) π₂ ((ffun F) ((Act X) (invPerm π₁) x)))
                                                                                                    ≣< ((Act Y) π₂ ((ffun G) ((Act X) (invPerm π₁) x)))
                                                                                                           and ((Act Y) π₂ ((ffun G) ((Act X) (invPerm π₂) x)))
                                                                                                           by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                       ((res Y) (P≡≈ π₂) (F≈G ((Act X) (invPerm π₁) x))) >
                                                                                      (((Act Y) π₂ ((ffun G) ((Act X) (invPerm π₁) x)))
                                                                                                    ≣< ((Act Y) π₂ ((ffun G) ((Act X) (invPerm π₂) x)))
                                                                                                           and ((Act Y) π₂ ((ffun G) ((Act X) (invPerm π₂) x)))
                                                                                                           by (≈ₐ Y) as (eq≈ₐ Y) on 
                                                                                                                              ((res Y) (P≡≈ π₂) ((feqi≈ G) ((res X) (p≈q⇒p⁻¹≈q⁻¹ π₁ π₂ π₁≈π₂) (≈≡ (eq≈ₐ X){x}{x} refl)))) >
                                                                                      (((Act Y) π₂ ((ffun G) ((Act X) (invPerm π₂) x))) by (≈ₐ Y) as (eq≈ₐ Y) )))) 
                                                                

-----------------------------------------------------------------------------------------------------------------------------------------
--associativity axiom
-----------------------------------------------------------------------------------------------------------------------------------------

fp₁p₂↠ : {X Y : Nominal}  p₁p₂Act {Perm}{Funfs X Y}{_++_}{≈fs {X}{Y}}{fAct {X}{Y}}
fp₁p₂↠ {X}{Y} = λ π₁ π₂   {F}    x  (((Act Y) π₁ ((Act Y) π₂ ((ffun F) ((Act X) (invPerm π₂) ((Act X) (invPerm π₁) x)))))
                                                                                 ≣< ((Act Y) (π₂ ++ π₁) ((ffun F) ((Act X) (invPerm π₂) ((Act X) (invPerm π₁) x))))
                                                                                       and ((Act Y) (π₂ ++ π₁) ((ffun F) ((Act X) (invPerm (π₂ ++ π₁)) x)))
                                                                                       by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                       ((p₁p₂↠ Y) π₁ π₂ {(ffun F) ((Act X) (invPerm π₂) ((Act X) (invPerm π₁) x))}) > 
                                                              (((Act Y) (π₂ ++ π₁) ((ffun F) ((Act X) (invPerm π₂) ((Act X) (invPerm π₁) x))))
                                                                                ≣< ((Act Y) (π₂ ++ π₁) ((ffun F) ((Act X) ((invPerm π₁) ++ (invPerm π₂)) x)))
                                                                                       and ((Act Y) (π₂ ++ π₁) ((ffun F) ((Act X) (invPerm (π₂ ++ π₁)) x)))
                                                                                       by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                       ((res Y) (P≡≈ (π₂ ++ π₁)) ((feqi≈ F) ((p₁p₂↠ X) (invPerm π₂) (invPerm π₁) {x}))) >
                                                              (((Act Y) (π₂ ++ π₁) ((ffun F) ((Act X) ((invPerm π₁) ++ (invPerm π₂)) x)))
                                                                                ≣< ((Act Y) (π₂ ++ π₁) ((ffun F) ((Act X) (invPerm (π₂ ++ π₁)) x)))
                                                                                       and ((Act Y) (π₂ ++ π₁) ((ffun F) ((Act X) (invPerm (π₂ ++ π₁)) x)))
                                                                                       by (≈ₐ Y) as (eq≈ₐ Y) on 
                                                                                                        ((res Y) (P≡≈ (π₂ ++ π₁)) ((feqi≈ F) ((res X) 
                                                                                                        ((isEquivalence.Symm (pEquiv≡)) {invPerm (π₂ ++ π₁)}{(invPerm π₁) ++ (invPerm π₂)} (p₁p₂⁻¹≈p₂⁻¹p₁⁻¹ π₂ π₁)) (≈≡ (eq≈ₐ X) {x}{x} refl)))) >
                                                             (((Act Y) (π₂ ++ π₁) ((ffun F) ((Act X) (invPerm (π₂ ++ π₁)) x))) by (≈ₐ Y) as (eq≈ₐ Y) ) )))))


-----------------------------------------------------------------------------------------------------------------------------------------------
--identity axiom
-----------------------------------------------------------------------------------------------------------------------------------------------

fι↠ : {X Y : Nominal}  ιAct {Perm}{Funfs X Y}{≈fs {X}{Y}}{fAct {X}{Y}} ι
fι↠ {X}{Y} = λ {F}   x  (((Act Y) ι ((ffun F) ((Act X) ι x)))  
                                                                          ≣< ((ffun F) ((Act X) ι x))
                                                                                and ((ffun F) x)
                                                                                by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                              (ι↠ Y) {((ffun F) ((Act X) ι x))} >
                                               (((ffun F) ((Act X) ι x))
                                                                        ≣< ((ffun F) x)
                                                                               and ((ffun F) x)
                                                                               by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                               (feqi≈ F)((ι↠ X) {x}) >
                                                (((ffun F) x) by (≈ₐ Y) as (eq≈ₐ Y) ))))



------------------------------------------------------------------------------------------------------------------
--exponential object
------------------------------------------------------------------------------------------------------------------

NomExp : (X Y : Nominal)  Nominal
NomExp X Y = record { Aₛ = Funfs X Y
                                    ; ≈ₐ = ≈fs {X} {Y}
                                    ; eq≈ₐ = eq≈fs {X}{Y}
                                    ; Act = λ π  λ F  fAct {X}{Y} π F
                                    ; res = λ {π₁ π₂ F G}  λ π₁≈π₂  λ F≈G  fActRes X Y {π₁}{π₂}{F}{G} π₁≈π₂ F≈G 
                                    ; p₁p₂↠ = fp₁p₂↠ {X}{Y}
                                    ; ι↠ = λ {F}  fι↠ {X}{Y}{F}
                                    ; some_supp = λ F  (fsupp F)
                                    ; suppAx = λ F  λ b c  λ b∉F  λ c∉F  λ x  ((fsuppAx F) b c b∉F c∉F x)
                                    } 


-------------------------------------------------------------------------------------------------------------------------------------
                                                --APPLICATION MORPHISM
-------------------------------------------------------------------------------------------------------------------------------------

appN : (X Y : Nominal)  Equivar (Prod (NomExp X Y) X) Y
appN X Y = record { ufun = λ fx  (ffun (proj₁ fx)) (proj₂ fx)
                               ; eqi≈ = λ {fx₁ fx₂}  λ fx₁≈fx₂  ((ffun (proj₁ fx₁)) (proj₂ fx₁) 
                                                                                          ≣< ((ffun (proj₁ fx₂)) (proj₂ fx₁)) and ((ffun (proj₁ fx₂)) (proj₂ fx₂)) by (≈ₐ Y) as (eq≈ₐ Y) on ((proj₁ fx₁≈fx₂) (proj₂ fx₁)) >  
                                                                                    ((ffun (proj₁ fx₂)) (proj₂ fx₁)
                                                                                          ≣< ((ffun (proj₁ fx₂)) (proj₂ fx₂)) and ((ffun (proj₁ fx₂)) (proj₂ fx₂)) by (≈ₐ Y) as (eq≈ₐ Y) on (feqi≈ (proj₁ fx₂))(proj₂ fx₁≈fx₂) >
                                                                                    (((ffun (proj₁ fx₂)) (proj₂ fx₂)) by (≈ₐ Y) as (eq≈ₐ Y) )))
                               ; equiv = λ π  λ fx  (isEquivalence.Symm (eq≈ₐ Y)) 
                                                                  (((Act Y) π ((ffun (proj₁ fx))((Act X) (invPerm π) ((Act X) π (proj₂ fx))))) 
                                                                                         ≣< ((Act Y) π ((ffun (proj₁ fx))((Act X) (π ++ (invPerm π)) (proj₂ fx)))) and ((Act Y) π ((ffun (proj₁ fx)) (proj₂ fx))) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                                                     ((res Y) (P≡≈ π) ((feqi≈ (proj₁ fx))((p₁p₂↠ X) (invPerm π) π {proj₂ fx})))  >
                                                                  (((Act Y) π ((ffun (proj₁ fx))((Act X) (π ++ (invPerm π)) (proj₂ fx))))
                                                                                        ≣<  ((Act Y) π ((ffun (proj₁ fx))((Act X) ι (proj₂ fx)))) and ((Act Y) π ((ffun (proj₁ fx)) (proj₂ fx))) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                       ((res Y) (P≡≈ π) ((feqi≈ (proj₁ fx))((res X)(pp⁻¹≡ι π)(≈≡ (eq≈ₐ X) {proj₂ fx}{proj₂ fx} refl))))   >
                                                                  (((Act Y) π ((ffun (proj₁ fx))((Act X) ι (proj₂ fx))))
                                                                                       ≣< ((Act Y) π ((ffun (proj₁ fx)) (proj₂ fx))) and ((Act Y) π ((ffun (proj₁ fx)) (proj₂ fx))) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                       ((res Y) (P≡≈ π) ((feqi≈ (proj₁ fx))((ι↠ X) {proj₂ fx})))   >
                                                                                       (((Act Y) π ((ffun (proj₁ fx)) (proj₂ fx))) by (≈ₐ Y) as (eq≈ₐ Y) )))) 
                                }

     

----------------------------------------------------------------------------------------------------------------------------------------
                                                      --CURRYING
----------------------------------------------------------------------------------------------------------------------------------------

currN : (X Y Z : Nominal)  (F : Equivar (Prod Z X) Y)  Equivar Z (NomExp X Y)
currN X Y Z F = record { ufun = λ z  record { ffun = λ x  (ufun F) ( z , x )
                                                                         ; fsupp = (some_supp Z) z
                                                                         ; fsuppAx = λ b c  λ b∉s  λ c∉s  λ x  
                                                                                  (((Act Y) [ ( b , c ) ] ((ufun F) (z , ((Act X) [ ( b , c ) ] x))))
                                                                                                      ≣< ((Act Y) [ ( b , c ) ] ((ufun F) (((Act Z) [ ( b , c ) ] z) , ((Act X) [ ( b , c ) ] x)))) and (ufun F (z , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                                      ((res Y)  {x}  P≡≈ [ ( b , c ) ] {x}) ((eqi≈ F) (((isEquivalence.Symm (eq≈ₐ Z))((suppAx Z) z b c b∉s c∉s)) , 
                                                                                                                                                                                  ((isEquivalence.Reflex (eq≈ₐ X)){(Act X) [ ( b , c ) ] x }))))  >
                                                                                  ((Act Y) [ ( b , c ) ] ((ufun F) (((Act Z) [ ( b , c ) ] z) , ((Act X) [ ( b , c ) ] x)))                          
                                                                                                      ≣< ((ufun F) (((Act Z) [ ( b , c ) ] ((Act Z) [ ( b , c ) ] z)) , ((Act X) [ ( b , c ) ] ((Act X) [ ( b , c ) ] x)))) and (ufun F (z , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                                   ((equiv F) [ ( b , c ) ] ((Act (Prod Z X)) [ ( b , c ) ] ( z , x ))) >
                                                                                  (((ufun F) (((Act Z) [ ( b , c ) ] ((Act Z) [ ( b , c ) ] z)) , ((Act X) [ ( b , c ) ] ((Act X) [ ( b , c ) ] x))))
                                                                                                      ≣< ((ufun F) (((Act Z) ([ ( b , c ) ] ++ [ ( b , c ) ]) z) , ((Act X) ([ ( b , c ) ] ++ [ ( b , c ) ]) x))) and (ufun F (z , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                                  ((eqi≈ F) (((p₁p₂↠ Z) [ ( b , c ) ] [ ( b , c ) ] {z}) , ((p₁p₂↠ X) [ ( b , c ) ] [ ( b , c ) ] {x}))) >                                 
                                                                                  (((ufun F) (((Act Z) ([ ( b , c ) ] ++ [ ( b , c ) ]) z) , ((Act X) ([ ( b , c ) ] ++ [ ( b , c ) ]) x)))
                                                                                                      ≣< ((ufun F) (((Act Z) ι z) , ((Act X) ι x))) and (ufun F (z , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                  ((eqi≈ F) (((res Z) (pp⁻¹≡ι [ ( b , c ) ]) (≈≡ (eq≈ₐ Z) {z}{z} refl)) , ((res X) (pp⁻¹≡ι [ ( b , c ) ]) (≈≡ (eq≈ₐ X) {x}{x} refl)))) >
                                                                                  (((ufun F) (((Act Z) ι z) , ((Act X) ι x))) 
                                                                                                      ≣< (ufun F (z , x)) and (ufun F (z , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                   ((eqi≈ F) (((ι↠ Z) {z}) , ((ι↠ X) {x}))) >
                                                                                  ((ufun F (z , x)) by (≈ₐ Y) as (eq≈ₐ Y) ))))))
                                                                         ; feqi≈ = λ {x₁}{x₂}  λ x₁≈x₂   (eqi≈ F) ((Reflex (eq≈ₐ Z)) {z} , x₁≈x₂)
                                                                         }
                                     ; eqi≈ = λ {z₁}{z₂}  λ z₁≈z₂  λ x  (eqi≈ F) ( z₁≈z₂ , (Reflex (eq≈ₐ X)) {x})
                                     ; equiv = λ π  λ z  λ x  (((Act Y) π ((ufun F) (z , ((Act X) (invPerm π) x))))
                                                                                                                 ≣< ((ufun F) (((Act Z) π z) , ((Act X) π ((Act X) (invPerm π) x)))) and ((ufun F) (((Act Z) π z) , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                                   ((equiv F) π (z , ((Act X) (invPerm π) x))) >
                                                                                (((ufun F) (((Act Z) π z) , ((Act X) π ((Act X) (invPerm π) x))))
                                                                                                                 ≣< (((ufun F) (((Act Z) π z) , ((Act X) ((invPerm π) ++ π) x)))) and ((ufun F) (((Act Z) π z) , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                               ((eqi≈ F)(((Reflex (eq≈ₐ Z)) {(Act Z) π z}) , ((p₁p₂↠ X) π (invPerm π) {x})))  >
                                                                                ((((ufun F) (((Act Z) π z) , ((Act X) ((invPerm π) ++ π) x))))
                                                                                                                ≣< (((ufun F) (((Act Z) π z) , ((Act X) ι x)))) and ((ufun F) (((Act Z) π z) , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                                ((eqi≈ F)(((Reflex (eq≈ₐ Z)) {(Act Z) π z}) , ((res X) (p⁻¹p≡ι π) (≈≡ (eq≈ₐ X) {x}{x} refl))))  >
                                                                                ((((ufun F) (((Act Z) π z) , ((Act X) ι x))))
                                                                                                                ≣< (((ufun F) (((Act Z) π z) ,  x))) and ((ufun F) (((Act Z) π z) , x)) by (≈ₐ Y) as (eq≈ₐ Y) on
                                                                                                                                                ((eqi≈ F)(((Reflex (eq≈ₐ Z)) {(Act Z) π z}) , ((ι↠ X) {x})))  >
                                                                                (((ufun F) (((Act Z) π z) , x)) by (≈ₐ Y) as (eq≈ₐ Y) )))))
                                                                          } 

-------------------------------------------------------------------------------------------------------------------------------------------------
--cartesian closed category
-------------------------------------------------------------------------------------------------------------------------------------------------

ExpN : (X Y : Nominal)  Exp{CarNom} X Y
ExpN X Y = record {  = NomExp X Y
                              ; app = appN X Y
                              ; curr = λ Z  λ F  currN X Y Z F
                              ; comm = λ Z  λ F  λ zx  (Reflex (eq≈ₐ Y)) {(ufun F) ((proj₁ zx) , (proj₂ zx))}
                              ; univ = λ Z  λ F  λ H  λ FC  λ z  λ x  (Symm (eq≈ₐ Y)) (FC (z , x))
                              } 

NomCCC : CCC
NomCCC = record { CarC = CarNom
                               ; exp = λ X Y  ExpN X Y
                               }

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

----------------------------------------------------------------------------------------------------------------------------------------------------
                                                     --EQUIVARIANT SUBSETS
---------------------------------------------------------------------------------------------------------------------------------------------------

EqCon : (N : Nominal)  (Con : (Aₛ N)  Set)  Set
EqCon N Con =  (π : Perm)  (n : Aₛ N)  Con n  Con ((Act N) π n)

record SubEq (N : Nominal) (Con : Aₛ N  Set) (Eq : EqCon N Con) : Set where
  constructor EQ
  field
    n∈N : Aₛ N
    satisfy : Con n∈N

open SubEq public

-------------------------------------------------------------------------------------------------------------------------------------------------------
--equivariant subsets are nominal sets
-------------------------------------------------------------------------------------------------------------------------------------------------------

NomSubEq : (N : Nominal)  (Con : Aₛ N  Set)  (Eq : EqCon N Con)  Nominal
NomSubEq N Con Eq = record { Aₛ = SubEq N Con Eq
                                                  ;  ≈ₐ = λ n₁ n₂  (≈ₐ N) (n∈N n₁) (n∈N n₂)
                                                  ;  eq≈ₐ = record { Reflex = λ {n}  (Reflex (eq≈ₐ N)) {n∈N n}
                                                                              ; Symm = λ n₁≈n₂  (Symm (eq≈ₐ N)) n₁≈n₂  
                                                                              ; Trans = λ n₁≈n₂ n₂≈n₃  (Trans (eq≈ₐ N)) n₁≈n₂ n₂≈n₃
                                                                              }
                                                  ;  Act = λ π  λ n  EQ ((Act N) π (n∈N n)) (Eq π (n∈N n) (satisfy n))
                                                  ;  res = λ π₁≈π₂ n₁≈n₂  (res N) π₁≈π₂ n₁≈n₂
                                                  ;  p₁p₂↠ = λ p₁ p₂ {n}  (p₁p₂↠ N) p₁ p₂ {n∈N n}
                                                  ;  ι↠ = λ {n}  (ι↠ N) {n∈N n}
                                                  ;  some_supp = λ n  (some_supp N) (n∈N n)
                                                  ;  suppAx = λ n b c b∉n c∉n  (suppAx N) (n∈N n) b c b∉n c∉n
                                                  }

-----------------------------------------------------------------------------------------------------------------------------------------------------
                                            --PULLBACKS IN NOM
-----------------------------------------------------------------------------------------------------------------------------------------------------        


-----------------------------------------------------------------------------------------------------------------------------------------------
--object
-----------------------------------------------------------------------------------------------------------------------------------------------

NomPullback : (X Y Z : Nominal)  (Equivar X Z)  (Equivar Y Z)  Nominal
NomPullback X Y Z F G = NomSubEq (Prod X Y)  xy  (≈ₐ Z) ((ufun F) (proj₁ xy)) ((ufun G) (proj₂ xy)))  π  λ xy  λ fx≈gy  let πx = (Act X) π (proj₁ xy) in let πy = (Act Y) π (proj₂ xy) in
                                                                       let fπx≈gπy = ((ufun F) πx) ≣< ((Act Z) π ((ufun F) (proj₁ xy))) and ((ufun G) πy) by (≈ₐ Z) as (eq≈ₐ Z) on ((Symm (eq≈ₐ Z)) ((equiv F) π (proj₁ xy))) >
                                                                                             (((Act Z) π ((ufun F) (proj₁ xy))) ≣< ((Act Z) π ((ufun G) (proj₂ xy))) and ((ufun G) πy) by (≈ₐ Z) as (eq≈ₐ Z) on ((res Z)  {w}  P≡≈ π {w}) fx≈gy) >
                                                                                             (((Act Z) π ((ufun G) (proj₂ xy))) ≣< ((ufun G) πy) and ((ufun G) πy) by (≈ₐ Z) as (eq≈ₐ Z) on ((equiv G) π (proj₂ xy)) >
                                                                                             (((ufun G) πy) by (≈ₐ Z) as (eq≈ₐ Z) ))) in fπx≈gπy)

--------------------------------------------------------------------------------------------------------------------------------------------
--projection morphisms
--------------------------------------------------------------------------------------------------------------------------------------------

NomPull1 : (X Y Z : Nominal)  (F : Equivar X Z)  (G : Equivar Y Z)  Equivar (NomPullback X Y Z F G) X
NomPull1 X Y Z F G = record { ufun = λ xyₛ  proj₁ (n∈N xyₛ)
                                               ;  eqi≈ = λ xy≈xy  proj₁ xy≈xy
                                               ;  equiv = λ π xyₛ  (Reflex (eq≈ₐ X)) {(Act X) π (proj₁ (n∈N xyₛ))}
                                               }

NomPull2 : (X Y Z : Nominal)  (F : Equivar X Z)  (G : Equivar Y Z)  Equivar (NomPullback X Y Z F G) Y
NomPull2 X Y Z F G = record { ufun = λ xyₛ  proj₂ (n∈N xyₛ)
                                               ;  eqi≈ = λ xy≈xy  proj₂ xy≈xy
                                               ;  equiv = λ π xyₛ  (Reflex (eq≈ₐ Y)) {(Act Y) π (proj₂ (n∈N xyₛ))}
                                               }

------------------------------------------------------------------------------------------------------------------------
--pullbacks
------------------------------------------------------------------------------------------------------------------------

NomPull : (X Y Z : Nominal)  (F : Equivar X Z)  (G : Equivar Y Z)  Pullbacks NomCat X Y Z F G
NomPull X Y Z F G = record { X⊗Y = NomPullback X Y Z F G 
                                             ;  X⊗Y→X = NomPull1 X Y Z F G
                                             ;  X⊗Y→Y = NomPull2 X Y Z F G
                                             ;  f∘p₁≡g∘p₂ = λ xyₛ  satisfy xyₛ
                                             ;  W→X⊗Y = λ W F' G' FF'≈GG'  record { ufun = λ w  EQ (((ufun F') w) , ((ufun G') w)) (FF'≈GG' w)
                                                                                                            ;  eqi≈ = λ w₁≈w₂  (((eqi≈ F') w₁≈w₂) , ((eqi≈ G') w₁≈w₂))
                                                                                                            ;  equiv = λ π w  (((equiv F') π w) , ((equiv G') π w))
                                                                                                            } 
                                             ;  WXY₁ = λ W F' G' FF'≈GG'  λ w  (Reflex (eq≈ₐ X)) {(ufun F') w} 
                                             ;  WXY₂ = λ W F' G' FF'≈GG'  λ w  (Reflex (eq≈ₐ Y)) {(ufun G') w}
                                             ;  W↠X⊗Y = λ W F' G' FF'≈GG' H P₁H≈F' P₂H≈G'  λ w  (((Symm (eq≈ₐ X))(P₁H≈F' w)) , ((Symm (eq≈ₐ Y))(P₂H≈G' w))) 
                                             }

PullNom : CatPull NomCat
PullNom = record { Pulls = λ X Y Z F G  NomPull X Y Z F G } 

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