module hott.ch2 where

open import foundation

variable
  l : Level
  A B A' B' X : UU l
  x y z : A

exercise2-1 : x ＝ y → y ＝ z → x ＝ z
exercise2-1 p q = p ∙ q
exercise2-1' : x ＝ y → y ＝ z → x ＝ z
exercise2-1' refl refl = refl

exercise2-6 : (p : x ＝ y) → is-equiv (λ (q : y ＝ z) → p ∙ q)
exercise2-6 p =
  ((λ x₁ → (inv p) ∙ x₁) , λ x₁ →
    equational-reasoning
      (_∙_ p ∘ (λ x₂ → inv p ∙ x₂)) x₁
    ＝ p ∙ (inv p ∙ x₁)
      by refl
    ＝ x₁
      by is-section-inv-concat p x₁) ,
  ((λ x₁ → (inv p) ∙ x₁) , λ x₁ →
    equational-reasoning
      ((λ x₂ → inv p ∙ x₂) ∘ _∙_ p) x₁
    ＝ inv p ∙ (p ∙ x₁)
      by refl
    ＝ x₁
      by is-retraction-inv-concat p x₁)

exercise2-9 : (A + B → X) ≃ (A → X) × (B → X)
exercise2-9 =
    (λ f → (λ z → f (inl z)) , (λ z → f (inr z)))
  , ( ( (λ g×h a+b → rec-coproduct (pr1 g×h) (pr2 g×h) a+b)
      ,  λ g×h → refl)
    ,   (λ g×h a+b → rec-coproduct (pr1 g×h) (pr2 g×h) a+b)
      ,  λ f → eq-htpy (lemma₁ f))
  where
    rec : (f : A + B → X) → (A + B → X)
    rec f = rec-coproduct (λ z → f (inl z)) (λ z → f (inr z))

    lemma₁ : (f : A + B → X) → (a+b : A + B) → (rec f) a+b ＝ f a+b
    lemma₁ f (inl a) = refl
    lemma₁ f (inr b) = refl

exercise2-17 : A ≃ A' → B ≃ B' → (A × B) ≃ (A' × B')
pr1 (exercise2-17 p q) =
  let af = pr1 p
      bf = pr1 q
  in λ a×b → af (pr1 a×b) , bf (pr2 a×b)
pr2 (exercise2-17 p q) =
  let af = pr1 p
      bf = pr1 q
      af-is-equiv = pr2 p
      bf-is-equiv = pr2 q

      af-is-inv = is-invertible-is-equiv af-is-equiv
      bf-is-inv = is-invertible-is-equiv bf-is-equiv

      af-inv = pr1 af-is-inv
      bf-inv = pr1 bf-is-inv

      do-af-inv = pr2 af-is-inv
      do-bf-inv = pr2 bf-is-inv

      inv = λ a'×b' → af-inv (pr1 a'×b') , bf-inv (pr2 a'×b')
  in (inv ,
      ind-product (λ x y →
        equational-reasoning
          (af ∘ af-inv) x , (bf ∘ bf-inv) y
        ＝ x , y
          by lemma ((af ∘ af-inv) x) x ((bf ∘ bf-inv) y) y
            (lemma₂ (eq-htpy (pr1 do-af-inv))) (lemma₂ (eq-htpy (pr1 do-bf-inv))) )),
      inv ,
      ind-product (λ x y →
        equational-reasoning
          (af-inv ∘ af) x , (bf-inv ∘ bf) y
        ＝ (x , y)
          by lemma ((af-inv ∘ af) x) x ((bf-inv ∘ bf) y) y
            (lemma₂ (eq-htpy (pr2 do-af-inv))) (lemma₂ (eq-htpy (pr2 do-bf-inv)))
     )
  where
    lemma : (a a' : A) → (b b' : B)
      → a ＝ a' → b ＝ b'
      → (a , b) ＝ (a' , b')
    lemma a a' b b' refl refl = refl
    
    lemma₂ : {f : A → A} → f ＝ id → f x ＝ x
    lemma₂ refl = refl

exercise2-17-use-univalence : {A B A' B' : UU l} → A ≃ A' → B ≃ B' → (A × B) ≃ (A' × B')
exercise2-17-use-univalence p q = equiv-eq (lemma (eq-equiv p) (eq-equiv q))
  where
    lemma : A ＝ A' → B ＝ B' → A × B ＝ A' × B'
    lemma refl refl = refl

exercise2-17-+ : {A B A' B' : UU l} → A ≃ A' → B ≃ B' → (A + B) ≃ (A' + B')
exercise2-17-+ p q = equiv-eq (lemma (eq-equiv p) (eq-equiv q))
  where
    lemma : A ＝ A' → B ＝ B' → A + B ＝ A' + B'
    lemma refl refl = refl

exercise2-17-Π : {A B A' B' : UU l} → A ≃ A' → B ≃ B' → ((x : A) → B) ≃ ((x : A') → B')
exercise2-17-Π p q = equiv-eq (lemma (eq-equiv p) (eq-equiv q))
  where
    lemma : A ＝ A' → B ＝ B' → ((x : A) → B) ＝ ((x : A') → B')
    lemma refl refl = refl