First steps of tripos-to-topos (UniMath#1911)

This PR contains the first steps of the tripos-to-topos construction. More specifically, it contains: - Category of partial setoids - Finite limits of partial setoids - Constant object functor (every type gives rise to a partial setoid with equality as the partial equivalence relation) - Properties of the constant object functor - Subobjects of a constant partial setoid `X` are the same as formulas in context `X` For the tripos-to-topos construction, only 2 steps are left: the subobject classifier and the construction of exponentials.
rmatthes · Aug 16, 2024 · 457184c · 457184c
1 parent 75bfea4
commit 457184c
Show file tree

Hide file tree

Showing 17 changed files with 5,755 additions and 40 deletions.
diff --git a/UniMath/CONTENTS.md b/UniMath/CONTENTS.md
@@ -336,10 +336,18 @@ The packages and files are listed here in logical order: each file depends only
    - [DisplayedCats/MonoCodomain/MonoCodColimits.v](CategoryTheory/DisplayedCats/MonoCodomain/MonoCodColimits.v)
    - [DisplayedCats/MonoCodomain/MonoCodRightAdjoint.v](CategoryTheory/DisplayedCats/MonoCodomain/MonoCodRightAdjoint.v)
    - [DisplayedCats/MonoCodomain/MonoHyperdoctrine.v](CategoryTheory/DisplayedCats/MonoCodomain/MonoHyperdoctrine.v)
-   - [DisplayedCats/Hyperdoctrines/Hyperdoctrine.v](CategoryTheory/DisplayedCats/Hyperdoctrines/Hyperdoctrine.v)
-   - [DisplayedCats/Hyperdoctrines/FirstOrderHyperdoctrine.v](CategoryTheory/DisplayedCats/Hyperdoctrines/FirstOrderHyperdoctrine.v)
-   - [DisplayedCats/Hyperdoctrines/Tripos.v](CategoryTheory/DisplayedCats/Hyperdoctrines/Tripos.v)
-   - [DisplayedCats/Hyperdoctrines/PERs.v](CategoryTheory/DisplayedCats/Hyperdoctrines/PERs.v)
+   - [Hyperdoctrines/Hyperdoctrine.v](CategoryTheory/Hyperdoctrines/Hyperdoctrine.v)
+   - [Hyperdoctrines/FirstOrderHyperdoctrine.v](CategoryTheory/Hyperdoctrines/FirstOrderHyperdoctrine.v)
+   - [Hyperdoctrines/Tripos.v](CategoryTheory/Hyperdoctrines/Tripos.v)
+   - [Hyperdoctrines/PartialEqRels/PERs.v](CategoryTheory/Hyperdoctrines/PartialEqRels/PERs.v)
+   - [Hyperdoctrines/PartialEqRels/PERMorphisms.v](CategoryTheory/Hyperdoctrines/PartialEqRels/PERMorphisms.v)
+   - [Hyperdoctrines/PartialEqRels/PERCategory.v](CategoryTheory/Hyperdoctrines/PartialEqRels/PERCategory.v)
+   - [Hyperdoctrines/PartialEqRels/PERConstantObjects.v](CategoryTheory/Hyperdoctrines/PartialEqRels/PERConstantObjects.v)
+   - [Hyperdoctrines/PartialEqRels/PERTerminal.v](CategoryTheory/Hyperdoctrines/PartialEqRels/PERTerminal.v)
+   - [Hyperdoctrines/PartialEqRels/PERInitial.v](CategoryTheory/Hyperdoctrines/PartialEqRels/PERInitial.v)
+   - [Hyperdoctrines/PartialEqRels/PERBinProducts.v](CategoryTheory/Hyperdoctrines/PartialEqRels/PERBinProducts.v)
+   - [Hyperdoctrines/PartialEqRels/PEREqualizers.v](CategoryTheory/Hyperdoctrines/PartialEqRels/PEREqualizers.v)
+   - [Hyperdoctrines/PartialEqRels/PERMonomorphisms.v](CategoryTheory/Hyperdoctrines/PartialEqRels/PERMonomorphisms.v)
    - [DisplayedCats/Examples/HValuedPredicates.v](CategoryTheory/DisplayedCats/Examples/HValuedPredicates.v)
    - [LocallyCartesianClosed/LocallyCartesianClosed.v](CategoryTheory/LocallyCartesianClosed/LocallyCartesianClosed.v)
    - [DisplayedCats/Fiberwise/DualBeckChevalley.v](CategoryTheory/DisplayedCats/Fiberwise/DualBeckChevalley.v)

diff --git a/UniMath/CategoryTheory/.package/files b/UniMath/CategoryTheory/.package/files
@@ -138,10 +138,19 @@ DisplayedCats/MonoCodomain/MonoCodColimits.v
 DisplayedCats/MonoCodomain/MonoCodRightAdjoint.v
 DisplayedCats/MonoCodomain/MonoHyperdoctrine.v
 
-DisplayedCats/Hyperdoctrines/Hyperdoctrine.v
-DisplayedCats/Hyperdoctrines/FirstOrderHyperdoctrine.v
-DisplayedCats/Hyperdoctrines/Tripos.v
-DisplayedCats/Hyperdoctrines/PERs.v
+Hyperdoctrines/Hyperdoctrine.v
+Hyperdoctrines/FirstOrderHyperdoctrine.v
+Hyperdoctrines/Tripos.v
+
+Hyperdoctrines/PartialEqRels/PERs.v
+Hyperdoctrines/PartialEqRels/PERMorphisms.v
+Hyperdoctrines/PartialEqRels/PERCategory.v
+Hyperdoctrines/PartialEqRels/PERConstantObjects.v
+Hyperdoctrines/PartialEqRels/PERTerminal.v
+Hyperdoctrines/PartialEqRels/PERInitial.v
+Hyperdoctrines/PartialEqRels/PERBinProducts.v
+Hyperdoctrines/PartialEqRels/PEREqualizers.v
+Hyperdoctrines/PartialEqRels/PERMonomorphisms.v
 
 DisplayedCats/Examples/HValuedPredicates.v
 

diff --git a/UniMath/CategoryTheory/DisplayedCats/Examples/HValuedPredicates.v b/UniMath/CategoryTheory/DisplayedCats/Examples/HValuedPredicates.v
@@ -61,9 +61,9 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproduct
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesianClosed.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums.
-Require Import UniMath.CategoryTheory.DisplayedCats.Hyperdoctrines.Hyperdoctrine.
-Require Import UniMath.CategoryTheory.DisplayedCats.Hyperdoctrines.FirstOrderHyperdoctrine.
-Require Import UniMath.CategoryTheory.DisplayedCats.Hyperdoctrines.Tripos.
+Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine.
+Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.
+Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos.
 
 Local Open Scope cat.
 Local Open Scope heyting.

diff --git a/UniMath/CategoryTheory/DisplayedCats/MonoCodomain/MonoHyperdoctrine.v b/UniMath/CategoryTheory/DisplayedCats/MonoCodomain/MonoHyperdoctrine.v
@@ -49,8 +49,8 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesian
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts.
 Require Import UniMath.CategoryTheory.RegularAndExact.RegularCategory.
-Require Import UniMath.CategoryTheory.DisplayedCats.Hyperdoctrines.Hyperdoctrine.
-Require Import UniMath.CategoryTheory.DisplayedCats.Hyperdoctrines.FirstOrderHyperdoctrine.
+Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine.
+Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.
 
 Local Open Scope cat.
 

diff --git a/.../Hyperdoctrines/FirstOrderHyperdoctrine.v → .../Hyperdoctrines/FirstOrderHyperdoctrine.v b/.../Hyperdoctrines/FirstOrderHyperdoctrine.v → .../Hyperdoctrines/FirstOrderHyperdoctrine.v
@@ -98,7 +98,7 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproduct
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesianClosed.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums.
-Require Import UniMath.CategoryTheory.DisplayedCats.Hyperdoctrines.Hyperdoctrine.
+Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine.
 Require Import UniMath.CategoryTheory.Limits.Initial.
 Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.Limits.BinProducts.
@@ -456,7 +456,7 @@ Proposition weaken_cut
   : Δ ⊢ ψ.
 Proof.
   refine (hyperdoctrine_cut _ q).
-  use (BinProductArrow _ (binprod_in_fib (pr1 (pr222 H)) Δ φ)).
+  use (BinProductArrow _ (binprod_in_fib _ Δ φ)).
   - apply hyperdoctrine_hyp.
   - exact p.
 Qed.
@@ -487,6 +487,44 @@ Proof.
     apply hyperdoctrine_hyp.
 Qed.
 
+Proposition hyp_ltrans
+            {H : first_order_hyperdoctrine}
+            {Γ : ty H}
+            {Δ Δ' Δ'' φ : form Γ}
+            (p : Δ ∧ (Δ' ∧ Δ'') ⊢ φ)
+  : (Δ ∧ Δ') ∧ Δ'' ⊢ φ.
+Proof.
+  refine (hyperdoctrine_cut _ p).
+  use conj_intro.
+  - do 2 use weaken_left.
+    apply hyperdoctrine_hyp.
+  - use conj_intro.
+    + use weaken_left.
+      use weaken_right.
+      apply hyperdoctrine_hyp.
+    + use weaken_right.
+      apply hyperdoctrine_hyp.
+Qed.
+
+Proposition hyp_rtrans
+            {H : first_order_hyperdoctrine}
+            {Γ : ty H}
+            {Δ Δ' Δ'' φ : form Γ}
+            (p : (Δ ∧ Δ') ∧ Δ'' ⊢ φ)
+  : Δ ∧ (Δ' ∧ Δ'') ⊢ φ.
+Proof.
+  refine (hyperdoctrine_cut _ p).
+  use conj_intro.
+  - use conj_intro.
+    + use weaken_left.
+      apply hyperdoctrine_hyp.
+    + use weaken_right.
+      use weaken_left.
+      apply hyperdoctrine_hyp.
+  - do 2 use weaken_right.
+    apply hyperdoctrine_hyp.
+Qed.
+
 (** * 6. Disjunction *)
 Definition first_order_hyperdoctrine_disj
            {H : first_order_hyperdoctrine}
@@ -1153,7 +1191,49 @@ Proof.
   exact r.
 Qed.
 
-Proposition hyperdoctrine_unit_eq
+Proposition hyperdoctrine_eq_transportf
+            {H : first_order_hyperdoctrine}
+            {Γ A : ty H}
+            {Δ : form Γ}
+            {t₁ t₂ : tm Γ A}
+            (φ : form A)
+            (p : Δ ⊢ t₁ ≡ t₂)
+            (q : Δ ⊢ φ [ t₁ ])
+  : Δ ⊢ φ [ t₂ ].
+Proof.
+  assert (Δ ⊢ t₁ ≡ t₂ ∧ φ [ t₁ ]) as r.
+  {
+    exact (conj_intro p q).
+  }
+  refine (hyperdoctrine_cut r _).
+  pose (hyperdoctrine_eq_elim
+          (φ [ π₂ (tm_var _) ])
+          (weaken_left (hyperdoctrine_hyp _) _)
+          (weaken_right (hyperdoctrine_hyp _) (t₁ ≡ t₂)))
+    as h.
+  rewrite !hyperdoctrine_comp_subst in h.
+  rewrite !hyperdoctrine_pr2_subst in h.
+  rewrite !var_tm_subst in h.
+  rewrite !hyperdoctrine_pair_pr2 in h.
+  exact h.
+Qed.
+
+Proposition hyperdoctrine_eq_transportb
+            {H : first_order_hyperdoctrine}
+            {Γ A : ty H}
+            {Δ : form Γ}
+            {t₁ t₂ : tm Γ A}
+            (φ : form A)
+            (p : Δ ⊢ t₁ ≡ t₂)
+            (q : Δ ⊢ φ [ t₂ ])
+  : Δ ⊢ φ [ t₁ ].
+Proof.
+  use (hyperdoctrine_eq_transportf _ _ q).
+  use hyperdoctrine_eq_sym.
+  exact p.
+Qed.
+
+Proposition hyperdoctrine_unit_eq_prf
             {H : first_order_hyperdoctrine}
             {Γ : ty H}
             (t : tm Γ 𝟙)
@@ -1164,6 +1244,18 @@ Proof.
   apply hyperdoctrine_unit_eq.
 Qed.
 
+Proposition hyperdoctrine_unit_tm_eq
+            {H : first_order_hyperdoctrine}
+            {Γ : ty H}
+            (t t' : tm Γ 𝟙)
+            (Δ : form Γ)
+  : Δ ⊢ t ≡ t'.
+Proof.
+  refine (hyperdoctrine_eq_trans (hyperdoctrine_unit_eq_prf t Δ) _).
+  use hyperdoctrine_eq_sym.
+  apply hyperdoctrine_unit_eq_prf.
+Qed.
+
 Proposition hyperdoctrine_eq_pr1
             {H : first_order_hyperdoctrine}
             {Γ A B : ty H}
@@ -1335,6 +1427,58 @@ Proof.
            (hyperdoctrine_eq_pair_right _ q)).
 Qed.
 
+Proposition hyperdoctrine_eq_prod_eq
+            {H : first_order_hyperdoctrine}
+            {Γ A B : ty H}
+            {Δ : form Γ}
+            {t₁ t₂ : tm Γ (A ×h B)}
+            (p : Δ ⊢ π₁ t₁ ≡ π₁ t₂)
+            (q : Δ ⊢ π₂ t₁ ≡ π₂ t₂)
+  : Δ ⊢ t₁ ≡ t₂.
+Proof.
+  rewrite (hyperdoctrine_pair_eta t₁).
+  rewrite (hyperdoctrine_pair_eta t₂).
+  use hyperdoctrine_eq_pair_eq.
+  - exact p.
+  - exact q.
+Qed.
+
+Proposition hyperdoctrine_subst_eq
+            {H : first_order_hyperdoctrine}
+            {Γ Γ' B : ty H}
+            {Δ : form _}
+            {s₁ s₂ : tm Γ Γ'}
+            (p : Δ ⊢ s₁ ≡ s₂)
+            (t : tm Γ' B)
+  : Δ ⊢ t [ s₁ ]tm ≡ t [ s₂ ]tm.
+Proof.
+  pose (φ := t [ s₁ [ π₁ (tm_var _) ]tm ]tm ≡ t [ π₂ (tm_var _) ]tm).
+  assert (Δ ⊢ φ [⟨ tm_var Γ, s₁ ⟩]) as q.
+  {
+    unfold φ.
+    rewrite equal_subst.
+    rewrite !tm_subst_comp.
+    rewrite hyperdoctrine_pr1_subst.
+    rewrite hyperdoctrine_pr2_subst.
+    rewrite var_tm_subst.
+    rewrite hyperdoctrine_pair_pr1.
+    rewrite hyperdoctrine_pair_pr2.
+    rewrite tm_subst_var.
+    apply hyperdoctrine_refl.
+  }
+  pose (r := hyperdoctrine_eq_elim φ p q).
+  unfold φ in r.
+  rewrite equal_subst in r.
+  rewrite !tm_subst_comp in r.
+  rewrite hyperdoctrine_pr1_subst in r.
+  rewrite hyperdoctrine_pr2_subst in r.
+  rewrite var_tm_subst in r.
+  rewrite hyperdoctrine_pair_pr1 in r.
+  rewrite hyperdoctrine_pair_pr2 in r.
+  rewrite tm_subst_var in r.
+  exact r.
+Qed.
+
 (** * 12. A tactic for simplifying goals in the internal language of first-order hyperdoctrines *)
 
 (**