Start working towards LCCC on Mod

src/Realizability/Assembly/Base.agda

@@ -13,6 +13,7 @@ open import Realizability.CombinatoryAlgebra
 
 module Realizability.Assembly.Base {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
   record Assembly (X : Type ℓ) : Type (ℓ-suc ℓ) where
+    constructor makeAssembly
     infix 25 _⊩_
     field
       _⊩_ : A → X → Type ℓ

src/Realizability/Assembly/Pullbacks.agda

@@ -0,0 +1,159 @@
+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
+
+module Realizability.Assembly.Pullbacks {ℓ} {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
+
+module _ (cspn : Cospan ASM) where
+  open Cospan cspn
+
+  X  = l .fst
+  xs = l .snd
+
+  Y  = m .fst
+  ys = m .snd
+
+  Z  = r .fst
+  zs = r .snd
+
+  f = s₁
+  g = s₂
+
+  opaque
+    pullbackType : Type ℓ
+    pullbackType = (Σ[ x ∈ X ] Σ[ z ∈ Z ] (f .map x ≡ g .map z))
+
+  opaque
+    unfolding pullbackType
+    pullbackAsm : Assembly pullbackType
+    Assembly._⊩_ pullbackAsm = λ { r (x , z , fx≡gz) → (pr₁ ⨾ r) ⊩[ xs ] x × ((pr₂ ⨾ r) ⊩[ zs ] z) }
+    Assembly.isSetX pullbackAsm = isSetΣ (xs .isSetX) (λ _ → isSetΣ (zs .isSetX) (λ _ → isProp→isSet (ys .isSetX _ _)))
+    Assembly.⊩isPropValued pullbackAsm = λ { r (x , z , fx≡gz) → isProp× (xs .⊩isPropValued _ _) (zs .⊩isPropValued _ _) }
+    Assembly.⊩surjective pullbackAsm =
+      (λ { (x , z , fx≡gz) →
+        do
+          (a , a⊩x) ← xs .⊩surjective x
+          (b , b⊩z) ← zs .⊩surjective z
+          return
+            (pair ⨾ a ⨾ b ,
+             subst (λ r' → r' ⊩[ xs ] x) (sym (pr₁pxy≡x _ _)) a⊩x ,
+             subst (λ r' → r' ⊩[ zs ] z) (sym (pr₂pxy≡y _ _)) b⊩z) })
+
+  opaque
+    unfolding pullbackType
+    unfolding pullbackAsm
+    pullbackPr₁ : AssemblyMorphism pullbackAsm xs
+    AssemblyMorphism.map pullbackPr₁ (x , z , fx≡gz) = x
+    AssemblyMorphism.tracker pullbackPr₁ =
+      return (pr₁ , (λ { (x , z , fx≡gz) r (pr₁r⊩x , pr₂r⊩z) → pr₁r⊩x }))
+
+  opaque
+    unfolding pullbackType
+    unfolding pullbackAsm
+    pullbackPr₂ : AssemblyMorphism pullbackAsm zs
+    AssemblyMorphism.map pullbackPr₂ (x , z , fx≡gz) = z
+    AssemblyMorphism.tracker pullbackPr₂ =
+      return (pr₂ , (λ { (x , z , fx≡gz) r (pr₁r⊩x , pr₂r⊩z) → pr₂r⊩z }))
+
+  opaque
+    unfolding pullbackAsm
+    unfolding pullbackPr₁
+    unfolding pullbackPr₂
+    pullback : Pullback ASM cspn
+    Pullback.pbOb pullback = pullbackType , pullbackAsm
+    Pullback.pbPr₁ pullback = pullbackPr₁
+    Pullback.pbPr₂ pullback = pullbackPr₂
+    Pullback.pbCommutes pullback = AssemblyMorphism≡ _ _ (funExt λ { (x , z , fx≡gz) → fx≡gz })
+    Pullback.univProp pullback {D , ds} p q pf≡qg =
+      uniqueExists
+        uniqueMorphism
+        ((AssemblyMorphism≡ _ _ (funExt (λ d → refl))) , (AssemblyMorphism≡ _ _ (funExt (λ d → refl))))
+        (λ !' → isProp× (isSetAssemblyMorphism _ _ p (!' ⊚ pullbackPr₁)) (isSetAssemblyMorphism _ _ q (!' ⊚ pullbackPr₂)))
+        λ { !' (p≡!'*pr₁ , q≡!'*pr₂) →
+          AssemblyMorphism≡
+            _ _
+            (funExt
+              λ d →
+                ΣPathP
+                  ((λ i → p≡!'*pr₁ i .map d) ,
+                    ΣPathPProp
+                      {u = q .map d , λ i → pf≡qg i .map d}
+                      {v = !' .map d .snd}
+                      (λ z → ys .isSetX _ _)
+                      λ i → q≡!'*pr₂ i .map d)) }
+        where
+        uniqueMap : D → pullbackType
+        uniqueMap d = p .map d , q .map d , λ i → pf≡qg i .map d
+
+        uniqueMorphism : AssemblyMorphism ds pullbackAsm
+        uniqueMorphism =
+          (makeAssemblyMorphism
+            uniqueMap
+            (do
+              (p~ , isTrackedP) ← p .tracker
+              (q~ , isTrackedQ) ← q .tracker
+              let
+                realizer : Term as 1
+                realizer = ` pair ̇ (` p~ ̇ # zero) ̇ (` q~ ̇ # zero)
+              return
+                (λ* realizer ,
+                 λ d r r⊩d →
+                   subst (λ r' → r' ⊩[ xs ] (p .map d)) (sym (cong (λ x → pr₁ ⨾ x) (λ*ComputationRule realizer r) ∙ pr₁pxy≡x _ _)) (isTrackedP d r r⊩d) ,
+                   subst (λ r' → r' ⊩[ zs ] (q .map d)) (sym (cong (λ x → pr₂ ⨾ x) (λ*ComputationRule realizer r) ∙ pr₂pxy≡y _ _)) (isTrackedQ d r r⊩d))))
+
+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 = {!!}

src/Realizability/Assembly/SetsReflectiveSubcategory.agda

@@ -0,0 +1,62 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Data.Sigma
+open import Cubical.Data.FinData
+open import Cubical.Data.Unit
+open import Cubical.HITs.PropositionalTruncation hiding (map)
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.Reflection.RecordEquiv
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Adjoint
+open import Cubical.Categories.NaturalTransformation
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
+
+module Realizability.Assembly.SetsReflectiveSubcategory {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+
+open import Realizability.Assembly.Base ca
+open import Realizability.Assembly.Morphism ca
+
+open Assembly
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
+
+forgetfulFunctor : Functor ASM (SET ℓ)
+Functor.F-ob forgetfulFunctor (X , asmX) = X , asmX .isSetX
+Functor.F-hom forgetfulFunctor {X , asmX} {Y , asmY} f = f .map
+Functor.F-id forgetfulFunctor = refl
+Functor.F-seq forgetfulFunctor {X , asmX} {Y , asmY} {Z , asmZ} f g = refl
+
+∇ : Functor (SET ℓ) ASM
+Functor.F-ob ∇ (X , isSetX) = X , makeAssembly (λ a x → Unit*) isSetX (λ _ _ → isPropUnit*) λ x → ∣ k , tt* ∣₁
+Functor.F-hom ∇ {X , isSetX} {Y , isSetY} f = makeAssemblyMorphism f (return (k , (λ _ _ _ → tt*)))
+Functor.F-id ∇ {X , isSetX} = AssemblyMorphism≡ _ _ refl
+Functor.F-seq ∇ {X , isSetX} {Y , isSetY} {Z , isSetZ} f g = AssemblyMorphism≡ _ _ refl
+
+module _ where
+  open UnitCounit
+
+  adjointUnitCounit : forgetfulFunctor ⊣ ∇
+  NatTrans.N-ob (_⊣_.η adjointUnitCounit) (X , asmX) = makeAssemblyMorphism (λ x → x) (return (k , (λ _ _ _ → tt*)))
+  NatTrans.N-hom (_⊣_.η adjointUnitCounit) {X , asmX} {Y , asmY} f = AssemblyMorphism≡ _ _ refl
+  NatTrans.N-ob (_⊣_.ε adjointUnitCounit) (X , isSetX) x = x
+  NatTrans.N-hom (_⊣_.ε adjointUnitCounit) {X , isSetX} {Y , isSetY} f = refl
+  TriangleIdentities.Δ₁ (_⊣_.triangleIdentities adjointUnitCounit) (X , asmX) = refl
+  TriangleIdentities.Δ₂ (_⊣_.triangleIdentities adjointUnitCounit) (X , isSetX) = AssemblyMorphism≡ _ _ refl
+
+module _ where
+  open NaturalBijection
+
+  adjointNaturalBijection : forgetfulFunctor ⊣ ∇
+  Iso.fun (_⊣_.adjIso adjointNaturalBijection) f = makeAssemblyMorphism f (return (k , (λ x r r⊩x → tt*)))
+  Iso.inv (_⊣_.adjIso adjointNaturalBijection) f = f .map
+  Iso.rightInv (_⊣_.adjIso adjointNaturalBijection) b = AssemblyMorphism≡ _ _ refl
+  Iso.leftInv (_⊣_.adjIso adjointNaturalBijection) a = refl
+  _⊣_.adjNatInD adjointNaturalBijection {X , isSetX} {Y , isSetY} f g = AssemblyMorphism≡ _ _ refl
+  _⊣_.adjNatInC adjointNaturalBijection {X , asmX} {Y , asmY} f g = refl
+

src/Realizability/Assembly/Terminal.agda

@@ -0,0 +1,49 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Sigma
+open import Cubical.Data.FinData
+open import Cubical.Data.Unit
+open import Cubical.HITs.PropositionalTruncation hiding (map)
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.Categories.Limits.Terminal
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
+
+module Realizability.Assembly.Terminal {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A)  where
+
+open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
+open import Realizability.Assembly.Base ca
+open import Realizability.Assembly.Morphism ca
+open CombinatoryAlgebra ca
+open Assembly
+open AssemblyMorphism
+
+terminalAsm : Assembly Unit*
+(Assembly._⊩_ terminalAsm) a tt* = Unit*
+Assembly.isSetX terminalAsm = isSetUnit*
+(Assembly.⊩isPropValued terminalAsm) a tt* = isPropUnit*
+Assembly.⊩surjective terminalAsm tt* = ∣ k , tt* ∣₁
+
+isTerminalTerminalAsm : isTerminal ASM (Unit* , terminalAsm)
+isTerminalTerminalAsm (X , asmX) =
+  inhProp→isContr
+    (makeAssemblyMorphism
+      (λ x → tt*)
+      (return
+        (k , (λ x r r⊩x → tt*))))
+    (λ f g →
+      AssemblyMorphism≡ _ _ (funExt λ x → refl))
+
+TerminalASM : Terminal ASM
+fst TerminalASM = Unit* , terminalAsm
+snd TerminalASM = isTerminalTerminalAsm
+
+-- global element
+module _ {X : Type ℓ} (asmX : Assembly X) (x : X) (r : A) (r⊩x : r ⊩[ asmX ] x) where
+
+  globalElement : AssemblyMorphism terminalAsm asmX
+  AssemblyMorphism.map globalElement tt* = x
+  AssemblyMorphism.tracker globalElement =
+    return
+      ((k ⨾ r) ,
+      (λ { tt* a tt* → subst (λ r' → r' ⊩[ asmX ] x) (sym (kab≡a _ _)) r⊩x }))

src/Realizability/Modest/Base.agda

@@ -0,0 +1,78 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Powerset
+open import Cubical.Foundations.Structure using (⟨_⟩; str)
+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.Reflection.RecordEquiv
+open import Cubical.Categories.Category
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
+open import Realizability.PropResizing
+
+module Realizability.Modest.Base {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A)  where
+
+open import Realizability.Assembly.Base ca
+open import Realizability.Assembly.Morphism ca
+
+open Assembly
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
+
+module _ {X : Type ℓ} (asmX : Assembly X) where
+
+  isModest : Type _
+  isModest = ∀ (x y : X) (a : A) → a ⊩[ asmX ] x → a ⊩[ asmX ] y → x ≡ y
+
+  isPropIsModest : isProp isModest
+  isPropIsModest = isPropΠ3 λ x y a → isProp→ (isProp→ (asmX .isSetX x y))
+
+  isUniqueRealised : isModest → ∀ (a : A) → isProp (Σ[ x ∈ X ] (a ⊩[ asmX ] x))
+  isUniqueRealised isMod a (x , a⊩x) (y , a⊩y) = Σ≡Prop (λ x' → asmX .⊩isPropValued a x') (isMod x y a a⊩x a⊩y)
+
+ModestSet : Type ℓ → Type (ℓ-suc ℓ)
+ModestSet X = Σ[ xs ∈ Assembly X ] isModest xs
+
+MOD : Category (ℓ-suc ℓ) ℓ
+MOD = ΣPropCat ASM λ { (X , asmX) → (Lift (isModest asmX)) , (isOfHLevelRespectEquiv 1 (LiftEquiv {A = isModest asmX}) (isPropIsModest asmX)) }
+
+-- Every modest set is isomorphic to a canonically modest set
+module Canonical (X : Type ℓ) (asmX : Assembly X) (isModestAsmX : isModest asmX) (resizing : hPropResizing ℓ) where
+  open ResizedPowerset resizing
+  -- Replace every term of X by it's set of realisers
+  realisersOf : X → ℙ A
+  realisersOf x a = (a ⊩[ asmX ] x) , (asmX .⊩isPropValued a x)
+
+  resizedRealisersOf : X → 𝓟 A
+  resizedRealisersOf x = ℙ→𝓟 A (realisersOf x)
+
+  realiserSet : Type ℓ
+  realiserSet = Σ[ P ∈ 𝓟 A ] ∃[ x ∈ X ] P ≡ resizedRealisersOf x
+
+  canonicalModestSet : Assembly realiserSet
+  Assembly._⊩_ canonicalModestSet r (P , ∃x) = r ϵ P
+  Assembly.isSetX canonicalModestSet = isSetΣ (isSet𝓟 A) (λ P → isProp→isSet isPropPropTrunc)
+  Assembly.⊩isPropValued canonicalModestSet r (P , ∃x) = isPropϵ r P
+  Assembly.⊩surjective canonicalModestSet (P , ∃x) =
+    do
+      (x , P≡⊩x) ← ∃x
+      (a , a⊩x) ← asmX .⊩surjective x
+      return
+        (a ,
+        (subst
+          (λ P → a ϵ P)
+          (sym P≡⊩x)
+          (subst (λ P → a ∈ P) (sym (compIsIdFunc (realisersOf x))) a⊩x)))
+  {-
+  isModestCanonicalModestSet : isModest canonicalModestSet
+  isModestCanonicalModestSet x y a a⊩x a⊩y =
+    Σ≡Prop
+      (λ _ → isPropPropTrunc)
+      (𝓟≡ (x .fst) (y .fst) (⊆-extensionality (𝓟→ℙ A (x .fst)) (𝓟→ℙ A (y .fst)) ((λ b b⊩x → {!!}) , {!!}))) -}
+
+