-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Subquotient and Canonical PER Operations
- Loading branch information
Showing
4 changed files
with
216 additions
and
65 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
79 changes: 79 additions & 0 deletions
79
src/Realizability/Modest/SubQuotientCanonicalPERToOriginal.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,79 @@ | ||
| 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.Path | ||
| open import Cubical.Foundations.Structure using (⟨_⟩; str) | ||
| open import Cubical.Data.Sigma | ||
| open import Cubical.Data.FinData | ||
| open import Cubical.Data.Unit | ||
| 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.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 hiding (Id) | ||
| open import Cubical.Categories.Constructions.Slice | ||
| open import Categories.CartesianMorphism | ||
| open import Categories.GenericObject | ||
| open import Realizability.CombinatoryAlgebra | ||
| open import Realizability.ApplicativeStructure | ||
| open import Realizability.PropResizing | ||
|
|
||
| module Realizability.Modest.SubQuotientCanonicalPERToOriginal {ℓ} {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.SetsReflectiveSubcategory ca | ||
| open import Realizability.Modest.Base ca | ||
| open import Realizability.Modest.UniformFamily ca | ||
| open import Realizability.Modest.CanonicalPER ca | ||
| open import Realizability.PERs.PER ca | ||
| open import Realizability.PERs.SubQuotient ca | ||
|
|
||
| open Assembly | ||
| open CombinatoryAlgebra ca | ||
| open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) | ||
| open Contravariant UNIMOD | ||
| open UniformFamily | ||
| open DisplayedUFamMap | ||
|
|
||
| module | ||
| _ {X : Type ℓ} | ||
| (asmX : Assembly X) | ||
| (isModestAsmX : isModest asmX) where | ||
|
|
||
| theCanonicalPER : PER | ||
| theCanonicalPER = canonicalPER asmX isModestAsmX | ||
|
|
||
| theSubQuotient : Assembly (subQuotient theCanonicalPER) | ||
| theSubQuotient = subQuotientAssembly theCanonicalPER | ||
|
|
||
| invert : AssemblyMorphism theSubQuotient asmX | ||
| AssemblyMorphism.map invert sq = SQ.rec (asmX .isSetX) mainMap mainMapCoh sq where | ||
|
|
||
| mainMap : Σ[ a ∈ A ] (theCanonicalPER .PER.relation a a) → X | ||
| mainMap (a , a~a) = PT.rec→Set (asmX .isSetX) action 2ConstantAction a~a where | ||
| action : Σ[ x ∈ X ] ((a ⊩[ asmX ] x) × (a ⊩[ asmX ] x)) → X | ||
| action (x , _ , _) = x | ||
|
|
||
| 2ConstantAction : 2-Constant action | ||
| 2ConstantAction (x , a⊩x , _) (x' , a⊩x' , _) = isModestAsmX x x' a a⊩x a⊩x' | ||
|
|
||
| mainMapCoh : ∀ a b a~b → mainMap a ≡ mainMap b | ||
| mainMapCoh (a , a~a) (b , b~b) a~b = | ||
| PT.elim3 | ||
| {P = λ a~a b~b a~b → mainMap (a , a~a) ≡ mainMap (b , b~b)} | ||
| (λ _ _ _ → asmX .isSetX _ _) | ||
| (λ { (x , a⊩x , _) (x' , b⊩x' , _) (x'' , a⊩x'' , b⊩x'') → | ||
| {!isModestAsmX x x' !} }) | ||
| a~a | ||
| b~b | ||
| a~b | ||
| AssemblyMorphism.tracker invert = {!!} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,88 @@ | ||
| 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.Path | ||
| open import Cubical.Foundations.Structure using (⟨_⟩; str) | ||
| open import Cubical.Data.Sigma | ||
| open import Cubical.Data.FinData | ||
| open import Cubical.Data.Unit | ||
| 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.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 hiding (Id) | ||
| open import Cubical.Categories.Constructions.Slice | ||
| open import Categories.CartesianMorphism | ||
| open import Categories.GenericObject | ||
| open import Realizability.CombinatoryAlgebra | ||
| open import Realizability.ApplicativeStructure | ||
| open import Realizability.PropResizing | ||
|
|
||
| module Realizability.Modest.UnresizedGeneric {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) (resizing : hPropResizing ℓ) where | ||
|
|
||
| open import Realizability.Assembly.Base ca | ||
| open import Realizability.Assembly.Morphism ca | ||
| open import Realizability.Assembly.Terminal ca | ||
| open import Realizability.Assembly.SetsReflectiveSubcategory ca | ||
| open import Realizability.Modest.Base ca | ||
| open import Realizability.Modest.UniformFamily ca | ||
| open import Realizability.Modest.CanonicalPER ca | ||
| open import Realizability.PERs.PER ca | ||
| open import Realizability.PERs.ResizedPER ca resizing | ||
| open import Realizability.PERs.SubQuotient ca | ||
|
|
||
| open Assembly | ||
| open CombinatoryAlgebra ca | ||
| open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) | ||
| open Contravariant UNIMOD | ||
| open UniformFamily | ||
| open DisplayedUFamMap | ||
|
|
||
| module Unresized | ||
| {X : Type ℓ} | ||
| (asmX : Assembly X) | ||
| (M : UniformFamily asmX) where | ||
|
|
||
| theCanonicalPER : ∀ x → PER | ||
| theCanonicalPER x = canonicalPER (M . assemblies x) (M .isModestFamily x) | ||
|
|
||
| elimRealizerForMx : ∀ {x : X} {Mx : M .carriers x} → Σ[ a ∈ A ] (a ⊩[ M .assemblies x ] Mx) → subQuotient (canonicalPER (M .assemblies x) (M .isModestFamily x)) | ||
| elimRealizerForMx {x} {Mx} (a , a⊩Mx) = [ a , (return (Mx , a⊩Mx , a⊩Mx)) ] | ||
|
|
||
| elimRealizerForMx2Constant : ∀ {x Mx} → 2-Constant (elimRealizerForMx {x} {Mx}) | ||
| elimRealizerForMx2Constant {x} {Mx} (a , a⊩Mx) (b , b⊩Mx) = | ||
| eq/ | ||
| (a , (return (Mx , a⊩Mx , a⊩Mx))) | ||
| (b , return (Mx , b⊩Mx , b⊩Mx)) | ||
| (return (Mx , a⊩Mx , b⊩Mx)) | ||
|
|
||
| mainMap : (x : X) (Mx : M .carriers x) → subQuotient (canonicalPER (M .assemblies x) (M .isModestFamily x)) | ||
| mainMap x Mx = | ||
| PT.rec→Set | ||
| squash/ | ||
| (elimRealizerForMx {x = x} {Mx = Mx}) | ||
| (elimRealizerForMx2Constant {x = x} {Mx = Mx}) | ||
| (M .assemblies x .⊩surjective Mx) | ||
|
|
||
| opaque | ||
| isTrackedMainMap : ∃[ r ∈ A ] (∀ (x : X) (a : A) → a ⊩[ asmX ] x → (Mx : M .carriers x) → (b : A) → b ⊩[ M .assemblies x ] Mx → (r ⨾ a ⨾ b) ⊩[ subQuotientAssembly (theCanonicalPER x) ] (mainMap x Mx)) | ||
| isTrackedMainMap = | ||
| return | ||
| ((λ*2 (# zero)) , | ||
| (λ x a a⊩x Mx b b⊩Mx → | ||
| PT.elim | ||
| {P = λ MxRealizer → (λ*2 (# zero) ⨾ a ⨾ b) ⊩[ subQuotientAssembly (theCanonicalPER x) ] (PT.rec→Set squash/ (elimRealizerForMx {x = x} {Mx = Mx}) (elimRealizerForMx2Constant {x = x} {Mx = Mx}) MxRealizer)} | ||
| (λ ⊩Mx → subQuotientAssembly (theCanonicalPER x) .⊩isPropValued (λ*2 (# zero) ⨾ a ⨾ b) (rec→Set squash/ elimRealizerForMx elimRealizerForMx2Constant ⊩Mx)) | ||
| (λ { (c , c⊩Mx) → | ||
| subst | ||
| (_⊩[ subQuotientAssembly (theCanonicalPER x) ] (elimRealizerForMx (c , c⊩Mx))) | ||
| (sym (λ*2ComputationRule (# zero) a b)) | ||
| (return (Mx , b⊩Mx , c⊩Mx))}) | ||
| (M .assemblies x .⊩surjective Mx))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters