cases producing metavariables

cases.hlean

open eq is_trunc

context
  parameters (X A C : Type) [Xtrunc : is_trunc 2 X]
    [Atrunc : is_trunc 1 A] [Cset : is_hset C]
    (ι' : A → X) (ι : C → A)

  definition fund_dbl_precat_flat_comp₁ {a₁ b₁ a₂ b₂ a₃ b₃ : X}
    {f₁ : a₁ = b₁} {g₁ : a₂ = b₂} {h₁ : a₁ = a₂} {i₁ : b₁ = b₂}
    {g₂ : a₃ = b₃} {h₂ : a₂ = a₃} {i₂ : b₂ = b₃}
    (v : h₂ ⬝ g₂ = g₁ ⬝ i₂)
    (u : h₁ ⬝ g₁ = f₁ ⬝ i₁) :
    (h₁ ⬝ h₂) ⬝ g₂ = f₁ ⬝ (i₁ ⬝ i₂) :=
  calc (h₁ ⬝ h₂) ⬝ g₂ = h₁ ⬝ (h₂ ⬝ g₂) : con.assoc
                 ... = h₁ ⬝ (g₁ ⬝ i₂) : v
                 ... = (h₁ ⬝ g₁) ⬝ i₂ : con.assoc'
                 ... = (f₁ ⬝ i₁) ⬝ i₂ : u
                 ... = f₁ ⬝ (i₁ ⬝ i₂) : con.assoc

  include Atrunc
  definition fund_dbl_precat_thin_comp₁_aux  {a b c₁ d₁ c₂ d₂ : A}
    (f₁ : a = b) (g₁ : c₁ = d₁) (h₁ : a = c₁) (i₁ : b = d₁)
    (g₂ : c₂ = d₂) (h₂ : c₁ = c₂) (i₂ : d₁ = d₂)
    (pv : h₂ ⬝ g₂ = g₁ ⬝ i₂) (pu : h₁ ⬝ g₁ = f₁ ⬝ i₁)
    (px : (h₁ ⬝ h₂) ⬝ g₂ = f₁ ⬝ (i₁ ⬝ i₂)) :
    transport (λ x, _ = _ ⬝ x) (inverse (ap_con ι' i₁ i₂))
      (transport (λ x, x ⬝ _ = _) (inverse (ap_con ι' h₁ h₂))
          (fund_dbl_precat_flat_comp₁
             (concat
                (concat (inverse (ap_con ι' h₂ g₂))
                   (transport (λ x, eq (ap ι' (concat h₂ g₂)) (ap ι' x)) pv
                      (refl (ap ι' (concat h₂ g₂)))))
                (ap_con ι' g₁ i₂))
             (concat
                (concat (inverse (ap_con ι' h₁ g₁))
                   (transport (λ x, _ = ap ι' x) pu (refl (ap ι' (concat h₁ g₁)))))
                (ap_con ι' f₁ i₁))))
    = (concat
       (concat (inverse (ap_con ι' (concat h₁ h₂) g₂))
          (transport (λ x, eq (ap ι' (concat (concat h₁ h₂) g₂)) (ap ι' x)) px
             (refl (ap ι' (concat (concat h₁ h₂) g₂)))))
       (ap_con ι' f₁ (concat i₁ i₂))) :=
  begin
    esimp {fund_dbl_precat_flat_comp₁},
    cases i₂, cases i₁,
    cases h₂, cases h₁,
    cases g₂, cases px, cases pv,
    assert P1 : pu = (refl (refl d₂)),
      exact (@is_hset.elim (d₂ = d₂) (@is_trunc_eq A 0 Atrunc d₂ d₂)
        (refl d₂) (refl d₂) pu (refl (refl d₂))),
    rewrite P1,
  end

end