From 8d2da84b618f70f0c9c70bc580ac4c96ebfcc2f9 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 5 Sep 2018 14:45:03 +0200
Subject: [PATCH] make arguments of some definitions implicit in cubical.square

---
 hott/cubical/square.hlean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean
index dbe0724dc..cfed932e0 100644
--- a/hott/cubical/square.hlean
+++ b/hott/cubical/square.hlean
@@ -552,6 +552,7 @@ namespace eq
 
   definition square_fill_r : Σ (p : a₂₀ = a₂₂) , square p₁₀ p₁₂ p₀₁ p :=
   by induction p₁₀; induction p₁₂; exact ⟨_, !hrefl⟩
+  variables {p₁₀ p₁₂ p₀₁ p₂₁}
 
   /- Squares having an 'ap' term on one face -/
   --TODO find better names