From 6d34d153116ade534a24ef7c8f441c467260d623 Mon Sep 17 00:00:00 2001 From: 5HT Date: Sun, 15 Oct 2023 22:34:10 +0300 Subject: [PATCH] localization --- foundations/modal/localization/index.html | 2 +- foundations/modal/localization/index.pug | 20 ++++++++++---------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/foundations/modal/localization/index.html b/foundations/modal/localization/index.html index a996a7b6..fc8295ea 100644 --- a/foundations/modal/localization/index.html +++ b/foundations/modal/localization/index.html @@ -14,7 +14,7 @@ universal -local type admitting a map from .

.

Introduction

(Localization Modality Constructors). The localization modality is generated by the following higher inductive composition structure:

-

data Localize (A X: U) (S T: A -> U) (F : (x:A) -> S x -> T x) +

data Localize (A X: U) (S T: A -> U) (F : (x:A) -> S x -> T x) = center (x: X) | ext (a: A) (f: S a -> Localize A X S T F) (t: T a) | isExt (a: A) (f: S a -> Localize A X S T F) (s: S a) <i> diff --git a/foundations/modal/localization/index.pug b/foundations/modal/localization/index.pug index ee311098..609d7607 100644 --- a/foundations/modal/localization/index.pug +++ b/foundations/modal/localization/index.pug @@ -41,23 +41,23 @@ block content $$ \begin{cases} \mathrm{center} : X \\ - \mathrm{ext} : \Pi_(a:A) \rightarrow (S(a) \rightarrow L_A(X)) \rightarrow T(a) \\ - \mathrm{isExt} : \Pi_(a:A) \rightarrow (f: S(a) \rightarrow L_A(X)) \\ - \hspace{1em} (s:S(a)) [i] + \mathrm{ext} : \Pi_(a:A) \rightarrow (S(a) \rightarrow L_{F_A}(X)) \rightarrow T(a) \\ + \mathrm{isExt} : \Pi_(a:A) \rightarrow (f: S(a) \rightarrow L_{F_A}(X)) + (s:S(a)) \\ \hspace{1em} [i] \begin{cases} - i=0 \mapsto \mathrm{ext}(a,f,F(a,s)), \\ + i=0 \mapsto \mathrm{ext}(a,f,F_a(s)) \\ i=1 \mapsto f(s) \end{cases} \\ - \mathrm{extEq} : \Pi_{a:A} \rightarrow (g,h: T(a) \rightarrow L_A(X)) \\ - \hspace{1em} (p: \Pi_{s:S(a)}g(F(a,s))=h(F_a(s)) \\ \hspace{1em} (t:T(a)) [i] + \mathrm{extEq} : \Pi_{a:A} \rightarrow (g,h: T(a) \rightarrow L_{F_A}(X)) \\ + \hspace{1em} (p: \Pi_{s:S(a)}g(F_a(s))=h(F_a(s))\ (t:T(a)) \\ \hspace{1em} [i] \begin{cases} - i=0 \mapsto g(t), \\ + i=0 \mapsto g(t) \\ i=1 \mapsto h(t) \end{cases} \\ - \mathrm{isExtEq} : \Pi_{a:A} \rightarrow (g,h: T(a) \rightarrow L_A(X)) \\ - \hspace{1em} (p: \Pi_{s:S(a)}g(F_a(s))=h(F(a,s)) \\ \hspace{1em} (s:S(a)) [i] + \mathrm{isExtEq} : \Pi_{a:A} \rightarrow (g,h: T(a) \rightarrow L_{F_A}(X)) \\ + \hspace{1em} (p: \Pi_{s:S(a)}g(F_a(s))=h(F_a(s))\ (s:S(a)) \\ \hspace{1em} [i] \begin{cases} - i=0 \mapsto \mathrm{extEq}(a,g,h,p,F(a,s))\ @\ 0, \\ + i=0 \mapsto \mathrm{extEq}(a,g,h,p,F_a(s))\ @\ 0 \\ i=1 \mapsto p(s)\ @\ 1 \end{cases} \\ \end{cases}.