Archive commit

src/Experiments/Counterexample.agda

@@ -0,0 +1,10 @@
+module Experiments.Counterexample where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.HITs.SetQuotients as SQ
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.IsEven
+open import Cubical.Data.Sigma
+open import Cubical.Data.Bool
+open import Cubical.Data.Sum as Sum
+

src/Realizability/Topos/FunctionalRelation.agda

@@ -4,14 +4,15 @@ open import Realizability.CombinatoryAlgebra
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Univalence
 open import Cubical.Data.Vec
 open import Cubical.Data.Nat
 open import Cubical.Data.FinData
 open import Cubical.Data.Fin hiding (Fin; _/_)
 open import Cubical.Data.Sigma
 open import Cubical.Data.Empty
 open import Cubical.Data.Unit
-open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation as PT
 open import Cubical.HITs.PropositionalTruncation.Monad
 open import Cubical.HITs.SetQuotients as SQ
 open import Cubical.Categories.Category
@@ -23,8 +24,9 @@ module Realizability.Topos.FunctionalRelation
   (isNonTrivial : CombinatoryAlgebra.s ca ≡ CombinatoryAlgebra.k ca → ⊥)
   where
 
+open import Realizability.Tripos.Prealgebra.Predicate ca as Pred hiding (Predicate)
 open import Realizability.Tripos.Algebra.Base {ℓ' = ℓ'} {ℓ'' = ℓ''} ca renaming (AlgebraicPredicate to Predicate)
-open import Realizability.Topos.Object {ℓ = ℓ} {ℓ' = ℓ'} {ℓ'' = ℓ''} ca isNonTrivial 
+open import Realizability.Topos.Object {ℓ = ℓ} {ℓ' = ℓ'} {ℓ'' = ℓ''} ca isNonTrivial
 
 open CombinatoryAlgebra ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
@@ -66,10 +68,95 @@ opaque
              (λ r' → r' ⊩[ perX .equality ] (x , x))
              (sym (λ*ComputationRule prover (r ∷ [])))
              (ts⊩isTransitive x x' x r (sm ⨾ r) r⊩x~x' (sm⊩isSymmetric x x' r r⊩x~x')))
-  isStrictCodomain (idFuncRel {X} perX) = {!!}
-  isExtensional (idFuncRel {X} perX) = {!!}
-  isSingleValued (idFuncRel {X} perX) = {!!}
-  isTotal (idFuncRel {X} perX) = {!!}
+  isStrictCodomain (idFuncRel {X} perX) =
+    do
+      (sm , sm⊩isSymmetric) ← perX .isSymmetric
+      (ts , ts⊩isTransitive) ← perX .isTransitive
+      let
+        prover : ApplStrTerm as 1
+        prover = ` ts ̇ (` sm ̇ # fzero) ̇ # fzero
+      return
+        ((λ* prover) ,
+         (λ x x' r r⊩x~x' → subst (λ r' → r' ⊩[ perX .equality ] (x' , x')) (sym (λ*ComputationRule prover (r ∷ []))) (ts⊩isTransitive x' x x' (sm ⨾ r) r (sm⊩isSymmetric x x' r r⊩x~x') r⊩x~x')))
+  isExtensional (idFuncRel {X} perX) =
+    do
+      (sm , sm⊩isSymmetric) ← perX .isSymmetric
+      (ts , ts⊩isTransitive) ← perX .isTransitive
+      let
+        prover : ApplStrTerm as 3
+        prover = ` ts ̇ (` ts ̇ (` sm ̇ # 0) ̇ # 2) ̇ # 1
+      return
+        (λ* prover ,
+        (λ x₁ x₂ x₃ x₄ r s p r⊩x₁~x₂ s⊩x₃~x₄ p⊩x₁~x₃ →
+          subst
+            (λ r' → r' ⊩[ perX .equality ] (x₂ , x₄))
+            (sym (λ*ComputationRule prover (r ∷ s ∷ p ∷ [])))
+            (ts⊩isTransitive
+              x₂ x₃ x₄
+              (ts ⨾ (sm ⨾ r) ⨾ p)
+              s
+              (ts⊩isTransitive
+                x₂ x₁ x₃
+                (sm ⨾ r) p
+                (sm⊩isSymmetric x₁ x₂ r r⊩x₁~x₂)
+              p⊩x₁~x₃) s⊩x₃~x₄)))
+  isSingleValued (idFuncRel {X} perX) =
+    do
+      (sm , sm⊩isSymmetric) ← perX .isSymmetric
+      (ts , ts⊩isTransitive) ← perX .isTransitive
+      let
+        prover : ApplStrTerm as 2
+        prover = ` ts ̇ (` sm ̇ # 0) ̇ # 1
+      return (λ* prover , (λ x x' x'' r s r⊩x~x' s⊩x~x'' → subst (λ r' → r' ⊩[ perX .equality ] (x' , x'')) (sym (λ*ComputationRule prover (r ∷ s ∷ []))) (ts⊩isTransitive x' x x'' (sm ⨾ r) s (sm⊩isSymmetric x x' r r⊩x~x') s⊩x~x'')))
+  isTotal (idFuncRel {X} perX) =
+    do
+      (sm , sm⊩isSymmetric) ← perX .isSymmetric
+      (ts , ts⊩isTransitive) ← perX .isTransitive
+      return (Id , (λ x x' r r⊩x~x' → ∣ x' , (subst (λ r' → r' ⊩[ perX .equality ] (x , x')) (sym (Ida≡a _)) r⊩x~x') ∣₁))
+
+opaque
+  unfolding _⊩[_]_
+  composeFuncRel :
+    ∀ {X Y Z : Type ℓ'}
+    → (perX : PartialEquivalenceRelation X)
+    → (perY : PartialEquivalenceRelation Y)
+    → (perZ : PartialEquivalenceRelation Z)
+    → FunctionalRelation perX perY
+    → FunctionalRelation perY perZ
+    → FunctionalRelation perX perZ
+  relation (composeFuncRel {X} {Y} {Z} perX perY perZ F G) =
+    [ record
+        { isSetX = isSet× (perX .isSetX) (perZ .isSetX)
+        ; ∣_∣ = λ { (x , z) r → ∃[ y ∈ Y ] (pr₁ ⨾ r) ⊩[ F .relation ] (x , y) × (pr₂ ⨾ r) ⊩[ G .relation ] (y , z) }
+        ; isPropValued = λ { (x , z) r → isPropPropTrunc } } ]
+  isStrictDomain (composeFuncRel {X} {Y} {Z} perX perY perZ F G) =
+    do
+      (stF , stF⊩isStrictF) ← F .isStrictDomain
+      return
+        (Id ,
+        (λ x z r r⊩∃y →
+          transport
+            (propTruncIdempotent (isProp⊩ _ (perX .equality) (x , x)))
+            (do
+              (s , sr⊩) ← r⊩∃y
+              (y , pr₁sr⊩Fxy , pr₂sr⊩Gyz) ← sr⊩
+              (eqX , [eqX]≡perX) ← []surjective (perX .equality)
+              return
+                (subst
+                  (λ per → (Id ⨾ r) ⊩[ per ] (x , x))
+                  [eqX]≡perX
+                  (transformRealizes (Id ⨾ r) eqX (x , x) {!!})))))
+  isStrictCodomain (composeFuncRel {X} {Y} {Z} perX perY perZ F G) = {!!}
+  isExtensional (composeFuncRel {X} {Y} {Z} perX perY perZ F G) = {!!}
+  isSingleValued (composeFuncRel {X} {Y} {Z} perX perY perZ F G) = {!!}
+  isTotal (composeFuncRel {X} {Y} {Z} perX perY perZ F G) = {!!}
 
   RT : Category (ℓ-max (ℓ-suc ℓ) (ℓ-max (ℓ-suc ℓ') (ℓ-suc ℓ''))) (ℓ-max (ℓ-suc ℓ) (ℓ-max (ℓ-suc ℓ') (ℓ-suc ℓ'')))
-  RT = {!!}
+  Category.ob RT = Σ[ X ∈ Type ℓ' ] PartialEquivalenceRelation X
+  Category.Hom[_,_] RT (X , perX) (Y , perY) = FunctionalRelation perX perY
+  Category.id RT {X , perX} = idFuncRel perX
+  Category._⋆_ RT {X , perX} {Y , perY} {Z , perZ} F G = {!!}
+  Category.⋆IdL RT = {!!}
+  Category.⋆IdR RT = {!!}
+  Category.⋆Assoc RT = {!!}
+  Category.isSetHom RT = {!!}

src/Realizability/Topos/Object.agda

@@ -2,11 +2,16 @@ open import Realizability.ApplicativeStructure renaming (Term to ApplStrTerm)
 open import Realizability.CombinatoryAlgebra
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Equiv
+open import Cubical.HITs.PropositionalTruncation
 open import Cubical.Data.Vec
 open import Cubical.Data.Nat
-open import Cubical.Data.FinData renaming (zero to fzero)
+open import Cubical.Data.FinData
 open import Cubical.Data.Sigma
 open import Cubical.Data.Empty
+open import Cubical.Reflection.RecordEquiv
 
 module Realizability.Topos.Object
   {ℓ ℓ' ℓ''}
@@ -21,10 +26,54 @@ open import Realizability.Tripos.Algebra.Base {ℓ' = ℓ'} {ℓ'' = ℓ''} ca r
 open CombinatoryAlgebra ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
 
-record PartialEquivalenceRelation (X : Type ℓ') : Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ'')) where
+record isPartialEquivalenceRelation (X : Type ℓ') (equality : Predicate (X × X)) : Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ'')) where
   field
     isSetX : isSet X
-    equality : Predicate (X × X)
     isSymmetric : ∃[ sm ∈ A ] (∀ x x' r → r ⊩[ equality ] (x , x') → (sm ⨾ r) ⊩[ equality ] (x' , x))
     isTransitive : ∃[ ts ∈ A ] (∀ x x' x'' r s → r ⊩[ equality ] (x , x') → s ⊩[ equality ] (x' , x'') → (ts ⨾ r ⨾ s) ⊩[ equality ] (x , x''))
-
+
+opaque
+  isPropIsPartialEquivalenceRelation : ∀ X equality → isProp (isPartialEquivalenceRelation X equality)
+  isPropIsPartialEquivalenceRelation X equality x y i =
+    record { isSetX = isPropIsSet {A = X} (x .isSetX) (y .isSetX) i ; isSymmetric = squash₁ (x .isSymmetric) (y .isSymmetric) i ; isTransitive = squash₁ (x .isTransitive) (y .isTransitive) i } where
+      open isPartialEquivalenceRelation
+
+record PartialEquivalenceRelation (X : Type ℓ') : Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ'')) where
+  field
+    equality : Predicate (X × X)
+    isPerEquality : isPartialEquivalenceRelation X equality
+  open isPartialEquivalenceRelation isPerEquality public
+
+open PartialEquivalenceRelation
+
+unquoteDecl PartialEquivalenceRelationIsoΣ = declareRecordIsoΣ PartialEquivalenceRelationIsoΣ (quote PartialEquivalenceRelation)
+
+PartialEquivalenceRelationΣ : (X : Type ℓ') → Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ''))
+PartialEquivalenceRelationΣ X = Σ[ equality ∈ Predicate (X × X) ] isPartialEquivalenceRelation X equality
+
+
+module _ (X : Type ℓ') where opaque
+  open Iso
+  PartialEquivalenceRelationΣ≡ : (perA perB : PartialEquivalenceRelationΣ X) → perA .fst ≡ perB .fst → perA ≡ perB
+  PartialEquivalenceRelationΣ≡ perA perB predicateEq = Σ≡Prop (λ x → isPropIsPartialEquivalenceRelation X x) predicateEq 
+
+  PartialEquivalenceRelationΣ≃ : (perA perB : PartialEquivalenceRelationΣ X) → (perA .fst ≡ perB .fst) ≃ (perA ≡ perB)
+  PartialEquivalenceRelationΣ≃ perA perB = Σ≡PropEquiv λ x → isPropIsPartialEquivalenceRelation X x
+
+  PartialEquivalenceRelationIso : (perA perB : PartialEquivalenceRelation X) → Iso (Iso.fun PartialEquivalenceRelationIsoΣ perA ≡ Iso.fun PartialEquivalenceRelationIsoΣ perB) (perA ≡ perB)
+  Iso.fun (PartialEquivalenceRelationIso perA perB) p i = Iso.inv PartialEquivalenceRelationIsoΣ (p i)
+  inv (PartialEquivalenceRelationIso perA perB) = cong (λ x → Iso.fun PartialEquivalenceRelationIsoΣ x)
+  rightInv (PartialEquivalenceRelationIso perA perB) b = refl
+  leftInv (PartialEquivalenceRelationIso perA perB) a = refl
+
+  -- Main SIP
+  PartialEquivalenceRelation≃ : (perA perB : PartialEquivalenceRelation X) → (perA .equality ≡ perB .equality) ≃ (perA ≡ perB)
+  PartialEquivalenceRelation≃ perA perB =
+    perA .equality ≡ perB .equality
+      ≃⟨ idEquiv (perA .equality ≡ perB .equality) ⟩
+    Iso.fun PartialEquivalenceRelationIsoΣ perA .fst ≡ Iso.fun PartialEquivalenceRelationIsoΣ perB .fst
+      ≃⟨ PartialEquivalenceRelationΣ≃ (Iso.fun PartialEquivalenceRelationIsoΣ perA) (Iso.fun PartialEquivalenceRelationIsoΣ perB) ⟩
+    Iso.fun PartialEquivalenceRelationIsoΣ perA ≡ Iso.fun PartialEquivalenceRelationIsoΣ perB
+      ≃⟨ isoToEquiv (PartialEquivalenceRelationIso perA perB) ⟩
+    perA ≡ perB
+      ■

src/Realizability/Tripos/Algebra/Base.agda

@@ -51,10 +51,9 @@ AlgebraicPredicate X = PosetReflection (Pred.PredicateProperties._≤_ {ℓ'' =
 
 infixl 50 _⊩[_]_
 opaque
-  _⊩[_]_ : ∀ {X : Type ℓ'} → A → AlgebraicPredicate X → X → Type (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
-  r ⊩[ ϕ ] x =
-    ⟨
-      SQ.rec
+  realizes : ∀ {X : Type ℓ'} → A → AlgebraicPredicate X → X → hProp (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
+  realizes {X} r ϕ x =
+    SQ.rec
         isSetHProp
         (λ Ψ → (∃[ s ∈ A ] Pred.Predicate.∣ Ψ ∣ x (s ⨾ r)) , isPropPropTrunc)
         (λ { Ψ Ξ (Ψ≤Ξ , Ξ≤Ψ) →
@@ -78,7 +77,22 @@ opaque
                     prover = ` s ̇ (` p ̇ # fzero)
                   return (λ* prover , subst (λ r' → Pred.Predicate.∣ Ψ ∣ x r') (sym (λ*ComputationRule prover (r ∷ []))) (s⊩Ξ≤Ψ x (p ⨾ r) p⊩Ξ)))) })
         ϕ
-    ⟩
+
+  _⊩[_]_ : ∀ {X : Type ℓ'} → A → AlgebraicPredicate X → X → Type (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
+  r ⊩[ ϕ ] x = ⟨ realizes r ϕ x ⟩
+
+  isProp⊩ : ∀ {X : Type ℓ'} → (a : A) → (ϕ : AlgebraicPredicate X) → (x : X) → isProp (a ⊩[ ϕ ] x)
+  isProp⊩ {X} a ϕ x = realizes a ϕ x .snd
+
+  transformRealizes : ∀ {X : Type ℓ'} → (r : A) → (ϕ : Pred.Predicate X) → (x : X) → (∃[ s ∈ A ] (s ⨾ r) ⊩[ [ ϕ ] ] x) → r ⊩[ [ ϕ ] ] x
+  transformRealizes {X} r ϕ x ∃ =
+    do
+      (s , s⊩ϕx) ← ∃
+      (p , ps⊩ϕx) ← s⊩ϕx
+      let
+        prover : Term as 1
+        prover = ` p ̇ (` s ̇ # fzero)
+      return (λ* prover , subst (λ r' → Pred.Predicate.∣ ϕ ∣ x r') (sym (λ*ComputationRule prover (r ∷ []))) ps⊩ϕx)
 
 module AlgebraicProperties (X : Type ℓ') (isSetX' : isSet X) (isNonTrivial : s ≡ k → ⊥) where
   open Pred

src/Realizability/Tripos/Prealgebra/Predicate/Properties.agda

@@ -1,6 +1,6 @@
 open import Realizability.CombinatoryAlgebra
-open import Realizability.ApplicativeStructure
-open import Cubical.Foundations.Prelude
+open import Realizability.ApplicativeStructure renaming (Term to ApplStrTerm; λ*-naturality to `λ*ComputationRule; λ*-chain to `λ*) hiding (λ*)
+open import Cubical.Foundations.Prelude as P
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Univalence
@@ -11,20 +11,24 @@ open import Cubical.Data.Sigma
 open import Cubical.Data.Empty
 open import Cubical.Data.Unit
 open import Cubical.Data.Sum
+open import Cubical.Data.Vec
 open import Cubical.HITs.PropositionalTruncation
 open import Cubical.HITs.PropositionalTruncation.Monad
 open import Cubical.Relation.Binary.Order.Preorder
 
 module
   Realizability.Tripos.Prealgebra.Predicate.Properties
-  {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+  {ℓ ℓ' ℓ''} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
 open import Realizability.Tripos.Prealgebra.Predicate.Base ca
 
 open CombinatoryAlgebra ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
 open Predicate
-module PredicateProperties {ℓ' ℓ''} (X : Type ℓ') where
+private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+private λ* = `λ* as fefermanStructure
+
+module PredicateProperties (X : Type ℓ') where
   private PredicateX = Predicate {ℓ'' = ℓ''} X
   open Predicate
   _≤_ : Predicate {ℓ'' = ℓ''} X → Predicate {ℓ'' = ℓ''} X → Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
@@ -83,12 +87,52 @@ module PredicateProperties {ℓ' ℓ''} (X : Type ℓ') where
   ∣ ϕ ⇒ ψ ∣ x a = ∀ b → (b ⊩ ∣ ϕ ∣ x) → (a ⨾ b) ⊩ ∣ ψ ∣ x
   (ϕ ⇒ ψ) .isPropValued x a = isPropΠ λ a → isPropΠ λ a⊩ϕx → ψ .isPropValued _ _
 
+module _ where
+  open PredicateProperties Unit*
+  private
+    Predicate' = Predicate {ℓ' = ℓ'} {ℓ'' = ℓ''}
+  module NotAntiSym (antiSym : ∀ (a b : Predicate Unit*) → (a≤b : a ≤ b) → (b≤a : b ≤ a) → a ≡ b) where
+    Lift' = Lift {i = ℓ} {j = (ℓ-max ℓ' ℓ'')}
+
+    kRealized : Predicate' Unit*
+    kRealized = record { isSetX = isSetUnit* ; ∣_∣ = λ x a → Lift' (a ≡ k) ; isPropValued = λ x a → isOfHLevelRespectEquiv 1 LiftEquiv (isSetA a k) }
+
+    k'Realized : Predicate' Unit*
+    k'Realized = record { isSetX = isSetUnit* ; ∣_∣ = λ x a → Lift' (a ≡ k') ; isPropValued = λ x a → isOfHLevelRespectEquiv 1 LiftEquiv (isSetA a k') }
+
+    kRealized≤k'Realized : kRealized ≤ k'Realized
+    kRealized≤k'Realized =
+      do
+        let
+          prover : ApplStrTerm as 1
+          prover = ` k'
+        return (λ* prover , λ { x a (lift a≡k) → lift (λ*ComputationRule prover (a ∷ [])) })
+
+    k'Realized≤kRealized : k'Realized ≤ kRealized
+    k'Realized≤kRealized =
+      do
+        let
+          prover : ApplStrTerm as 1
+          prover = ` k
+        return (λ* prover , λ { x a (lift a≡k') → lift (λ*ComputationRule prover (a ∷ [])) })
+
+    kRealized≡k'Realized : kRealized ≡ k'Realized
+    kRealized≡k'Realized = antiSym kRealized k'Realized kRealized≤k'Realized k'Realized≤kRealized
+
+    Lift≡ : Lift' (k ≡ k) ≡ Lift' (k ≡ k')
+    Lift≡ i = ∣ kRealized≡k'Realized i ∣ tt* k
+
+    Liftk≡k' : Lift' (k ≡ k')
+    Liftk≡k' = transport Lift≡ (lift refl)
+
+    k≡k' : k ≡ k'
+    k≡k' = Liftk≡k' .lower
 
-module Morphism {ℓ' ℓ''} {X Y : Type ℓ'} (isSetX : isSet X) (isSetY : isSet Y)  where
+module Morphism {X Y : Type ℓ'} (isSetX : isSet X) (isSetY : isSet Y)  where
   PredicateX = Predicate {ℓ'' = ℓ''} X
   PredicateY = Predicate {ℓ'' = ℓ''} Y
-  module PredicatePropertiesX = PredicateProperties {ℓ'' = ℓ''} X
-  module PredicatePropertiesY = PredicateProperties {ℓ'' = ℓ''} Y
+  module PredicatePropertiesX = PredicateProperties X
+  module PredicatePropertiesY = PredicateProperties Y
   open PredicatePropertiesX renaming (_≤_ to _≤X_ ; isProp≤ to isProp≤X)
   open PredicatePropertiesY renaming (_≤_ to _≤Y_ ; isProp≤ to isProp≤Y)
   open Predicate hiding (isSetX)
@@ -232,15 +276,14 @@ module Morphism {ℓ' ℓ''} {X Y : Type ℓ'} (isSetX : isSet X) (isSetY : isSe
 
 -- The proof is trivial but I am the reader it was left to as an exercise
 module BeckChevalley
-    {ℓ' ℓ'' : Level}
     (I J K : Type ℓ')
     (isSetI : isSet I)
     (isSetJ : isSet J)
     (isSetK : isSet K)
     (f : J → I)
     (g : K → I) where
 
-    module Morphism' = Morphism {ℓ' = ℓ'} {ℓ'' = ℓ''}
+    module Morphism' = Morphism
     open Morphism'
 
     L = Σ[ k ∈ K ] Σ[ j ∈ J ] (g k ≡ f j)