~tslil/univalence-to-funext

5aefd676fb53018c77a9735ffde8bedc05ad5bb0 — tslil clingman 1 year, 6 months ago dd01e95
For some reason Agda could no longer infer for idp, added explicit
1 files changed, 15 insertions(+), 14 deletions(-)

M Univalence-to-funext.agda
M Univalence-to-funext.agda => Univalence-to-funext.agda +15 -14
@@ 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β)