Add Binary Sum Types and Truncations

Application/NegativeAxioms/Canonicity.agda

@@ -5,7 +5,7 @@
 
 module Application.NegativeAxioms.Canonicity where
 
-open import Definition.Untyped as U
+open import Definition.Untyped as U hiding (ℕ≢∪ ; Empty≢∪ ; ℕ≢∥ ; Empty≢∥)
 
 open import Definition.Typed
 open import Definition.Typed.Properties
@@ -142,6 +142,18 @@ appNeg (conv n c)    c' = appNeg n (trans c c')
 ¬negℕ (sigma _ _ _) c = ℕ≢Σ (sym c)
 ¬negℕ (conv n c)   c' = ¬negℕ n (trans c c')
 
+¬neg∪ : NegativeType Γ C → Γ ⊢ C ≡ A ∪ B → ⊥
+¬neg∪ empty         c = Empty≢∪ c
+¬neg∪ (pi _ _)      c = B≢∪ BΠ c
+¬neg∪ (sigma _ _ _) c = B≢∪ BΣ c
+¬neg∪ (conv n c)   c' = ¬neg∪ n (trans c c')
+
+¬neg∥ : NegativeType Γ C → Γ ⊢ C ≡ ∥ A ∥ → ⊥
+¬neg∥ empty         c = Empty≢∥ c
+¬neg∥ (pi _ _)      c = B≢∥ BΠ c
+¬neg∥ (sigma _ _ _) c = B≢∥ BΣ c
+¬neg∥ (conv n c)   c' = ¬neg∥ n (trans c c')
+
 -- Negative contexts
 ---------------------------------------------------------------------------
 
@@ -174,6 +186,8 @@ module Main (nΓ : NegativeContext Γ) (consistent : ∀{t} → Γ ⊢ t ∷ Emp
   neNeg (fstⱼ ⊢A A⊢B d  ) (fstₙ n          ) = fstNeg (neNeg d n) (refl (Σⱼ ⊢A ▹ A⊢B))
   neNeg (sndⱼ ⊢A A⊢B d  ) (sndₙ n          ) = sndNeg (neNeg d n) (refl (Σⱼ ⊢A ▹ A⊢B)) (fstⱼ ⊢A A⊢B d)
   neNeg (natrecⱼ _ _ _ d) (natrecₙ _ _ _ n ) = ⊥-elim (¬negℕ (neNeg d n) ⊢ℕ) where ⊢ℕ = refl (ℕⱼ (wfTerm d))
+  neNeg (casesⱼ d _ _ _ ) (casesₙ _ n _ _  ) = ⊥-elim (¬neg∪ (neNeg d n) (refl (syntacticTerm d)))
+  neNeg (∥ₑⱼ d _ _      ) (∥ₑₙ _ n _       ) = ⊥-elim (¬neg∥ (neNeg d n) (refl (syntacticTerm d)))
   neNeg (Emptyrecⱼ _ d  ) (Emptyrecₙ _ _   ) = ⊥-elim (consistent d)
   neNeg (conv d c       ) n                  = conv (neNeg d n) c
 
@@ -199,13 +213,18 @@ module Main (nΓ : NegativeContext Γ) (consistent : ∀{t} → Γ ⊢ t ∷ Emp
   -- * Canonical types
   nfN (Πⱼ _ ▹ _)      (Πₙ _ _)    c = ⊥-elim (U≢ℕ c)
   nfN (Σⱼ _ ▹ _)      (Σₙ _ _)    c = ⊥-elim (U≢ℕ c)
+  nfN (_ ∪ⱼ _)        (∪ₙ _ _)    c = ⊥-elim (U≢ℕ c)
+  nfN (∥ _ ∥ⱼ)        (∥ₙ _)      c = ⊥-elim (U≢ℕ c)
   nfN (ℕⱼ _)           ℕₙ         c = ⊥-elim (U≢ℕ c)
   nfN (Emptyⱼ _)       Emptyₙ     c = ⊥-elim (U≢ℕ c)
   nfN (Unitⱼ _)        Unitₙ      c = ⊥-elim (U≢ℕ c)
 
   -- * Canonical forms
   nfN (lamⱼ _ _)      (lamₙ _)    c = ⊥-elim (ℕ≢Π (sym c))
   nfN (prodⱼ _ _ _ _) (prodₙ _ _) c = ⊥-elim (ℕ≢Σ (sym c))
+  nfN (injlⱼ _ _)     (injlₙ _)   c = ⊥-elim (ℕ≢∪ (sym c))
+  nfN (injrⱼ _ _)     (injrₙ _)   c = ⊥-elim (ℕ≢∪ (sym c))
+  nfN (∥ᵢⱼ _)         (∥ᵢₙ _)     c = ⊥-elim (ℕ≢∥ (sym c))
   nfN (starⱼ _)       starₙ       c = ⊥-elim (ℕ≢Unitⱼ (sym c))
   -- q.e.d
 

Definition/Conversion.agda

@@ -48,6 +48,17 @@ mutual
                   → Γ ⊢ h [conv↑] g ∷ Π ℕ ▹ (F ▹▹ F [ suc (var x0) ]↑)
                   → Γ ⊢ k ~ l ↓ ℕ
                   → Γ ⊢ natrec F a₀ h k ~ natrec G b₀ g l ↑ F [ k ]
+    cases-cong    : ∀ {t t' u u' v v' A B C C'}
+                  → Γ ⊢ C [conv↑] C'
+                  → Γ ⊢ t ~ t' ↓ A ∪ B
+                  → Γ ⊢ u [conv↑] u' ∷ A ▹▹ C
+                  → Γ ⊢ v [conv↑] v' ∷ B ▹▹ C
+                  → Γ ⊢ cases C t u v ~ cases C' t' u' v' ↑ C
+    ∥ₑ-cong    : ∀ {a a' f f' A B B'}
+                  → Γ ⊢ B [conv↑] B'
+                  → Γ ⊢ a ~ a' ↓ ∥ A ∥
+                  → Γ ⊢ f [conv↑] f' ∷ A ▹▹ ∥ B ∥
+                  → Γ ⊢ ∥ₑ B a f ~ ∥ₑ B' a' f' ↑ ∥ B ∥
     Emptyrec-cong : ∀ {k l F G}
                   → Γ ⊢ F [conv↑] G
                   → Γ ⊢ k ~ l ↓ Empty
@@ -94,6 +105,13 @@ mutual
                → Γ ⊢ F [conv↑] H
                → Γ ∙ F ⊢ G [conv↑] E
                → Γ ⊢ Σ F ▹ G [conv↓] Σ H ▹ E
+    ∪-cong     : ∀ {A B C D}
+               → Γ ⊢ A [conv↑] B
+               → Γ ⊢ C [conv↑] D
+               → Γ ⊢ A ∪ C [conv↓] B ∪ D
+    ∥-cong     : ∀ {A B}
+               → Γ ⊢ A [conv↑] B
+               → Γ ⊢ ∥ A ∥ [conv↓] ∥ B ∥
 
   -- Term equality.
   record _⊢_[conv↑]_∷_ (Γ : Con Term n) (t u A : Term n) : Set where
@@ -150,6 +168,36 @@ mutual
               → Γ ⊢ fst p [conv↑] fst r ∷ F
               → Γ ⊢ snd p [conv↑] snd r ∷ G [ fst p ]
               → Γ ⊢ p [conv↓] r ∷ Σ F ▹ G
+    ∪₁-η      : ∀ {p r pa ra A B}
+              → Γ ⊢ p ∷ A ∪ B
+              → Γ ⊢ r ∷ A ∪ B
+              → InjectionL p pa
+              → InjectionL r ra
+              → Γ ⊢ pa [conv↑] ra ∷ A
+              → Γ ⊢ p [conv↓] r ∷ A ∪ B
+    ∪₂-η      : ∀ {p r pa ra A B}
+              → Γ ⊢ p ∷ A ∪ B
+              → Γ ⊢ r ∷ A ∪ B
+              → InjectionR p pa
+              → InjectionR r ra
+              → Γ ⊢ pa [conv↑] ra ∷ B
+              → Γ ⊢ p [conv↓] r ∷ A ∪ B
+    ∪₃-η      : ∀ {p r A B C D}
+              → Γ ⊢ A ≡ C
+              → Γ ⊢ B ≡ D
+              → Γ ⊢ p ~ r ↓ A ∪ B
+              → Γ ⊢ p [conv↓] r ∷ C ∪ D
+    ∥₁-η      : ∀ {p r pa ra A}
+              → Γ ⊢ p ∷ ∥ A ∥
+              → Γ ⊢ r ∷ ∥ A ∥
+              → TruncI p pa
+              → TruncI r ra
+              → Γ ⊢ pa [conv↑] ra ∷ A
+              → Γ ⊢ p [conv↓] r ∷ ∥ A ∥
+    ∥₂-η      : ∀ {p r A B}
+              → Γ ⊢ A ≡ B
+              → Γ ⊢ p ~ r ↓ ∥ A ∥
+              → Γ ⊢ p [conv↓] r ∷ ∥ B ∥
     η-unit    : ∀ {k l}
               → Γ ⊢ k ∷ Unit
               → Γ ⊢ l ∷ Unit

Definition/Conversion/Conversion.agda

@@ -10,6 +10,7 @@ open import Definition.Typed.Properties
 open import Definition.Conversion
 open import Definition.Conversion.Stability
 open import Definition.Conversion.Soundness
+open import Definition.Conversion.Whnf using (ne~↑ ; ne~↓)
 open import Definition.Typed.Consequences.Syntactic
 open import Definition.Typed.Consequences.Substitution
 open import Definition.Typed.Consequences.Injectivity
@@ -84,14 +85,52 @@ mutual
             rProd
             (convConv↑Term Γ≡Δ F≡ fstConv)
             (convConv↑Term Γ≡Δ (substTypeEq G≡ (refl ⊢fst)) sndConv)
+  convConv↓Term Γ≡Δ A≡B whnfB (∪₁-η ⊢p ⊢r pInj rInj cnv)
+    with ∪≡A A≡B whnfB
+  ... | C , D , PE.refl =
+    let C≡ , D≡ = ∪-injectivity A≡B
+    in  ∪₁-η (stabilityTerm Γ≡Δ (conv ⊢p A≡B))
+             (stabilityTerm Γ≡Δ (conv ⊢r A≡B))
+             pInj rInj
+             (convConv↑Term Γ≡Δ C≡ cnv)
+  convConv↓Term Γ≡Δ A≡B whnfB (∪₂-η ⊢p ⊢r pInj rInj cnv)
+    with ∪≡A A≡B whnfB
+  ... | C , D , PE.refl =
+    let C≡ , D≡ = ∪-injectivity A≡B
+    in  ∪₂-η (stabilityTerm Γ≡Δ (conv ⊢p A≡B))
+             (stabilityTerm Γ≡Δ (conv ⊢r A≡B))
+             pInj rInj
+             (convConv↑Term Γ≡Δ D≡ cnv)
+  convConv↓Term Γ≡Δ A≡B whnfB (∪₃-η c₁ c₂ p~r)
+    with ∪≡A A≡B whnfB
+  ... | C , D , PE.refl =
+    let C≡ , D≡ = ∪-injectivity A≡B
+    in  ∪₃-η (stabilityEq Γ≡Δ (trans c₁ C≡))
+             (stabilityEq Γ≡Δ (trans c₂ D≡))
+             (stability~↓ Γ≡Δ p~r)
+  convConv↓Term Γ≡Δ A≡B whnfB (∥₁-η ⊢p ⊢r pi ri cnv)
+    with ∥≡A A≡B whnfB
+  ... | C , PE.refl =
+    let C≡ = ∥-injectivity A≡B
+    in  ∥₁-η (stabilityTerm Γ≡Δ (conv ⊢p A≡B))
+             (stabilityTerm Γ≡Δ (conv ⊢r A≡B))
+             pi ri
+             (convConv↑Term Γ≡Δ C≡ cnv)
+  convConv↓Term Γ≡Δ A≡B whnfB (∥₂-η c₁ p~r)
+    with ∥≡A A≡B whnfB
+  ... | C , PE.refl =
+    let C≡ = ∥-injectivity A≡B
+    in  ∥₂-η (stabilityEq Γ≡Δ (trans c₁ C≡))
+             (stability~↓ Γ≡Δ p~r)
   convConv↓Term Γ≡Δ A≡B whnfB (η-unit [t] [u] tUnit uUnit) rewrite Unit≡A A≡B whnfB =
     let [t] = stabilityTerm Γ≡Δ [t]
         [u] = stabilityTerm Γ≡Δ [u]
     in  η-unit [t] [u] tUnit uUnit
 
 -- Conversion of algorithmic equality with the same context.
-convConvTerm : ∀ {t u A B}
-              → Γ ⊢ t [conv↑] u ∷ A
-              → Γ ⊢ A ≡ B
-              → Γ ⊢ t [conv↑] u ∷ B
-convConvTerm t<>u A≡B = convConv↑Term (reflConEq (wfEq A≡B)) A≡B t<>u
+abstract
+  convConvTerm : ∀ {t u A B}
+               → Γ ⊢ t [conv↑] u ∷ A
+               → Γ ⊢ A ≡ B
+               → Γ ⊢ t [conv↑] u ∷ B
+  convConvTerm t<>u A≡B = convConv↑Term (reflConEq (wfEq A≡B)) A≡B t<>u