From d644d36931f405a3abea72cda40c698ac410529d Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Thu, 30 May 2024 23:05:45 +0530 Subject: [PATCH] Archive --- src/Categories/PullbackFunctor.agda | 97 +++++++++++ .../ApplicativeStructure.lagda.md | 31 ++-- .../Assembly/LocallyCartesianClosed.agda | 155 ++++++++++++++++++ src/Realizability/Assembly/Pullbacks.agda | 40 ----- src/Realizability/Assembly/Reindexing.agda | 43 +++++ 5 files changed, 311 insertions(+), 55 deletions(-) create mode 100644 src/Categories/PullbackFunctor.agda create mode 100644 src/Realizability/Assembly/LocallyCartesianClosed.agda create mode 100644 src/Realizability/Assembly/Reindexing.agda diff --git a/src/Categories/PullbackFunctor.agda b/src/Categories/PullbackFunctor.agda new file mode 100644 index 0000000..caea860 --- /dev/null +++ b/src/Categories/PullbackFunctor.agda @@ -0,0 +1,97 @@ +{-# OPTIONS --allow-unsolved-metas #-} +open import Cubical.Foundations.Prelude +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.Limits.Pullback +open import Cubical.Categories.Constructions.Slice + +module Categories.PullbackFunctor where + +private + variable + ℓ ℓ' : Level +module _ (C : Category ℓ ℓ') (pullbacks : Pullbacks C) where + open Category C + open Pullback + open SliceOb + open SliceHom + module _ {X Y : ob} (f : Hom[ X , Y ]) where + module TransformMaps {A B : ob} (m : Hom[ A , Y ]) (n : Hom[ B , Y ]) (k : Hom[ A , B ]) (tri : k ⋆ n ≡ m) where + cospanA : Cospan C + cospanA = cospan X Y A f m + + cospanB : Cospan C + cospanB = cospan X Y B f n + + P : ob + P = pullbacks cospanA .pbOb + + Q : ob + Q = pullbacks cospanB .pbOb + + f*m : Hom[ P , X ] + f*m = pullbacks cospanA .pbPr₁ + + g : Hom[ P , A ] + g = pullbacks cospanA .pbPr₂ + + f*n : Hom[ Q , X ] + f*n = pullbacks cospanB .pbPr₁ + + h : Hom[ Q , B ] + h = pullbacks cospanB .pbPr₂ + + f*m⋆f≡g⋆m : f*m ⋆ f ≡ g ⋆ m + f*m⋆f≡g⋆m = pullbacks cospanA .pbCommutes + + g⋆k : Hom[ P , B ] + g⋆k = g ⋆ k + + g⋆k⋆n≡f*m⋆f : (g ⋆ k) ⋆ n ≡ f*m ⋆ f + g⋆k⋆n≡f*m⋆f = + (g ⋆ k) ⋆ n + ≡⟨ ⋆Assoc g k n ⟩ + g ⋆ (k ⋆ n) + ≡⟨ cong (λ x → g ⋆ x) tri ⟩ + g ⋆ m + ≡⟨ sym f*m⋆f≡g⋆m ⟩ + f*m ⋆ f + ∎ + + arrow : Hom[ P , Q ] + arrow = pullbackArrow C (pullbacks cospanB) f*m g⋆k (sym g⋆k⋆n≡f*m⋆f) + + arrow⋆f*n≡f*m : arrow ⋆ f*n ≡ f*m + arrow⋆f*n≡f*m = sym (pullbackArrowPr₁ C (pullbacks cospanB) f*m g⋆k (sym g⋆k⋆n≡f*m⋆f)) + + reindexFunctor : Functor (SliceCat C Y) (SliceCat C X) + Functor.F-ob reindexFunctor (sliceob {A} m) = sliceob (pullbacks (cospan X Y A f m) .pbPr₁) + Functor.F-hom reindexFunctor {sliceob {A} m} {sliceob {B} n} (slicehom k tri) = slicehom arrow arrow⋆f*n≡f*m where open TransformMaps m n k tri + Functor.F-id reindexFunctor {sliceob {A} m} = SliceHom-≡-intro' C X (pullbackArrowUnique C (pullbacks cospanB) f*m g⋆k (sym g⋆k⋆n≡f*m⋆f) id (sym (⋆IdL f*m)) (⋆IdR g ∙ sym (⋆IdL g))) where open TransformMaps m m id (⋆IdL m) + Functor.F-seq reindexFunctor {sliceob {A} m} {sliceob {B} n} {sliceob {C'} o} (slicehom j jComm) (slicehom k kComm) = SliceHom-≡-intro' C X {!!} where + module ABTransform = TransformMaps m n j jComm + module BCTransform = TransformMaps n o k kComm + module ACTransform = TransformMaps m o (j ⋆ k) (⋆Assoc j k o ∙ cong (λ x → j ⋆ x) kComm ∙ jComm) + + P : ob + P = ABTransform.P + + f*m : Hom[ P , X ] + f*m = ABTransform.f*m + + Q : ob + Q = ABTransform.Q + + R : ob + R = BCTransform.P + + f*n : Hom[ Q , X ] + f*n = ABTransform.f*n + + g : Hom[ P , A ] + g = ABTransform.g + + f*m⋆f≡g⋆m : f*m ⋆ f ≡ g ⋆ m + f*m⋆f≡g⋆m = ABTransform.f*m⋆f≡g⋆m + + diff --git a/src/Realizability/ApplicativeStructure.lagda.md b/src/Realizability/ApplicativeStructure.lagda.md index 3eeb7dd..2287fef 100644 --- a/src/Realizability/ApplicativeStructure.lagda.md +++ b/src/Realizability/ApplicativeStructure.lagda.md @@ -60,7 +60,7 @@ module _ {ℓ} {A : Type ℓ} (as : ApplicativeStructure A) where infix 23 `_ infixl 22 _̇_ data Term (n : ℕ) : Type ℓ where - # : (Vec A n → A) → Term n + # : Fin n → Term n `_ : A → Term n _̇_ : Term n → Term n → Term n ``` @@ -69,8 +69,8 @@ These terms can be evaluated into $A$ if we can give the values of the free vari ```agda ⟦_⟧ : ∀ {n} → Term n → Vec A n → A - ⟦_⟧ (` a) subs = a - ⟦_⟧ {n} (# k) subs = k subs + ⟦_⟧ (` a) _ = a + ⟦_⟧ {n} (# k) subs = lookup k subs ⟦_⟧ (a ̇ b) subs = (⟦ a ⟧ subs) ⨾ (⟦ b ⟧ subs) applicationChain : ∀ {n m} → Vec (Term m) (suc n) → Term m @@ -115,12 +115,13 @@ We will call this `λ*abst` and this will turn out to behave very similar to λ ```agda module ComputationRules (feferman : Feferman) where open Feferman feferman - + opaque λ*abst : ∀ {n} → (e : Term (suc n)) → Term n - λ*abst {n} (# x) = {!!} - λ*abst {n} (` x) = {!!} - λ*abst {n} (e ̇ e₁) = {!!} + λ*abst {n} (# zero) = ` s ̇ ` k ̇ ` k + λ*abst {n} (# (suc x)) = ` k ̇ # x + λ*abst {n} (` x) = ` k ̇ ` x + λ*abst {n} (e ̇ e₁) = ` s ̇ λ*abst e ̇ λ*abst e₁ ``` **Remark** : It is important to note that in general, realizability is developed using **partial combinatory algebras** and **partial applicative structures**. In this case, `λ*abst` is not particularly well-behaved. The β reduction-esque rule we derive also does not behave *completely* like β reduction. See Jonh Longley's PhD thesis "Realizability Toposes and Language Semantics" Theorem 1.1.9. @@ -130,7 +131,7 @@ We will call this `λ*abst` and this will turn out to behave very similar to λ We define meta-syntactic sugar for some of the more common cases : ```agda - {-λ* : Term one → A + λ* : Term one → A λ* t = ⟦ λ*abst t ⟧ [] λ*2 : Term two → A @@ -140,7 +141,7 @@ We define meta-syntactic sugar for some of the more common cases : λ*3 t = ⟦ λ*abst (λ*abst (λ*abst t)) ⟧ [] λ*4 : Term four → A - λ*4 t = ⟦ λ*abst (λ*abst (λ*abst (λ*abst t))) ⟧ [] -} + λ*4 t = ⟦ λ*abst (λ*abst (λ*abst (λ*abst t))) ⟧ [] ``` We now show that we have a β-reduction-esque operation. We proceed by induction on the structure of the term and the number of free variables. @@ -149,7 +150,7 @@ For the particular combinatory algebra Λ/β (terms of the untyped λ calculus q TODO : Prove this. ```agda - {- opaque + opaque unfolding λ*abst βreduction : ∀ {n} → (body : Term (suc n)) → (prim : A) → (subs : Vec A n) → ⟦ λ*abst body ̇ ` prim ⟧ subs ≡ ⟦ body ⟧ (prim ∷ subs) βreduction {n} (# zero) prim subs = @@ -167,24 +168,24 @@ TODO : Prove this. ⟦ λ*abst rator ⟧ subs ⨾ prim ⨾ (⟦ λ*abst rand ⟧ subs ⨾ prim) ≡⟨ cong₂ (λ x y → x ⨾ y) (βreduction rator prim subs) (βreduction rand prim subs) ⟩ ⟦ rator ⟧ (prim ∷ subs) ⨾ ⟦ rand ⟧ (prim ∷ subs) - ∎ -} + ∎ ```
```agda - {-λ*chainTerm : ∀ n → Term n → Term zero + λ*chainTerm : ∀ n → Term n → Term zero λ*chainTerm zero t = t λ*chainTerm (suc n) t = λ*chainTerm n (λ*abst t) λ*chain : ∀ {n} → Term n → A - λ*chain {n} t = ⟦ λ*chainTerm n t ⟧ [] -} + λ*chain {n} t = ⟦ λ*chainTerm n t ⟧ [] ```
We provide useful reasoning combinators that are useful and frequent. ```agda - {- opaque + opaque unfolding reverse unfolding foldl unfolding chain @@ -231,5 +232,5 @@ We provide useful reasoning combinators that are useful and frequent. ⟦ λ*abst t ⟧ (c ∷ b ∷ a ∷ []) ⨾ ⟦ ` d ⟧ (c ∷ b ∷ a ∷ []) ≡⟨ βreduction t d (c ∷ b ∷ a ∷ []) ⟩ ⟦ t ⟧ (d ∷ c ∷ b ∷ a ∷ []) - ∎ -} + ∎ ``` diff --git a/src/Realizability/Assembly/LocallyCartesianClosed.agda b/src/Realizability/Assembly/LocallyCartesianClosed.agda new file mode 100644 index 0000000..8e94d88 --- /dev/null +++ b/src/Realizability/Assembly/LocallyCartesianClosed.agda @@ -0,0 +1,155 @@ +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.HITs.PropositionalTruncation as PT hiding (map) +open import Cubical.HITs.PropositionalTruncation.Monad +open import Cubical.Categories.Limits.Pullback +open import Cubical.Categories.Category.Base +open import Cubical.Categories.Functor +open import Cubical.Categories.Constructions.Slice +open import Cubical.Categories.Adjoint +open import Realizability.CombinatoryAlgebra +open import Realizability.ApplicativeStructure +open import Categories.PullbackFunctor + +module Realizability.Assembly.LocallyCartesianClosed {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open CombinatoryAlgebra ca +open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) hiding (Z) +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca +open import Realizability.Assembly.Pullbacks ca +open import Realizability.Assembly.Reindexing ca +open NaturalBijection +open SliceOb + +module _ {X Y : Type ℓ} {asmX : Assembly X} {asmY : Assembly Y} (f : AssemblyMorphism asmX asmY) where + module SliceDomain {V : Type ℓ} {asmV : Assembly V} (h : AssemblyMorphism asmV asmX) where + + D : Type ℓ + D = Σ[ y ∈ Y ] Σ[ s ∈ (fiber (f .map) y → V)] (∀ (yFiberF : fiber (f .map) y) → h .map (s yFiberF) ≡ yFiberF .fst) + + isSetD : isSet D + isSetD = + isSetΣ + (asmY .isSetX) + (λ y → + isSetΣ + (isSet→ (asmV .isSetX)) + (λ s → + isSetΠ λ yFiberF → isProp→isSet (asmX .isSetX _ _))) + + _⊩D_ : A → D → Type ℓ + r ⊩D (y , s , coh) = ((pr₁ ⨾ r) ⊩[ asmY ] y) × (∀ (yFiberF : fiber (f .map) y) (a : A) → a ⊩[ asmX ] (yFiberF .fst) → (pr₂ ⨾ r ⨾ a) ⊩[ asmV ] (s yFiberF)) + + isProp⊩D : ∀ r d → isProp (r ⊩D d) + isProp⊩D r d = + isProp× + (asmY .⊩isPropValued _ _) + (isPropΠ + λ yFiberF → + isPropΠ + λ a → + isProp→ (asmV .⊩isPropValued _ _)) + + asmD : Assembly (Σ[ d ∈ D ] ∃[ r ∈ A ] (r ⊩D d)) + Assembly._⊩_ asmD r (d@(y , s , coh) , ∃r) = r ⊩D d + Assembly.isSetX asmD = isSetΣ isSetD (λ d → isProp→isSet isPropPropTrunc) + Assembly.⊩isPropValued asmD r (d@(y , s , coh) , ∃a) = isProp⊩D r d + Assembly.⊩surjective asmD (d , ∃a) = ∃a + + projection : AssemblyMorphism asmD asmY + AssemblyMorphism.map projection (d@(y , s , coh) , ∃r) = y + AssemblyMorphism.tracker projection = + return + (pr₁ , + (λ { (d@(y , s , coh) , ∃a) r r⊩d → r⊩d .fst })) + + private module SliceDomainHom {V W : Type ℓ} {asmV : Assembly V} {asmW : Assembly W} (g : AssemblyMorphism asmV asmX) (h : AssemblyMorphism asmW asmX) (j : AssemblyMorphism asmV asmW) (comm : j ⊚ h ≡ g) where + + rawMap : SliceDomain.D g → SliceDomain.D h + rawMap (y , s , coh) = + y , + (λ fib → j .map (s fib)) , + λ { fib@(x , fx≡y) → + h .map (j .map (s fib)) + ≡[ i ]⟨ comm i .map (s fib) ⟩ + g .map (s fib) + ≡⟨ coh fib ⟩ + x + ∎ } + + transformRealizers : ∀ (d : SliceDomain.D g) → Σ[ b ∈ A ] (SliceDomain._⊩D_ g b d) → Σ[ j~ ∈ A ] (tracks {xs = asmV} {ys = asmW} j~ (j .map)) → Σ[ r ∈ A ] (SliceDomain._⊩D_ h r (rawMap d)) + transformRealizers d@(y , s , coh) (e , pr₁e⊩y , pr₂e⊩) (j~ , isTrackedJ) = + let + realizer : A + realizer = pair ⨾ (pr₁ ⨾ e) ⨾ λ* (` j~ ̇ (` pr₂ ̇ ` e ̇ # zero)) + + pr₁realizer≡pr₁e : pr₁ ⨾ realizer ≡ pr₁ ⨾ e + pr₁realizer≡pr₁e = + pr₁ ⨾ realizer + ≡⟨ refl ⟩ -- unfolding + pr₁ ⨾ (pair ⨾ (pr₁ ⨾ e) ⨾ λ* (` j~ ̇ (` pr₂ ̇ ` e ̇ # zero))) + ≡⟨ pr₁pxy≡x _ _ ⟩ + pr₁ ⨾ e + ∎ + + pr₂realizerEq : (a : A) → pr₂ ⨾ realizer ⨾ a ≡ j~ ⨾ (pr₂ ⨾ e ⨾ a) + pr₂realizerEq a = + pr₂ ⨾ realizer ⨾ a + ≡⟨ refl ⟩ + pr₂ ⨾ (pair ⨾ (pr₁ ⨾ e) ⨾ λ* (` j~ ̇ (` pr₂ ̇ ` e ̇ # zero))) ⨾ a + ≡⟨ cong (λ x → x ⨾ a) (pr₂pxy≡y _ _) ⟩ + λ* (` j~ ̇ (` pr₂ ̇ ` e ̇ # zero)) ⨾ a + ≡⟨ λ*ComputationRule (` j~ ̇ (` pr₂ ̇ ` e ̇ # zero)) a ⟩ + j~ ⨾ (pr₂ ⨾ e ⨾ a) + ∎ + in + (realizer , + (subst (λ r' → r' ⊩[ asmY ] y) (sym pr₁realizer≡pr₁e) pr₁e⊩y , + (λ { fib@(x , fx≡y) a a⊩x → + subst (λ r' → r' ⊩[ asmW ] (j .map (s fib))) (sym (pr₂realizerEq a)) (isTrackedJ (s fib) (pr₂ ⨾ e ⨾ a) (pr₂e⊩ fib a a⊩x)) }))) + + morphism : AssemblyMorphism (SliceDomain.asmD g) (SliceDomain.asmD h) + AssemblyMorphism.map morphism (d@(y , s , coh) , ∃r) = rawMap d , PT.rec2 isPropPropTrunc (λ r⊩d j~ → ∣ transformRealizers d r⊩d j~ ∣₁) ∃r (j .tracker) + AssemblyMorphism.tracker morphism = + do + (j~ , isTrackedJ) ← j .tracker + let + closure : Term as 2 + closure = (` j~ ̇ (` pr₂ ̇ # one ̇ # zero)) + + realizer : Term as 1 + realizer = ` pair ̇ (` pr₁ ̇ # zero) ̇ (λ*abst closure) + return + (λ* realizer , + (λ { (d@(y , s , coh) , ∃r) a (pr₁a⊩y , pr₂a⊩) → + let + pr₁Eq : pr₁ ⨾ (λ* realizer ⨾ a) ≡ pr₁ ⨾ a + pr₁Eq = + pr₁ ⨾ (λ* realizer ⨾ a) + ≡⟨ cong (λ x → pr₁ ⨾ x) (λ*ComputationRule realizer a) ⟩ + pr₁ ⨾ (pair ⨾ (pr₁ ⨾ a) ⨾ _) + ≡⟨ pr₁pxy≡x _ _ ⟩ + pr₁ ⨾ a + ∎ + in + subst (λ r' → r' ⊩[ asmY ] y) (sym pr₁Eq) pr₁a⊩y , + (λ { fib@(x , fx≡y) b b⊩x → {!isTrackedJ !} }) })) + + Π[_] : Functor (SliceCat ASM (X , asmX)) (SliceCat ASM (Y , asmY)) + Functor.F-ob Π[_] (sliceob {V , asmV} h) = sliceob (SliceDomain.projection h) + Functor.F-hom Π[_] {sliceob {V , asmV} g} {sliceob {W , asmW} h} (slicehom j comm) = {!!} + Functor.F-id Π[_] = {!!} + Functor.F-seq Π[_] = {!!} + + reindex⊣Π[_] : reindexFunctor ASM PullbacksASM f ⊣ Π[_] + Iso.fun (_⊣_.adjIso reindex⊣Π[_]) = λ fo → slicehom {!!} {!!} + Iso.inv (_⊣_.adjIso reindex⊣Π[_]) = {!!} + Iso.rightInv (_⊣_.adjIso reindex⊣Π[_]) = {!!} + Iso.leftInv (_⊣_.adjIso reindex⊣Π[_]) = {!!} + _⊣_.adjNatInD reindex⊣Π[_] = {!!} + _⊣_.adjNatInC reindex⊣Π[_] = {!!} diff --git a/src/Realizability/Assembly/Pullbacks.agda b/src/Realizability/Assembly/Pullbacks.agda index d138559..9a5f39f 100644 --- a/src/Realizability/Assembly/Pullbacks.agda +++ b/src/Realizability/Assembly/Pullbacks.agda @@ -117,43 +117,3 @@ module _ (cspn : Cospan ASM) where PullbacksASM : Pullbacks ASM PullbacksASM cspn = pullback cspn - --- Using pullbacks we get a functor that sends any f : X → Y to f* : Asm / Y → Asm / X -module _ {X Y : Type ℓ} (asmX : Assembly X) (asmY : Assembly Y) (f : AssemblyMorphism asmX asmY) where - open Pullback - opaque - unfolding pullbackAsm - unfolding pullbackPr₁ - unfolding pullback - pullbackFunctor : Functor (SliceCat ASM (Y , asmY)) (SliceCat ASM (X , asmX)) - Functor.F-ob pullbackFunctor sliceY = sliceob (pullback (cospan (X , asmX) (Y , asmY) (sliceY .S-ob) f (sliceY .S-arr)) .pbPr₁) - Functor.F-hom pullbackFunctor {ySliceA} {ySliceB} sliceHomAB = - {-let - sliceACospan : Cospan ASM - sliceACospan = cospan (X , asmX) (Y , asmY) (ySliceA .S-ob) f (ySliceA .S-arr) - p = pullbackPr₂ sliceACospan - m = ySliceA .S-arr - n = ySliceB .S-arr - f*m = pullbackPr₁ sliceACospan - h = sliceHomAB .S-hom - m≡h⊚n = sliceHomAB .S-comm - f*m⊚f≡p⊚m = pbCommutes (pullback sliceACospan) - arrow = - pullbackArrow - ASM - (pullback (cospan (X , asmX) (Y , asmY) (ySliceB .S-ob) f (ySliceB .S-arr))) (pullbackPr₁ sliceACospan) (p ⊚ h) - (AssemblyMorphism≡ _ _ - (funExt - λ { (x , a , fx≡ma) → - f .map x - ≡⟨ fx≡ma ⟩ - m .map a - ≡[ i ]⟨ m≡h⊚n (~ i) .map a ⟩ - n .map (h .map a) - ∎ })) - in - slicehom - arrow-} - {!!} - Functor.F-id pullbackFunctor = {!!} - Functor.F-seq pullbackFunctor = {!!} diff --git a/src/Realizability/Assembly/Reindexing.agda b/src/Realizability/Assembly/Reindexing.agda new file mode 100644 index 0000000..13ddc62 --- /dev/null +++ b/src/Realizability/Assembly/Reindexing.agda @@ -0,0 +1,43 @@ +{-# OPTIONS --allow-unsolved-metas #-} +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.HITs.PropositionalTruncation hiding (map) +open import Cubical.HITs.PropositionalTruncation.Monad +open import Cubical.Categories.Limits.Pullback +open import Cubical.Categories.Category.Base +open import Cubical.Categories.Functor +open import Cubical.Categories.Constructions.Slice +open import Realizability.CombinatoryAlgebra +open import Realizability.ApplicativeStructure +open import Categories.PullbackFunctor + +module Realizability.Assembly.Reindexing {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open CombinatoryAlgebra ca +open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) hiding (Z) +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca +open import Realizability.Assembly.Pullbacks ca +-- Using pullbacks we get a functor that sends any f : X → Y to f* : Asm / Y → Asm / X +module _ {X Y : Type ℓ} {asmX : Assembly X} {asmY : Assembly Y} (f : AssemblyMorphism asmX asmY) where + + open TransformMaps ASM PullbacksASM f + open SliceOb + open SliceHom + open Pullback + + opaque + reindexPb : {A : Type ℓ} (asmA : Assembly A) (m : AssemblyMorphism asmA asmY) → ASM .Category.ob + reindexPb {A} asmA m = pullback (cospan (X , asmX) (Y , asmY) (A , asmA) f m) .pbOb + + opaque + reindexOb : SliceOb ASM (Y , asmY) → SliceOb ASM (X , asmX) + reindexOb (sliceob {A , asmA} m) = sliceob (pullback (cospan (X , asmX) (Y , asmY) (A , asmA) f m) .pbPr₁) + + opaque + unfolding reindexOb + reindexHom : (m n : SliceOb ASM (Y , asmY)) → SliceHom ASM (Y , asmY) m n → SliceHom ASM (X , asmX) (reindexOb m) (reindexOb n) + reindexHom (sliceob {A , asmA} m) (sliceob {B , asmB} n) (slicehom k tri) = slicehom (arrow m n k tri) (arrow⋆f*n≡f*m m n k tri) +