Merge pull request #23 from rahulc29/polymorphism

Render changes

src/Realizability/Assembly/Exponentials.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical --allow-unsolved-metas #-}
+{-# OPTIONS --cubical #-}
 open import Cubical.Foundations.Prelude
 open import Cubical.Data.Sigma
 open import Cubical.Data.FinData hiding (eq)
@@ -22,7 +22,6 @@ _⇒_ : {A B : Type ℓ} → (as : Assembly A) → (bs : Assembly B) → Assembl
 _⇒_ {A} {B} as bs .⊩isPropValued r f = isPropTracks {X = A} {Y = B} {xs = as} {ys = bs}  r (f .map)
 (as ⇒ bs) .⊩surjective f = f .tracker
 
--- What a distinguished gentleman
 eval : {X Y : Type ℓ} → (xs : Assembly X) → (ys : Assembly Y) → AssemblyMorphism ((xs ⇒ ys) ⊗ xs) ys
 eval xs ys .map (f , x) = f .map x
 eval {X} {Y} xs ys .tracker =

src/Realizability/Modest/Base.agda

@@ -27,13 +27,13 @@ open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a t
 module _ {X : Type ℓ} (asmX : Assembly X) where
 
   isModest : Type _
-  isModest = ∀ (x y : X) (a : A) → a ⊩[ asmX ] x → a ⊩[ asmX ] y → x ≡ y
+  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))
+  isPropIsModest = isPropΠ2 λ x y → isProp→ (asmX .isSetX x y)
 
   isUniqueRealized : isModest → ∀ (a : A) → isProp (Σ[ x ∈ X ] (a ⊩[ asmX ] x))
-  isUniqueRealized isMod a (x , a⊩x) (y , a⊩y) = Σ≡Prop (λ x' → asmX .⊩isPropValued a x') (isMod x y a a⊩x a⊩y)
+  isUniqueRealized 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

src/Realizability/Modest/CanonicalPER.agda

@@ -53,13 +53,7 @@ module _
   PER.isPropValued canonicalPER a b (x , a⊩x , b⊩x) (x' , a⊩x' , b⊩x') =
     Σ≡Prop
       (λ x → isProp× (asmX .⊩isPropValued a x) (asmX .⊩isPropValued b x))
-      (isModestAsmX x x' a a⊩x a⊩x')
+      (isModestAsmX x x' ∣ a , a⊩x , a⊩x' ∣₁)
   fst (PER.isPER canonicalPER) a b (x , a⊩x , b⊩x) = x , b⊩x , a⊩x
   snd (PER.isPER canonicalPER) a b c (x , a⊩x , b⊩x) (x' , b⊩x' , c⊩x') =
-    x' , subst (a ⊩[ asmX ]_) (isModestAsmX x x' b b⊩x b⊩x') a⊩x , c⊩x'
-
-CanonicalPERFunctor : Functor MOD PERCat
-Functor.F-ob CanonicalPERFunctor (X , asmX , isModestAsmX) = canonicalPER asmX isModestAsmX
-Functor.F-hom CanonicalPERFunctor {X , asmX , isModestAsmX} {Y , asmY , isModestAsmY} f = {!!}
-Functor.F-id CanonicalPERFunctor = {!!}
-Functor.F-seq CanonicalPERFunctor = {!!}
+    x' , subst (a ⊩[ asmX ]_) (isModestAsmX x x' ∣ b , b⊩x , b⊩x' ∣₁) a⊩x , c⊩x'

src/Realizability/Modest/PartialSurjection.agda

@@ -132,15 +132,19 @@ module ModestSetIso (X : Type ℓ) (isCorrectHLevel : isSet X) where
     do
       ((a , s) , ≡x) ← surj .isSurjectionEnumeration x
       return (a , (s , ≡x))
-  snd (PartialSurjection→ModestSet surj) x y r (s , ≡x) (t , ≡x') =
-    x
-      ≡⟨ sym ≡x ⟩
-    surj .enumeration (r , s)
-      ≡⟨ cong (λ s → surj .enumeration (r , s)) (surj .isPropSupport r s t) ⟩
-    surj .enumeration (r , t)
-      ≡⟨ ≡x' ⟩
-    y
-      ∎
+  snd (PartialSurjection→ModestSet surj) x y ∃a =
+    PT.elim
+      (λ _ → surj .isSetX x y)
+      (λ { (r , (s , ≡x) , (t , ≡y)) →
+        x
+          ≡⟨ sym ≡x ⟩
+        surj .enumeration (r , s)
+          ≡⟨ cong (λ s → surj .enumeration (r , s)) (surj .isPropSupport r s t) ⟩
+        surj .enumeration (r , t)
+          ≡⟨ ≡y ⟩
+        y
+          ∎ })
+      ∃a
 
   opaque
     rightInv : ∀ surj → ModestSet→PartialSurjection (PartialSurjection→ModestSet surj) ≡ surj

src/Realizability/Modest/SubQuotientCanonicalPERIso.agda

@@ -69,9 +69,9 @@ module
     reprActionCoh : ∀ a b a~b → reprAction a ≡ reprAction b
     reprActionCoh (a , x , a⊩x , _) (b , x' , b⊩x' , _) (x'' , a⊩x'' , b⊩x'') =
       x
-        ≡⟨ isModestAsmX x x'' a a⊩x a⊩x'' ⟩
+        ≡⟨ isModestAsmX x x'' ∣ a , a⊩x , a⊩x'' ∣₁ ⟩
       x''
-        ≡⟨ isModestAsmX x'' x' b b⊩x'' b⊩x' ⟩
+        ≡⟨ isModestAsmX x'' x' ∣ b , b⊩x'' , b⊩x' ∣₁ ⟩
       x'
         ∎
   AssemblyMorphism.tracker invert = return (Id , (λ sq a a⊩sq → goal sq a a⊩sq)) where
@@ -90,7 +90,7 @@ module
       isPropMotive sq = isPropΠ2 λ a a⊩sq → asmX .⊩isPropValued _ _
 
       elemMotive : (x : domain theCanonicalPER) → motive [ x ]
-      elemMotive (r , x , r⊩x , _) a (x' , a⊩x' , r⊩x') = subst (a ⊩[ asmX ]_) (isModestAsmX x' x r r⊩x' r⊩x) a⊩x'
+      elemMotive (r , x , r⊩x , _) a (x' , a⊩x' , r⊩x') = subst (a ⊩[ asmX ]_) (isModestAsmX x' x ∣ r , r⊩x' , r⊩x ∣₁) a⊩x'
 
     goal : (sq : subQuotient theCanonicalPER) → (a : A) → a ⊩[ theSubQuotient ] sq → (Id ⨾ a) ⊩[ asmX ] (invert .map sq)
     goal sq a a⊩sq = subst (_⊩[ asmX ] _) (sym (Ida≡a a)) (realizability sq a a⊩sq)

src/Realizability/PERs/SubQuotient.agda

@@ -73,21 +73,25 @@ module _
       (λ [a] → isPropPropTrunc)
       (λ { (a , a~a) → return (a , a~a) })
       [a]
-      
+
   isModestSubQuotientAssembly : isModest subQuotientAssembly
-  isModestSubQuotientAssembly x y a a⊩x a⊩y =
-    SQ.elimProp2
-      {P = λ x y → motive x y}
-      isPropMotive
-      (λ { (x , x~x) (y , y~y) a a~x a~y →
-        eq/ (x , x~x) (y , y~y) (PER.isTransitive per x a y (PER.isSymmetric per a x a~x) a~y) })
-      x y
-      a a⊩x a⊩y where
+  isModestSubQuotientAssembly x y ∃a =
+    PT.elim
+      (λ _ → squash/ x y)
+      (λ { (a , a⊩x , a⊩y) →
+        SQ.elimProp2
+          {P = motive}
+          isPropMotive
+          (λ { (x , x~x) (y , y~y) a a~x a~y →
+            eq/ (x , x~x) (y , y~y) (PER.isTransitive per x a y (PER.isSymmetric per a x a~x) a~y) })
+          x y a a⊩x a⊩y })
+      ∃a where
         motive : ∀ (x y : subQuotient) → Type ℓ
         motive x y = ∀ (a : A) (a⊩x : a ⊩[ subQuotientAssembly ] x) (a⊩y : a ⊩[ subQuotientAssembly ] y) → x ≡ y
 
         isPropMotive : ∀ x y → isProp (motive x y)
         isPropMotive x y = isPropΠ3 λ _ _ _ → squash/ x y
+
 
 module _ (R S : PER) (f : perMorphism R S) where
 

src/Realizability/Topos/Equalizer.agda

@@ -19,21 +19,11 @@ More formally, we can show that ∃[ ob ∈ RTObject ] ∃[ eq ∈ RTMorphism ob
 To do this, we firstly show the universal property for the case when we have already been given the
 representatives.
 
-Since we are eliminating a set quotient into a proposition, we can choose any representatives.
-
-Thus we have shown that RT merely has equalisers.
-
-The idea of showing the mere existence of equalisers was suggested by Jon Sterling.
+It is possible to define things differently and quotient predicates by realizable equivalence but that causes type-checking time
+to explode, so we do not do that here.
 
 See also : Remark 2.7 of "Tripos Theory" by JHP
 
-──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
-
-An extra note worth adding is that the code is quite difficult to read and very ugly. This is mostly due to the fact that a lot
-of the things that are "implicit" in an informal setting need to be justified here. More so than usual.
-
-There is additional bureacracy because we have to deal with eliminators of set quotients. This makes things a little more complicated.
-
 -}
 open import Realizability.ApplicativeStructure renaming (Term to ApplStrTerm)
 open import Realizability.CombinatoryAlgebra

src/Realizability/Topos/SubobjectClassifier.agda

@@ -238,6 +238,8 @@ Predicate.isPropValued truePredicate tt* r = isPropUnit*
 ⊤ = fromPredicate truePredicate
 
 -- The subobject classifier classifies subobjects represented by strict relations
+-- Since every subobject is isomorphic to one represented by a strict relation
+-- this is enough to establish that true : 1 → Ω is a subobject classifier
 module ClassifiesStrictRelations
   (X : Type ℓ)
   (perX : PartialEquivalenceRelation X)