{-# OPTIONS --without-K --rewriting --overlapping-instances --instance-search-depth=4 #-}

open import lib.Basics
open import lib.types.LoopSpace
open import 2Grp
open import 2GrpMap
open import 2GrpMap-conv
open import 2SGrpMap
open import Hmtpy2Grp
open import KFunctor
open import LoopK-hom
import Delooping
open import Biadj-data.Loop-zig-zag-defs
open import Biadj-data.Loop-zig-zag-aux2a
open import Biadj-data.Loop-zig-zag-aux2b-defs

module Biadj-data.Loop-zig-zag-aux2b where

module Loop-zz-aux2b {i j} {X : Type i} {Y : Type j} {{ηX : has-level  X}} {{ηY : has-level  Y}} {x₀ : X} {y₀ : Y}
  (f : ⊙[ X , x₀ ] ⊙→ ⊙[ Y , y₀ ]) where
  
  open Delooping
  open Loop-zz-defs f
  open Loop-zz-aux2a f
  open Loop-zz-aux2b-defs f

  instance
  
    _ : has-level  (base (Ω ⊙[ X , x₀ ]) == base (Ω ⊙[ X , x₀ ]))
    _ = has-level-apply-instance {{K₂-is-2type (Ω ⊙[ X , x₀ ])}}

    _ : has-level  (base (Ω ⊙[ Y , y₀ ]) == base (Ω ⊙[ Y , y₀ ]))
    _ = has-level-apply-instance {{K₂-is-2type (Ω ⊙[ Y , y₀ ])}}

  abstract

    ρ₂-translate0 :
      ρ₂
        =ₛ
      ap (λ m → Loop2Grp-map f ∘2G m) (Loop-zz₀ x₀) ◃∙
      natiso2G-to-== ρ₂-trans-mid ◃∙
      ! (ap (λ m → m ∘2G Loop2Grp-map f) (Loop-zz₀ y₀)) ◃∎
    ρ₂-translate0 =
      ρ₂
        =ₛ₁⟨  &  & ρ₂-mid-translate ⟩
      ap (λ m → Loop2Grp-map f ∘2G m) (Loop-zz₀ x₀) ◃∙
      natiso2G-to-== ρ₂-trans-mid ◃∙
      ! (ap (λ m → m ∘2G Loop2Grp-map f) (Loop-zz₀ y₀)) ◃∎ ∎ₛ

    ρ₂-translate1 :
      ap (λ m → Loop2Grp-map f ∘2G m) (Loop-zz₀ x₀) ◃∙
      natiso2G-to-== ρ₂-trans-mid ◃∙
      ! (ap (λ m → m ∘2G Loop2Grp-map f) (Loop-zz₀ y₀)) ◃∎
        =ₛ
      ap (λ m → Loop2Grp-map f ∘2G m) (Loop-zz₀ x₀) ◃∙
      natiso2G-to-== ρ₂-trans-mid ◃∙
      τ₁ ◃∎
    ρ₂-translate1 =
      ap (λ m → Loop2Grp-map f ∘2G m) (Loop-zz₀ x₀) ◃∙
      natiso2G-to-== ρ₂-trans-mid ◃∙
      ! (ap (λ m → m ∘2G Loop2Grp-map f) (Loop-zz₀ y₀)) ◃∎
        =ₛ₁⟨  &  & ! (!-whisk2G-conv-r {f₁ = Loop2Grp-map f} (Loop-zz₀-iso y₀)) ⟩
      ap (λ m → Loop2Grp-map f ∘2G m) (Loop-zz₀ x₀) ◃∙
      natiso2G-to-== ρ₂-trans-mid ◃∙
      τ₁ ◃∎ ∎ₛ

    ρ₂-translate2 :
      ap (λ m → Loop2Grp-map f ∘2G m) (Loop-zz₀ x₀) ◃∙
      natiso2G-to-== ρ₂-trans-mid ◃∙
      τ₁ ◃∎
        =ₛ
      τ₀ ◃∙
      natiso2G-to-== ρ₂-trans-mid ◃∙
      τ₁ ◃∎
    ρ₂-translate2 =
      ap (λ m → Loop2Grp-map f ∘2G m) (Loop-zz₀ x₀) ◃∙
      natiso2G-to-== ρ₂-trans-mid ◃∙
      τ₁ ◃∎
        =ₛ₁⟨  &  & ! (whisk2G-conv-l {f₂ = Loop2Grp-map f} (Loop-zz₀-iso x₀)) ⟩
      τ₀ ◃∙
      natiso2G-to-== ρ₂-trans-mid ◃∙
      τ₁ ◃∎ ∎ₛ