Exercise 2.11 from the HoTT book

Pullback.agda

{-# OPTIONS --without-K #-}
open import Agda.Primitive renaming (Set to Type)
open import Data.Product
open import Data.Product.Properties
open import Function.Base
open import Relation.Binary.PropositionalEquality
open import Axiom.Extensionality.Propositional

module Pullback (funext : Extensionality _ _) where

module _ {A B C : Type} (f : A → C) (g : B → C) where
  Pullback = Σ A λ a → Σ B λ b → f a ≡ g b

  π₁ : Pullback → A
  π₁ (a , b , p) = a

  π₂ : Pullback → B
  π₂ (a , b , p) = b

  square : ∀ x → f (π₁ x) ≡ g (π₂ x)
  square (a , b , p) = p

module _ {A B C : Type} (f : A → C) (g : B → C) (X : Type) where
  φ : (X → Pullback f g) → Pullback {X → A} {X → B} {X → C} (f ∘_) (g ∘_)
  φ h = π₁ f g ∘ h , π₂ f g ∘ h , funext (square f g ∘ h)

  φ⁻¹ : Pullback {X → A} {X → B} {X → C} (f ∘_) (g ∘_) → (X → Pullback f g)
  φ⁻¹ (p₁ , p₂ , sq) x = p₁ x , p₂ x , cong (λ f → f x) sq

  φ-φ⁻¹ : ∀ f → φ (φ⁻¹ f) ≡ f
  φ-φ⁻¹ (p₁ , p₂ , sq) = Σ-≡,≡→≡ (refl , Σ-≡,≡→≡ (refl , {! funext ∘ happly ≡ id  !}))

  φ⁻¹-φ : ∀ f → φ⁻¹ (φ f) ≡ f
  φ⁻¹-φ f = funext (λ x → Σ-≡,≡→≡ (refl , Σ-≡,≡→≡ (refl , {! happly ∘ funext ≡ id  !})))