Merge pull request #829 from ecavallo/non-dependent-product-in-autouarel

Add non-dependent product special case to uarel automation
agda · Jun 2, 2022 · 2868ce7 · 2868ce7
2 parents 1d9b969 + 48864c4
commit 2868ce7
Show file tree

Hide file tree

Showing 2 changed files with 42 additions and 3 deletions.
diff --git a/Cubical/Displayed/Auto.agda b/Cubical/Displayed/Auto.agda
@@ -40,6 +40,13 @@ mutual
 
     univ : ∀ ℓU → UARelDesc (𝒮-Univ ℓU)
 
+    -- Having a special descriptor for non-dependent × helps to avoid
+    -- combinatorial explosion. Automation will try to apply this first.
+    prod : ∀ {ℓA ℓ≅A ℓB ℓ≅B}
+      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} (dA : UARelDesc 𝒮-A)
+      {B : Type ℓB} {𝒮-B : UARel B ℓ≅B} (dB : UARelDesc 𝒮-B)
+      → UARelDesc (𝒮-A ×𝒮 𝒮-B)
+
     sigma : ∀ {ℓA ℓ≅A ℓB ℓ≅B}
       {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} (dA : UARelDesc 𝒮-A)
       {B : A → Type ℓB} {𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B} (dB : DUARelDesc 𝒮-A 𝒮ᴰ-B)
@@ -110,6 +117,12 @@ mutual
       → UARelReindex f
       → SubstRelDesc 𝒮-A (𝒮ˢ-reindex f (𝒮ˢ-El ℓU))
 
+    prod : ∀ {ℓA ℓ≅A ℓB ℓC}
+      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
+      {B : A → Type ℓB} {𝒮ˢ-B : SubstRel 𝒮-A B} (dB : SubstRelDesc 𝒮-A 𝒮ˢ-B)
+      {C : A → Type ℓC} {𝒮ˢ-C : SubstRel 𝒮-A C} (dC : SubstRelDesc 𝒮-A 𝒮ˢ-C)
+      → SubstRelDesc 𝒮-A (𝒮ˢ-B ×𝒮ˢ 𝒮ˢ-C)
+
     sigma : ∀ {ℓA ℓ≅A ℓB ℓC}
       {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
       {B : A → Type ℓB} {𝒮ˢ-B : SubstRel 𝒮-A B} (dB : SubstRelDesc 𝒮-A 𝒮ˢ-B)
@@ -141,6 +154,12 @@ mutual
       → UARelReindex f
       → DUARelDesc 𝒮-A (𝒮ᴰ-reindex f (𝒮ᴰ-El ℓU))
 
+    prod : ∀ {ℓA ℓ≅A ℓB ℓ≅B ℓC ℓ≅C}
+      {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
+      {B : A → Type ℓB} {𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B} (dB : DUARelDesc 𝒮-A 𝒮ᴰ-B)
+      {C : A → Type ℓC} {𝒮ᴰ-C : DUARel 𝒮-A C ℓ≅C} (dC : DUARelDesc 𝒮-A 𝒮ᴰ-C)
+      → DUARelDesc 𝒮-A (𝒮ᴰ-B ×𝒮ᴰ 𝒮ᴰ-C)
+
     sigma : ∀ {ℓA ℓ≅A ℓB ℓ≅B ℓC ℓ≅C}
       {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
       {B : A → Type ℓB} {𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B} (dB : DUARelDesc 𝒮-A 𝒮ᴰ-B)
@@ -178,7 +197,7 @@ mutual
   autoUARelDesc : ℕ → R.Term → R.TC Unit
   autoUARelDesc zero hole = R.typeError [ R.strErr "Out of fuel" ]
   autoUARelDesc (suc n) hole =
-    tryUniv <|> trySigma <|> tryParam <|> tryPi <|> tryUnit <|> useGeneric
+    tryUniv <|> tryProd <|> trySigma <|> tryParam <|> tryPi <|> tryUnit <|> useGeneric
     where
     tryUniv : R.TC Unit
     tryUniv = R.unify (R.con (quote UARelDesc.univ) [ varg R.unknown ]) hole
@@ -198,6 +217,7 @@ mutual
       R.unify (R.con (quote UARelDesc.param) (paramTy v∷ hole₁ v∷ [])) hole >>
       autoUARelDesc n hole₁
 
+    tryProd = tryBinary (quote UARelDesc.prod)
     trySigma = tryBinary (quote UARelDesc.sigma)
     tryPi = tryBinary (quote UARelDesc.pi)
 
@@ -234,7 +254,7 @@ mutual
   autoSubstRelDesc : ℕ → R.Term → R.TC Unit
   autoSubstRelDesc zero hole = R.typeError [ R.strErr "Out of fuel" ]
   autoSubstRelDesc (suc n) hole =
-    tryConstant <|> tryEl <|> tryEl <|> trySigma <|> tryPi <|> useGeneric
+    tryConstant <|> tryEl <|> tryProd <|> trySigma <|> tryPi <|> useGeneric
     where
     tryConstant : R.TC Unit
     tryConstant =
@@ -254,6 +274,7 @@ mutual
       autoSubstRelDesc n hole₁ >>
       autoSubstRelDesc n hole₂
 
+    tryProd = tryBinary (quote SubstRelDesc.prod)
     trySigma = tryBinary (quote SubstRelDesc.sigma)
     tryPi = tryBinary (quote SubstRelDesc.pi)
 
@@ -263,7 +284,7 @@ mutual
   autoDUARelDesc : ℕ → R.Term → R.TC Unit
   autoDUARelDesc zero hole = R.typeError [ R.strErr "Out of fuel" ]
   autoDUARelDesc (suc n) hole =
-    tryConstant <|> tryEl <|> trySigma <|> tryPiˢ <|> tryPi <|> useGeneric
+    tryConstant <|> tryEl <|> tryProd <|> trySigma <|> tryPiˢ <|> tryPi <|> useGeneric
     where
     tryConstant : R.TC Unit
     tryConstant =
@@ -285,6 +306,7 @@ mutual
       autoDUARelDesc n hole₁ >>
       autoDUARelDesc n hole₂
 
+    tryProd = tryBinary (quote DUARelDesc.prod)
     trySigma = tryBinary (quote DUARelDesc.sigma)
     tryPi = tryBinary (quote DUARelDesc.pi)
 

diff --git a/Cubical/Displayed/Sigma.agda b/Cubical/Displayed/Sigma.agda
@@ -99,3 +99,20 @@ module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
   𝒮ˢ-Σ .uaˢ p _ =
     fromPathP
       (DUARel.uaᴰ (𝒮ᴰ-Σ (Subst→DUA 𝒮ˢ-B) (Subst→DUA 𝒮ˢ-C))  _ p _ .fst (refl , refl))
+
+-- SubstRel on a non-dependent product
+
+module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
+  {B : A → Type ℓB} (𝒮ˢ-B : SubstRel 𝒮-A B)
+  {C : A → Type ℓC} (𝒮ˢ-C : SubstRel 𝒮-A C)
+  where
+
+  open UARel 𝒮-A
+  open SubstRel
+  private
+    module B = SubstRel 𝒮ˢ-B
+    module C = SubstRel 𝒮ˢ-C
+
+  _×𝒮ˢ_ : SubstRel 𝒮-A (λ a → B a × C a)
+  _×𝒮ˢ_ .act p = ≃-× (B.act p) (C.act p)
+  _×𝒮ˢ_ .uaˢ p (b , c) = ΣPathP (B.uaˢ p b , C.uaˢ p c)