Skip to content

Commit

Permalink
Families of modest sets as displayed category
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahulc29
rahulc29 committed Jun 26, 2024
1 parent 41d4f18 commit 73d04b5
Show file tree
Hide file tree
Showing 5 changed files with 362 additions and 40 deletions.
220 changes: 183 additions & 37 deletions src/Realizability/Modest/UniformFamily.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.Path
open import Cubical.Foundations.Structure using (⟨_⟩; str)
open import Cubical.Data.Sigma
open import Cubical.Data.FinData
Expand All @@ -13,59 +14,204 @@ open import Cubical.HITs.PropositionalTruncation.Monad
open import Cubical.Reflection.RecordEquiv
open import Cubical.Categories.Category
open import Cubical.Categories.Displayed.Base
open import Cubical.Categories.Displayed.Reasoning
open import Cubical.Categories.Limits.Pullback
open import Cubical.Categories.Functor
open import Cubical.Categories.Functor hiding (Id)
open import Cubical.Categories.Constructions.Slice
open import Realizability.CombinatoryAlgebra
open import Realizability.ApplicativeStructure
open import Realizability.PropResizing

module Realizability.Modest.UniformFamily {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where


open import Realizability.Assembly.Base ca
open import Realizability.Assembly.Morphism ca
open import Realizability.Assembly.Terminal ca
open import Realizability.Assembly.LocallyCartesianClosed ca
open import Realizability.Modest.Base ca

open Assembly
open CombinatoryAlgebra ca
open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)

UNIMOD : Categoryᴰ ASM (ℓ-suc ℓ) ℓ
Categoryᴰ.ob[ UNIMOD ] (X , asmX) = Σ[ Y ∈ Type ℓ ] Σ[ asmY ∈ Assembly Y ] isModest asmY × AssemblyMorphism asmY asmX
Categoryᴰ.Hom[_][_,_] UNIMOD {X , asmX} {Y , asmY} reindex (V , asmV , isModestAsmV , m) (W , asmW , isModestAsmW , n) = Σ[ reindexᵈ ∈ (AssemblyMorphism asmV asmW) ] m ⊚ reindex ≡ reindexᵈ ⊚ n
Categoryᴰ.idᴰ UNIMOD {X , asmX} {V , asmV , isModestAsmV , m} = (identityMorphism asmV) , (Category.⋆IdR ASM m ∙ sym (Category.⋆IdL ASM m))
Categoryᴰ._⋆ᴰ_ UNIMOD
{X , asmX} {Y , asmY} {Z , asmZ} {f} {g}
{U , asmU , isModestU , m} {V , asmV , isModestV , n} {W , asmW , isModestW , o}
(fᵈ , fᵈcomm) (gᵈ , gᵈcomm) =
(fᵈ ⊚ gᵈ) ,
(m ⊚ (f ⊚ g)
≡⟨ sym (Category.⋆Assoc ASM m f g) ⟩
(m ⊚ f) ⊚ g
≡⟨ cong (λ x → x ⊚ g) fᵈcomm ⟩
fᵈ ⊚ n ⊚ g
≡⟨ Category.⋆Assoc ASM fᵈ n g ⟩
fᵈ ⊚ (n ⊚ g)
≡⟨ cong (fᵈ ⊚_) gᵈcomm ⟩
fᵈ ⊚ (gᵈ ⊚ o)
≡⟨ sym (Category.⋆Assoc ASM fᵈ gᵈ o) ⟩
fᵈ ⊚ gᵈ ⊚ o
∎)
Categoryᴰ.⋆IdLᴰ UNIMOD {X , asmX} {Y , asmY} {f} {V , asmV , isModestAsmV , m} {W , asmW , isModestAsmW , n} (fᵈ , fᵈcomm) =
ΣPathPProp (λ fᵈ → isSetAssemblyMorphism asmV asmY _ _) (Category.⋆IdL ASM fᵈ)
Categoryᴰ.⋆IdRᴰ UNIMOD {X , asmX} {Y , asmY} {f} {V , asmV , isModestAsmV , m} {W , asmW , isModestAsmW , n} (fᵈ , fᵈcomm) =
ΣPathPProp (λ fᵈ → isSetAssemblyMorphism asmV asmY _ _) (Category.⋆IdR ASM fᵈ)
Categoryᴰ.⋆Assocᴰ UNIMOD
{X , asmX} {Y , asmY} {Z , asmZ} {W , asmW} {f} {g} {h}
{Xᴰ , asmXᴰ , isModestAsmXᴰ , pX} {Yᴰ , asmYᴰ , isModestAsmYᴰ , pY} {Zᴰ , asmZᴰ , isModestAsmZᴰ , pZ} {Wᴰ , asmWᴰ , isModestAsmWᴰ , pW}
(fᵈ , fᵈcomm) (gᵈ , gᵈcomm) (hᵈ , hᵈcomm) =
ΣPathPProp (λ comp → isSetAssemblyMorphism asmXᴰ asmW _ _) (Category.⋆Assoc ASM fᵈ gᵈ hᵈ )
Categoryᴰ.isSetHomᴰ UNIMOD = isSetΣ (isSetAssemblyMorphism _ _) (λ f → isProp→isSet (isSetAssemblyMorphism _ _ _ _))
record UniformFamily {I : Type ℓ} (asmI : Assembly I) : Type (ℓ-suc ℓ) where
no-eta-equality
field
carriers : I → Type ℓ
assemblies : ∀ i → Assembly (carriers i)
isModestFamily : ∀ i → isModest (assemblies i)
open UniformFamily
record DisplayedUFamMap {I J : Type ℓ} (asmI : Assembly I) (asmJ : Assembly J) (u : AssemblyMorphism asmI asmJ) (X : UniformFamily asmI) (Y : UniformFamily asmJ) : Type ℓ where
no-eta-equality
field
fibrewiseMap : ∀ i → X .carriers i → Y .carriers (u .map i)
isTracked : ∃[ e ∈ A ] (∀ (i : I) (a : A) (a⊩i : a ⊩[ asmI ] i) (x : X .carriers i) (b : A) (b⊩x : b ⊩[ X .assemblies i ] x) → (e ⨾ a ⨾ b) ⊩[ Y .assemblies (u .map i) ] (fibrewiseMap i x))

open DisplayedUFamMap

DisplayedUFamMapPathP :
∀ {I J} (asmI : Assembly I) (asmJ : Assembly J) →
∀ u v X Y
→ (uᴰ : DisplayedUFamMap asmI asmJ u X Y)
→ (vᴰ : DisplayedUFamMap asmI asmJ v X Y)
→ (p : u ≡ v)
→ (∀ (i : I) (x : X .carriers i) → PathP (λ j → Y .carriers (p j .map i)) (uᴰ .fibrewiseMap i x) (vᴰ .fibrewiseMap i x))
-----------------------------------------------------------------------------------------------------------------------
→ PathP (λ i → DisplayedUFamMap asmI asmJ (p i) X Y) uᴰ vᴰ
fibrewiseMap (DisplayedUFamMapPathP {I} {J} asmI asmJ u v X Y uᴰ vᴰ p pᴰ dimI) i x = pᴰ i x dimI
isTracked (DisplayedUFamMapPathP {I} {J} asmI asmJ u v X Y uᴰ vᴰ p pᴰ dimI) =
isProp→PathP
{B = λ dimJ → ∃[ e ∈ A ] ((i : I) (a : A) → a ⊩[ asmI ] i → (x : X .carriers i) (b : A) → b ⊩[ X .assemblies i ] x → (e ⨾ a ⨾ b) ⊩[ Y .assemblies (p dimJ .map i) ] pᴰ i x dimJ)}
(λ dimJ → isPropPropTrunc)
(uᴰ .isTracked)
(vᴰ .isTracked)
dimI

isSetDisplayedUFamMap : ∀ {I J} (asmI : Assembly I) (asmJ : Assembly J) → ∀ u X Y → isSet (DisplayedUFamMap asmI asmJ u X Y)
fibrewiseMap (isSetDisplayedUFamMap {I} {J} asmI asmJ u X Y f g p q dimI dimJ) i x =
isSet→isSet'
(Y .assemblies (u .map i) .isSetX)
{a₀₀ = fibrewiseMap f i x}
{a₀₁ = fibrewiseMap f i x}
refl
{a₁₀ = fibrewiseMap g i x}
{a₁₁ = fibrewiseMap g i x}
refl
(λ dimK → fibrewiseMap (p dimK) i x)
(λ dimK → fibrewiseMap (q dimK) i x)
dimJ dimI
isTracked (isSetDisplayedUFamMap {I} {J} asmI asmJ u X Y f g p q dimI dimJ) =
isProp→SquareP
{B = λ dimI dimJ →
∃[ e ∈ A ]
((i : I) (a : A) →
a ⊩[ asmI ] i →
(x : X .carriers i) (b : A) →
b ⊩[ X .assemblies i ] x →
(e ⨾ a ⨾ b) ⊩[ Y .assemblies (u .map i) ]
isSet→isSet'
(Y .assemblies
(u .map i)
.isSetX)
(λ _ → fibrewiseMap f i x) (λ _ → fibrewiseMap g i x)
(λ dimK → fibrewiseMap (p dimK) i x)
(λ dimK → fibrewiseMap (q dimK) i x) dimJ dimI)}
(λ dimI dimJ → isPropPropTrunc)
{a = isTracked f}
{b = isTracked g}
{c = isTracked f}
{d = isTracked g}
refl
refl
(λ dimK → isTracked (p dimK))
(λ dimK → isTracked (q dimK))
dimI dimJ

open Categoryᴰ UNIMOD
DisplayedUFamMapPathPIso :
∀ {I J} (asmI : Assembly I) (asmJ : Assembly J) →
∀ u v X Y
→ (uᴰ : DisplayedUFamMap asmI asmJ u X Y)
→ (vᴰ : DisplayedUFamMap asmI asmJ v X Y)
→ (p : u ≡ v)
→ Iso
(∀ (i : I) (x : X .carriers i) → PathP (λ dimI → Y .carriers (p dimI .map i)) (uᴰ .fibrewiseMap i x) (vᴰ .fibrewiseMap i x))
(PathP (λ dimI → DisplayedUFamMap asmI asmJ (p dimI) X Y) uᴰ vᴰ)
Iso.fun (DisplayedUFamMapPathPIso {I} {J} asmI asmJ u v X Y uᴰ vᴰ p) pᴰ = DisplayedUFamMapPathP asmI asmJ u v X Y uᴰ vᴰ p pᴰ
Iso.inv (DisplayedUFamMapPathPIso {I} {J} asmI asmJ u v X Y uᴰ vᴰ p) uᴰ≡vᴰ i x dimI = (uᴰ≡vᴰ dimI) .fibrewiseMap i x
Iso.rightInv (DisplayedUFamMapPathPIso {I} {J} asmI asmJ u v X Y uᴰ vᴰ p) uᴰ≡vᴰ dimI dimJ =
isSet→SquareP
{A = λ dimK dimL → DisplayedUFamMap asmI asmJ (p dimL) X Y}
(λ dimI dimJ → isSetDisplayedUFamMap asmI asmJ (p dimJ) X Y)
{a₀₀ = uᴰ}
{a₀₁ = vᴰ}
(λ dimK → DisplayedUFamMapPathP asmI asmJ u v X Y uᴰ vᴰ p (λ i x dimL → uᴰ≡vᴰ dimL .fibrewiseMap i x) dimK)
{a₁₀ = uᴰ}
{a₁₁ = vᴰ}
uᴰ≡vᴰ
refl
refl dimI dimJ
Iso.leftInv (DisplayedUFamMapPathPIso {I} {J} asmI asmJ u v X Y uᴰ vᴰ p) pᴰ = refl

UniformFamily : {X : Type ℓ} → (asmX : Assembly X) → Type (ℓ-suc ℓ)
UniformFamily {X} asmX = UNIMOD .Categoryᴰ.ob[_] (X , asmX)
idDisplayedUFamMap : ∀ {I} (asmI : Assembly I) (p : UniformFamily asmI) → DisplayedUFamMap asmI asmI (identityMorphism asmI) p p
DisplayedUFamMap.fibrewiseMap (idDisplayedUFamMap {I} asmI p) i pi = pi
DisplayedUFamMap.isTracked (idDisplayedUFamMap {I} asmI p) =
return
(λ*2 realizer ,
λ i a a⊩i x b b⊩x →
subst
(λ r → r ⊩[ p .assemblies i ] x)
(sym (λ*2ComputationRule realizer a b))
b⊩x) where
realizer : Term as 2
realizer = # zero

module _
{I J K : Type ℓ}
(asmI : Assembly I)
(asmJ : Assembly J)
(asmK : Assembly K)
(f : AssemblyMorphism asmI asmJ)
(g : AssemblyMorphism asmJ asmK)
(X : UniformFamily asmI)
(Y : UniformFamily asmJ)
(Z : UniformFamily asmK)
(fᴰ : DisplayedUFamMap asmI asmJ f X Y)
(gᴰ : DisplayedUFamMap asmJ asmK g Y Z) where

composeDisplayedUFamMap : DisplayedUFamMap asmI asmK (f ⊚ g) X Z
DisplayedUFamMap.fibrewiseMap composeDisplayedUFamMap i Xi = gᴰ .fibrewiseMap (f .map i) (fᴰ .fibrewiseMap i Xi)
DisplayedUFamMap.isTracked composeDisplayedUFamMap =
do
(gᴰ~ , isTrackedGᴰ) ← gᴰ .isTracked
(fᴰ~ , isTrackedFᴰ) ← fᴰ .isTracked
(f~ , isTrackedF) ← f .tracker
let
realizer : Term as 2
realizer = ` gᴰ~ ̇ (` f~ ̇ # one) ̇ (` fᴰ~ ̇ # one ̇ # zero)
return
(λ*2 realizer ,
(λ i a a⊩i x b b⊩x →
subst
(_⊩[ Z .assemblies (g .map (f .map i)) ] _)
(sym (λ*2ComputationRule realizer a b))
(isTrackedGᴰ (f .map i) (f~ ⨾ a) (isTrackedF i a a⊩i) (fᴰ .fibrewiseMap i x) (fᴰ~ ⨾ a ⨾ b) (isTrackedFᴰ i a a⊩i x b b⊩x))))

UNIMOD : Categoryᴰ ASM (ℓ-suc ℓ) ℓ
Categoryᴰ.ob[ UNIMOD ] (I , asmI) = UniformFamily asmI
Categoryᴰ.Hom[_][_,_] UNIMOD {I , asmI} {J , asmJ} u X Y = DisplayedUFamMap asmI asmJ u X Y
Categoryᴰ.idᴰ UNIMOD {I , asmI} {X} = idDisplayedUFamMap asmI X
Categoryᴰ._⋆ᴰ_ UNIMOD {I , asmI} {J , asmJ} {K , asmK} {f} {g} {X} {Y} {Z} fᴰ gᴰ = composeDisplayedUFamMap asmI asmJ asmK f g X Y Z fᴰ gᴰ
Categoryᴰ.⋆IdLᴰ UNIMOD {I , asmI} {J , asmJ} {f} {X} {Y} fᴰ =
DisplayedUFamMapPathP
asmI asmJ
(identityMorphism asmI ⊚ f) f
X Y
(composeDisplayedUFamMap asmI asmI asmJ (Category.id ASM) f X X Y (idDisplayedUFamMap asmI X) fᴰ)
fᴰ
(Category.⋆IdL ASM f)
(λ i x → refl)
Categoryᴰ.⋆IdRᴰ UNIMOD {I , asmI} {J , asmJ} {f} {X} {Y} fᴰ =
DisplayedUFamMapPathP
asmI asmJ
(f ⊚ identityMorphism asmJ) f
X Y
(composeDisplayedUFamMap asmI asmJ asmJ f (Category.id ASM) X Y Y fᴰ (idDisplayedUFamMap asmJ Y))
fᴰ
(Category.⋆IdR ASM f)
λ i x → refl
Categoryᴰ.⋆Assocᴰ UNIMOD {I , asmI} {J , asmJ} {K , asmK} {L , asmL} {f} {g} {h} {X} {Y} {Z} {W} fᴰ gᴰ hᴰ =
DisplayedUFamMapPathP
asmI asmL
((f ⊚ g) ⊚ h) (f ⊚ (g ⊚ h))
X W
(composeDisplayedUFamMap
asmI asmK asmL
(f ⊚ g) h X Z W
(composeDisplayedUFamMap asmI asmJ asmK f g X Y Z fᴰ gᴰ)
hᴰ)
(composeDisplayedUFamMap
asmI asmJ asmL
f (g ⊚ h) X Y W
fᴰ (composeDisplayedUFamMap asmJ asmK asmL g h Y Z W gᴰ hᴰ))
(Category.⋆Assoc ASM f g h)
λ i x → refl
Categoryᴰ.isSetHomᴰ UNIMOD {I , asmI} {J , asmJ} {f} {X} {Y} = isSetDisplayedUFamMap asmI asmJ f X Y
7 changes: 4 additions & 3 deletions src/Realizability/PERs/PER.agda
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
open import Realizability.ApplicativeStructure
open import Realizability.CombinatoryAlgebra
open import Realizability.PropResizing
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure using (⟨_⟩; str)
Expand Down Expand Up @@ -70,8 +69,10 @@ isEquivTracker R S (a , _) (b , _) = (∀ r → r ~[ R ] r → (a ⨾ r) ~[ S ]

isEquivRelIsEquivTracker : (R S : PER) → BR.isEquivRel (isEquivTracker R S)
BinaryRelation.isEquivRel.reflexive (isEquivRelIsEquivTracker R S) (a , isTrackerA) r r~r = isTrackerA r r r~r
BinaryRelation.isEquivRel.symmetric (isEquivRelIsEquivTracker R S) (a , isTrackerA) (b , isTrackerB) a~b r r~r = isSymmetric S (a ⨾ r) (b ⨾ r) (a~b r r~r)
BinaryRelation.isEquivRel.transitive (isEquivRelIsEquivTracker R S) (a , isTrackerA) (b , isTrackerB) (c , isTrackerC) a~b b~c r r~r = isTransitive S (a ⨾ r) (b ⨾ r) (c ⨾ r) (a~b r r~r) (b~c r r~r)
BinaryRelation.isEquivRel.symmetric (isEquivRelIsEquivTracker R S) (a , isTrackerA) (b , isTrackerB) a~b r r~r =
isSymmetric S (a ⨾ r) (b ⨾ r) (a~b r r~r)
BinaryRelation.isEquivRel.transitive (isEquivRelIsEquivTracker R S) (a , isTrackerA) (b , isTrackerB) (c , isTrackerC) a~b b~c r r~r =
isTransitive S (a ⨾ r) (b ⨾ r) (c ⨾ r) (a~b r r~r) (b~c r r~r)

isPropIsEquivTracker : ∀ R S a b → isProp (isEquivTracker R S a b)
isPropIsEquivTracker R S (a , isTrackerA) (b , isTrackerB) = isPropΠ2 λ r r~r → isPropValued S (a ⨾ r) (b ⨾ r)
Expand Down
91 changes: 91 additions & 0 deletions src/Realizability/PERs/ResizedPER.agda
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,91 @@
open import Realizability.ApplicativeStructure
open import Realizability.CombinatoryAlgebra
open import Realizability.PropResizing
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure using (⟨_⟩; str)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Functions.FunExtEquiv
open import Cubical.Relation.Binary
open import Cubical.Data.Sigma
open import Cubical.Data.FinData
open import Cubical.Data.Vec
open import Cubical.Reflection.RecordEquiv
open import Cubical.HITs.PropositionalTruncation as PT hiding (map)
open import Cubical.HITs.PropositionalTruncation.Monad
open import Cubical.HITs.SetQuotients as SQ
open import Cubical.Categories.Category
open import Cubical.Categories.Functor hiding (Id)

module Realizability.PERs.ResizedPER
{ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) (resizing : hPropResizing ℓ) where

open import Realizability.Assembly.Base ca
open import Realizability.Assembly.Morphism ca
open import Realizability.PERs.PER ca

open CombinatoryAlgebra ca
open Combinators ca renaming (i to Id; ia≡a to Ida≡a)

smallHProp = resizing .fst
hProp≃smallHProp = resizing .snd
smallHProp≃hProp = invEquiv hProp≃smallHProp

hPropIsoSmallHProp : Iso (hProp ℓ) smallHProp
hPropIsoSmallHProp = equivToIso hProp≃smallHProp

shrink : hProp ℓ → smallHProp
shrink = Iso.fun hPropIsoSmallHProp

enlarge : smallHProp → hProp ℓ
enlarge = Iso.inv hPropIsoSmallHProp

enlarge⋆shrink≡id : section shrink enlarge
enlarge⋆shrink≡id = Iso.rightInv hPropIsoSmallHProp

shrink⋆enlarge≡id : retract shrink enlarge
shrink⋆enlarge≡id = Iso.leftInv hPropIsoSmallHProp

extractType : smallHProp → Type ℓ
extractType p = ⟨ enlarge p ⟩

extractFromShrunk : ∀ p isPropP → extractType (shrink (p , isPropP)) ≡ p
extractFromShrunk p isPropP =
extractType (shrink (p , isPropP))
≡⟨ refl ⟩
⟨ enlarge (shrink (p , isPropP)) ⟩
≡⟨ cong ⟨_⟩ (shrink⋆enlarge≡id (p , isPropP)) ⟩
p
∎

record ResizedPER : Type ℓ where
no-eta-equality
constructor makeResizedPER
field
relation : A → A → smallHProp
isSymmetric : ∀ a b → extractType (relation a b) → extractType (relation b a)
isTransitive : ∀ a b c → extractType (relation a b) → extractType (relation b c) → extractType (relation a c)

open ResizedPER

ResizedPERHAEquivPER : HAEquiv ResizedPER PER
PER.relation (fst ResizedPERHAEquivPER resized) =
(λ a b → extractType (resized .relation a b)) ,
λ a b → str (enlarge (resized .relation a b))
fst (PER.isPER (fst ResizedPERHAEquivPER resized)) a b a~b = resized .isSymmetric a b a~b
snd (PER.isPER (fst ResizedPERHAEquivPER resized)) a b c a~b b~c = resized .isTransitive a b c a~b b~c
relation (isHAEquiv.g (snd ResizedPERHAEquivPER) per) a b =
shrink ((per .PER.relation .fst a b) , (per .PER.relation .snd a b))
isSymmetric (isHAEquiv.g (snd ResizedPERHAEquivPER) per) a b a~b =
subst _ (sym (extractFromShrunk (per .PER.relation .fst b a) (per .PER.relation .snd b a))) {!per .PER.isPER .fst a b a~b!}
isTransitive (isHAEquiv.g (snd ResizedPERHAEquivPER) per) a b c a~b b~c = {!!}
isHAEquiv.linv (snd ResizedPERHAEquivPER) resized = {!!}
isHAEquiv.rinv (snd ResizedPERHAEquivPER) per = {!!}
isHAEquiv.com (snd ResizedPERHAEquivPER) resized = {!!}

ResizedPER≃PER : ResizedPER ≃ PER
ResizedPER≃PER = ResizedPERHAEquivPER .fst , isHAEquiv→isEquiv (ResizedPERHAEquivPER .snd)
6 changes: 6 additions & 0 deletions src/Realizability/PERs/SystemF.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,12 @@ module Syntax where
Ren* : TypeCtxt → TypeCtxt → Type
Ren* Γ Δ = ∀ {K} → K ∈* Γ → K ∈* Δ

lift* : ∀ {Γ Δ k} → Ren* Γ Δ → Ren* (Γ , k) (Δ , k)
lift* {Γ} {Δ} {k} ρ {.k} here = here
lift* {Γ} {Δ} {k} ρ {K} (there inm) = there (ρ inm)

ren* : ∀ {Γ Δ} →

data _∈_ : ∀ {Γ} → Tp Γ tp → TermCtxt Γ → Type where
here : ∀ {Γ} {A : Tp Γ tp} {Θ : TermCtxt Γ} → A ∈ (Θ , A)
thereType : ∀ {Γ} {A B : Tp Γ tp} {Θ : TermCtxt Γ} → A ∈ Θ → A ∈ (Θ , B)
Expand Down
Loading

0 comments on commit 73d04b5

Please sign in to comment.