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