module Adj where
{-
This file proves that the separated product functor has a right adjoint.
-}
open import Basics
open import Atoms
open import Perms
open import PermProp
open import CatDef
open import Nom
open import FreshNom
open import NameAbst
----------------------------------------------------------------------------------------------------------------------------------------------------------
--Adjunction
----------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------
--counit
------------------------------------------------------------------------------------------------------------------------------------------------------------
conc : (X : Nominal) → Equivar (([A] X) *A) X
conc X = record { ufun = λ axa' → let a' = (Aelem axa') in let ax = (Xelem axa') in let a = (proj₁ ax) in let x = (proj₂ ax) in ((Act X) [(a' , a)] x)
; eqi≈ = λ {a₁x₁a₁'}{a₂x₂a₂'} → λ axa' → let a₁'≡a₂' = (proj₂ axa') in let ax≈ax = (proj₁ axa') in
let x₁≈a'ax₁ = ax≈a'a'ax {X = X} (freshCon a₁x₁a₁') in let x₂≈a'ax₂ = ax≈a'a'ax {X = X} (freshCon a₂x₂a₂')
in let a'ax₁≈a'ax₂ = (Trans (α≈ X)) ((Trans (α≈ X))((Symm (α≈ X)) x₁≈a'ax₁) ax≈ax) x₂≈a'ax₂
in let x₁≈x₂ = ax₁≈ax₂ {X = X} a₁'≡a₂' a'ax₁≈a'ax₂ in x₁≈x₂
; equiv = λ π → λ axa' → let a' = (Aelem axa') in let ax = (Xelem axa') in let a = (proj₁ ax) in let x = (proj₂ ax) in
let x≈x = (((Act X) π ((Act X) [(a' , a)] x))
≣< ((Act X) ([(a' , a)] ++ π) x) and ((Act X) [(PermAct π a') , (PermAct π a)] ((Act X) π x)) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) π [(a' , a)] {x}) >
(((Act X) ([(a' , a)] ++ π) x)
≣< ((Act X) (π ++ [(PermAct π a') , (PermAct π a)]) x) and ((Act X) [(PermAct π a') , (PermAct π a)] ((Act X) π x)) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((res X) (π+πab≈abπ π a' a) (≈≡ (eq≈ₐ X) {x}{x} refl))) >
(((Act X) (π ++ [(PermAct π a') , (PermAct π a)]) x)
≣<((Act X) [(PermAct π a') , (PermAct π a)] ((Act X) π x)) and ((Act X) [(PermAct π a') , (PermAct π a)] ((Act X) π x)) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((p₁p₂↠ X) [(PermAct π a') , (PermAct π a)] π {x})) >
(((Act X) [(PermAct π a') , (PermAct π a)] ((Act X) π x)) by (≈ₐ X) as (eq≈ₐ X) ▴)))) in x≈x
}
-----------------------------------------------------------------------------------------------------------------------------------------------
--unique morphism
-----------------------------------------------------------------------------------------------------------------------------------------------
Y⟶[A]X : (X Y : Nominal) → (F : Equivar (Y *A) X) → Equivar Y ([A] X)
Y⟶[A]X X Y F = record {ufun = λ y → let csup = (some_supp Y) y in let b = outside csup in let b∉y = outside∉ csup
in let y≈y = bby≈y {Y} y b
in let ya = SP y b (fresh b b∉y y≈y) in let ax = (b , ((ufun F) ya)) in ax
; eqi≈ = λ {y₁}{y₂} → λ y₁≈y₂ → let a₁ = outside ((some_supp Y) y₁) in let a₁∉y₁ = outside∉ ((some_supp Y) y₁)
in let a₂ = outside ((some_supp Y) y₂) in let a₂∉y₂ = outside∉ ((some_supp Y) y₂)
in let ya₁ = (SP y₁ a₁ (fresh a₁ a₁∉y₁ (bby≈y {Y} y₁ a₁)))
in let ya₂ = (SP y₂ a₂ (fresh a₂ a₂∉y₂ (bby≈y {Y} y₂ a₂)))
in let x₁ = (ufun F) ya₁
in let x₂ = (ufun F) ya₂
in let c3 = ((some_supp Y) y₁) ++ ((some_supp Y) y₂)
in let c2 = ((some_supp X) x₂) ++ c3
in let c1 = ((some_supp X) x₁) ++ c2
in let b = outside c1 in let b∉xy = outside∉ c1
in let b∉x₁ = ∉⊆₁ {(some_supp X) x₁}{c2} b b∉xy
in let b∉x₂ = ∉⊆₁ {(some_supp X) x₂}{c3} b (∉⊆₂ {(some_supp X) x₁}{c2} b b∉xy)
in let b∉y₁ = ∉⊆₁ {(some_supp Y) y₁}{(some_supp Y) y₂} b (∉⊆₂ {(some_supp X) x₂}{c3} b (∉⊆₂ {(some_supp X) x₁}{c2} b b∉xy))
in let b∉y₂ = ∉⊆₂ {(some_supp Y) y₁}{(some_supp Y) y₂} b (∉⊆₂ {(some_supp X) x₂}{c3} b (∉⊆₂ {(some_supp X) x₁}{c2} b b∉xy))
in let x₁≈x₂ = (((Act X) [(b , a₁)] ((ufun F) ya₁))
≣< ((ufun F) ((Act (Y *A)) [(b , a₁)] ya₁)) and ((Act X) [(b , a₂)] ((ufun F) ya₂)) by (≈ₐ X) as (eq≈ₐ X) on
((equiv F) [(b , a₁)] ya₁) >
(((ufun F) ((Act (Y *A)) [(b , a₁)] ya₁))
≣< ((ufun F) (SP y₁ b (fresh b b∉y₁ (bby≈y {Y} y₁ b)))) and ((Act X) [(b , a₂)] ((ufun F) ya₂)) by (≈ₐ X) as (eq≈ₐ X) on
((eqi≈ F) (((suppAx Y) y₁ b a₁ b∉y₁ a₁∉y₁) , (swapabb≡a b a₁))) >
(((ufun F) (SP y₁ b _))
≣< ((ufun F) (SP y₂ b (fresh b b∉y₂ (bby≈y {Y} y₂ b)))) and ((Act X) [(b , a₂)] ((ufun F) ya₂)) by (≈ₐ X) as (eq≈ₐ X) on
((eqi≈ F) (y₁≈y₂ , refl)) >
(((ufun F) (SP y₂ b _))
≣< ((ufun F) ((Act (Y *A)) [(b , a₂)] ya₂)) and ((Act X) [(b , a₂)] ((ufun F) ya₂)) by (≈ₐ X) as (eq≈ₐ X) on
((eqi≈ F) (((Symm (eq≈ₐ Y))((suppAx Y) y₂ b a₂ b∉y₂ a₂∉y₂)) , (sym (swapabb≡a b a₂)))) >
(((ufun F) ((Act (Y *A)) [(b , a₂)] ya₂))
≣< ((Act X) [(b , a₂)] ((ufun F) ya₂)) and ((Act X) [(b , a₂)] ((ufun F) ya₂)) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X))((equiv F) [(b , a₂)] ya₂)) >
(((Act X) [(b , a₂)] ((ufun F) ya₂)) by (≈ₐ X) as (eq≈ₐ X) ▴))))))
in NName b b∉x₁ b∉x₂ x₁≈x₂
; equiv = λ π → λ y → let πy = (Act Y) π y in let a₁ = outside ((some_supp Y) y) in let a₁∉y = outside∉ ((some_supp Y) y) in let ya₁ = (SP y a₁ (fresh a₁ a₁∉y (bby≈y {Y} y a₁)))
in let x₁ = (ufun F) ya₁ in let a₂ = outside ((some_supp Y) πy) in let a₂∉πy = outside∉ ((some_supp Y) πy) in let πya₂ = (SP πy a₂ (fresh a₂ a₂∉πy (bby≈y {Y} πy a₂)))
in let x₂ = (ufun F) πya₂ in let πx₁ = (Act X) π x₁ in
let c4 = ((some_supp Y) y) ++ ((some_supp Y) πy) in
let c3 = ((some_supp X) x₂) ++ c4 in
let c2 = ((some_supp X) πx₁) ++ c3 in
let c1 = (flatten π) ++ c2 in
let b = outside c1 in
let b∉xy = outside∉ c1 in
let b∉π = ∉⊆₁ {flatten π}{c2} b b∉xy in
let b∉πx₁ = ∉⊆₁ {(some_supp X) πx₁} {c3} b (∉⊆₂ {flatten π}{c2} b b∉xy) in
let b∉x₂ = ∉⊆₁ {(some_supp X) x₂}{c4} b (∉⊆₂ {(some_supp X) πx₁} {c3} b (∉⊆₂ {flatten π}{c2} b b∉xy)) in
let b∉y = ∉⊆₁ {(some_supp Y) y}{(some_supp Y) πy} b (∉⊆₂ {(some_supp X) x₂}{c4} b (∉⊆₂ {(some_supp X) πx₁} {c3} b (∉⊆₂ {flatten π}{c2} b b∉xy))) in
let b∉πy = ∉⊆₂ {(some_supp Y) y}{(some_supp Y) πy} b (∉⊆₂ {(some_supp X) x₂}{c4} b (∉⊆₂ {(some_supp X) πx₁} {c3} b (∉⊆₂ {flatten π}{c2} b b∉xy))) in
let y≈y = (((Act Y) ([(a₁ , b)] ++ π) y)
≣< ((Act Y) π ((Act Y) [(a₁ , b)] y)) and ((Act Y) [(b , a₂)] πy) by (≈ₐ Y) as (eq≈ₐ Y) on
((Symm (eq≈ₐ Y)) ((p₁p₂↠ Y) π [(a₁ , b)] {y})) >
(((Act Y) π ((Act Y) [(a₁ , b)] y))
≣< πy and ((Act Y) [(b , a₂)] πy) by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {x} → P≡≈ π {x}) ((suppAx Y) y a₁ b a₁∉y b∉y)) >
(πy
≣< ((Act Y) [(b , a₂)] πy) and ((Act Y) [(b , a₂)] πy) by (≈ₐ Y) as (eq≈ₐ Y) on
((Symm (eq≈ₐ Y)) ((suppAx Y) πy b a₂ b∉πy a₂∉πy)) >
(((Act Y) [(b , a₂)] πy) by (≈ₐ Y) as (eq≈ₐ Y) ▴)))) in
let b≈b = ((PermAct ([(a₁ , b)] ++ π) a₁)
≡< p₁++p₂≡p₂p₁ {a₁} [(a₁ , b)] π >
((PermAct π (PermAct [(a₁ , b)] a₁))
≡< cong (λ w → PermAct π w) (swapaba≡b a₁ b) >
((PermAct π b)
≡< pa≡a π b b∉π >
(b
≡< sym (swapabb≡a b a₂) >
((PermAct [(b , a₂)] a₂) ▪))))) in
let x₁≈x₂ = (((Act X) [(b , (PermAct π a₁))] ((Act X) π x₁))
≣< ((Act X) [((PermAct π a₁) , b)] ((Act X) π x₁)) and ((Act X) [(b , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → ab=ba b (PermAct π a₁) {x}) (≈≡ (eq≈ₐ X) {(Act X) π x₁} {(Act X) π x₁} refl)) >
(((Act X) [((PermAct π a₁) , b)] ((Act X) π x₁))
≣< ((Act X) (π ++ [((PermAct π a₁) , b)]) x₁) and ((Act X) [(b , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) [((PermAct π a₁) , b)] π {x₁}) >
(((Act X) (π ++ [((PermAct π a₁) , b)]) x₁)
≣< ((Act X) ([(a₁ , b)] ++ π) x₁) and ((Act X) [(b , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {w} → πabπ≈πab π a₁ b b∉π {w}) (≈≡ (eq≈ₐ X) {x₁}{x₁} refl)) >
(((Act X) ([(a₁ , b)] ++ π) x₁)
≣< ((ufun F) ((Act (Y *A)) ([(a₁ , b)] ++ π) ya₁)) and ((Act X) [(b , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((equiv F) ([(a₁ , b)] ++ π) ya₁) >
(((ufun F) ((Act (Y *A)) ([(a₁ , b)] ++ π) ya₁))
≣< ((ufun F) ((Act (Y *A)) [(b , a₂)] πya₂)) and ((Act X) [(b , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((eqi≈ F) (y≈y , b≈b)) >
(((ufun F) ((Act (Y *A)) [(b , a₂)] πya₂))
≣< ((Act X) [(b , a₂)] x₂) and ((Act X) [(b , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) on
((Symm (eq≈ₐ X)) ((equiv F) [(b , a₂)] πya₂)) >
(((Act X) [(b , a₂)] x₂) by (≈ₐ X) as (eq≈ₐ X) ▴))))))) in
NName b b∉πx₁ b∉x₂ x₁≈x₂
}
------------------------------------------------------------------------------------------------------------------------------------
--adjoint
------------------------------------------------------------------------------------------------------------------------------------
*A⊣[A] : Adjoint NomCat NomCat NomSep NomAbs
*A⊣[A] = record { counit = λ X → conc X
; f̂ = λ X Y → λ F → Y⟶[A]X X Y F
; f̂ε = λ X Y → λ F → λ ya' → let y = (Xelem ya') in let a' = (Aelem ya') in let a = outside ((some_supp Y) y) in let a∉y = outside∉ ((some_supp Y) y)
in let a'ay≈y = (fixed (Some⇒any {X = Y} (freshCon ya') a a∉y)) in let ya = (SP y a (fresh a a∉y (bby≈y {Y} y a)))
in let x = (ufun F) ya in
let x≈x = (((Act X) [(a' , a)] x)
≣< ((ufun F) ((Act (Y *A)) [(a' , a)] ya)) and ((ufun F) ya') by (≈ₐ X) as (eq≈ₐ X) on
((equiv F) [(a' , a)] ya) >
(((ufun F) ((Act (Y *A)) [(a' , a)] ya))
≣< ((ufun F) ya') and ((ufun F) ya') by (≈ₐ X) as (eq≈ₐ X) on
((eqi≈ F) (a'ay≈y , (swapabb≡a a' a))) >
(((ufun F) ya') by (≈ₐ X) as (eq≈ₐ X) ▴))) in x≈x
; unif̂ = λ X Y → λ F G → λ G∘C≈F → λ y → let a = outside ((some_supp Y) y) in let a∉y = outside∉ ((some_supp Y) y) in let ya = (SP y a (fresh a a∉y (bby≈y {Y} y a)))
in let g≈f = G∘C≈F ya in let a#gy = freshCon ((ufun (X*A⟶Y*A Y ([A] X) G)) ya) in let gy≈aa'x = ax≈a'a'ax {X = X} a#gy
in let ag≈af = ≈α X ((Act X) [(a , (proj₁ ((ufun G) y)))] (proj₂ ((ufun G) y))) ((ufun F) ya) a a refl g≈f
in let g≈f̂ = Trans (α≈ X) gy≈aa'x ag≈af in g≈f̂
}
------------------------------------------------------------------------------------------------------------------------------------------