Add 2 argument version of ua→ (#713)

agda · Feb 3, 2022 · ccf7c01 · ccf7c01
1 parent 9acdecf
commit ccf7c01
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/Cubical/Foundations/Univalence.agda b/Cubical/Foundations/Univalence.agda
@@ -263,6 +263,14 @@ ua→⁻ {e = e} {f₀ = f₀} {f₁} p a i =
       })
     (p i (transp (λ j → ua e (j ∧ i)) (~ i) a))
 
+ua→2 : ∀ {ℓ ℓ' ℓ''} {A₀ A₁ : Type ℓ} {e₁ : A₀ ≃ A₁}
+  {B₀ B₁ : Type ℓ'} {e₂ : B₀ ≃ B₁}
+  {C : (i : I) → Type ℓ''}
+  {f₀ : A₀ → B₀ → C i0} {f₁ : A₁ → B₁ → C i1}
+  → (∀ a b → PathP C (f₀ a b) (f₁ (e₁ .fst a) (e₂ .fst b)))
+  → PathP (λ i → ua e₁ i → ua e₂ i → C i) f₀ f₁
+ua→2 h = ua→ (ua→ ∘ h)
+
 -- Useful lemma for unfolding a transported function over ua
 -- If we would have regularity this would be refl
 transportUAop₁ : ∀ {A B : Type ℓ} → (e : A ≃ B) (f : A → A) (x : B)