For some reason Agda could no longer infer for idp, added explicit

1 files changed, 15 insertions, 14 deletions

diff --git a/Univalence-to-funext.agda b/Univalence-to-funext.agda
index c2935b2..edec07a 100644
--- a/Univalence-to-funext.agda
+++ b/Univalence-to-funext.agda
@@ -33,7 +33,7 @@ module _ {i j} {A : Type i} {B : A → Type j} where
   Σ=≃pair : {v w : Σ A B} → (v == w) ≃ (Σ-path-pair v w)
   Σ=≃pair = equiv Σ=→pair pair→Σ= pair→Σ=→pair Σ=→pair→Σ=
 
-               
+
 --============================================================================--
 --                           Univalence
 
@@ -44,7 +44,7 @@ postulate
   ua : ∀ {i} {A B : Type i} → (A ≃ B) → (A == B)
   idtoeqv-ua-β : ∀ {i} {A B : Type i} (e : A ≃ B) → idtoeqv (ua e) == e
 
-eqv-post∘ : ∀ {i} {A B : Type i} {C : Type i} (p : A == B) → 
+eqv-post∘ : ∀ {i} {A B : Type i} {C : Type i} (p : A == B) →
             fst (idtoeqv (ap (λ T → (C → T)) p)) == _∘_ (fst (idtoeqv p))
 eqv-post∘ idp = idp
 
@@ -92,7 +92,7 @@ contr-retract : ∀ {i} {A B : Type i}
 contr-retract r s h p = has-level-in
                       ((r (fst c)) , λ y → ap r (snd c (s y)) ∙ h y)
                       where c = has-level-apply p
-                      
+
 module _ {i j} {A : Type i} {B : Type j} where
   is-contr-map : (f : A → B) → Type (lmax i j)
   is-contr-map f = (y : B) → is-contr (hfiber f y)
@@ -118,7 +118,7 @@ module _ {i j} {A : Type i} {B : Type j} where
       β : g ∘ f ∼ (idf A)
       β a = fst (Σ=→pair (snd (has-level-apply (c (f a))) (a , idp)))
 
-      
+
 
   equiv-is-contr-map : {f : A → B} → (is-equiv f → is-contr-map f)
   equiv-is-contr-map {f = f} e b =
@@ -132,7 +132,7 @@ module _ {i j} {A : Type i} {B : Type j} where
 
       β : f ∘ g ∼ (idf B)
       β = is-equiv.f-g e
-      
+
       hf : hfiber f b
       hf = ((g b) , (β b))
 
@@ -147,19 +147,22 @@ module _ {i j} {A : Type i} {B : Type j} where
         ! (ap f  (fc (a , p))) ∙ (β b)
           =⟨ ap ! (ap-∙ f (ap g (! p)) (α a)) ∙2 idp ⟩
         ! (ap f (ap g (! p)) ∙ ap f (α a)) ∙ (β b)
-          =⟨ ap ! (idp ∙2 is-equiv.adj e a) ∙2 idp {a = β b}⟩
+        =⟨ ap ! (idp {a = ap f (ap g (! p))} ∙2 is-equiv.adj e a) ∙2
+           idp {a = β b} ⟩
         ! (ap f (ap g (! p)) ∙ (β (f a))) ∙ (β b)
           =⟨ ap ! (∘-ap f g (! p) ∙2 idp) ∙2 idp ⟩
         ! (ap (f ∘ g) (! p) ∙ (β (f a))) ∙ (β b)
           =⟨ !-∙ (ap (f ∘ g) (! p)) (β (f a)) ∙2 idp ⟩
         (! (β (f a)) ∙ ! (ap (λ x → f (g x)) (! p))) ∙ (β b)
-          =⟨ (idp ∙2 !-ap (f ∘ g) (! p)) ∙2 idp {a = β b}⟩
+          =⟨ (idp {a = ! (β (f a))} ∙2 !-ap (f ∘ g) (! p)) ∙2 idp {a = β b} ⟩
         (! (β (f a)) ∙ (ap (f ∘ g) (! (! p)))) ∙ (β b)
-          =⟨ (idp ∙2 ap (ap (f ∘ g)) (!-! p)) ∙2 idp {a = β b} ⟩
+          =⟨ (idp {a = ! (β (f a))} ∙2 ap (ap (f ∘ g)) (!-! p)) ∙2
+             idp {a = β b} ⟩
         (! (β (f a)) ∙ (ap (f ∘ g) p)) ∙ (β b)
           =⟨ ∙-assoc (! (β (f a))) (ap (f ∘ g) p) (β b) ⟩
         ! (β (f a)) ∙ (ap (f ∘ g) p ∙ (β b))
-          =⟨ idp {a = ! (β (f a))} ∙2 (nat-lemma p β ∙ (idp ∙2 ap-idf p)) ⟩
+         =⟨ idp {a = ! (β (f a))} ∙2
+            (nat-lemma p β ∙ idp {a = β (f a)} ∙2 ap-idf p) ⟩
         ! (β (f a)) ∙ (β (f a) ∙ p)
           =⟨ ! (∙-assoc (! (β (f a))) (β (f a)) p) ⟩
         (! (β (f a)) ∙ β (f a)) ∙ p
@@ -167,8 +170,6 @@ module _ {i j} {A : Type i} {B : Type j} where
         p
           =∎
 
-      
-
 --============================================================================--
 --                        Univalence implies funext
 
@@ -178,7 +179,7 @@ module _ {i} {A : Type i} {B : A → Type i} {f : Π A B} where
 
   graphType : Type i
   graphType = Σ A image
-  
+
   prA : graphType → A
   prA = fst
 
@@ -191,7 +192,7 @@ module _ {i} {A : Type i} {B : A → Type i} {f : Π A B} where
 
       β : (a : graphType) → (fst a , f (fst a), idp) == a
       β (a , b , p) = pair→Σ= (idp , (pair→Σ= (p , (tr-post-concat idp))))
-                
+
   fibreOverId : Type i
   fibreOverId = hfiber (_∘_ prA) (idf A)
 
@@ -203,7 +204,7 @@ module _ {i} {A : Type i} {B : A → Type i} {f : Π A B} where
 
         pβ : fst (idtoeqv p) == prA
         pβ = ap fst (idtoeqv-ua-β prA-is-equiv)
-        
+
         prA∘-is-equiv : is-contr-map (λ g → prA ∘ g)
         prA∘-is-equiv = transport is-contr-map
                          (eqv-post∘ p ∙ ap (λ x → _∘_ x) pβ)