{-# OPTIONS --safe --without-K #-}

open import Algebra.Bundles using (Group)
module Algebra.Group.Reasoning {g₁ gβ‚‚} (𝓖 : Group g₁ gβ‚‚) where

open import Algebra.Group.Symmetric 𝓖
open import Algebra.Group.Symmetric.Equality 𝓖
open import Algebra.Group.Symmetric.Inclusion 𝓖 public
open import Algebra.Group.Symmetric.PartialEquality 𝓖

open Group PartSymGroup hiding (_β‰ˆ_)
open Group 𝓖 using (_β‰ˆ_)

applyAt : βˆ€ f {g} before after β†’ f ≣ g β†’ before ∘ f ∘ after ≣' before ∘ g ∘ after
applyAt f {g} before after p = βˆ™-congΚ³ {after} {before ∘ f} {before ∘ g} lem
 where
  lem : before ∘ f ≣' before ∘ g
  lem = βˆ™-congΛ‘ {before} {f} {g} (weaken p)

applyAtT : βˆ€ f {g} before after {h}
         β†’ f ≣ g
         β†’ before ∘ g ∘ after ≣' h
         β†’ before ∘ f ∘ after ≣' h
applyAtT f {g} before after p rest = ≣'-trans {before ∘ f ∘ after} {before ∘ g ∘ after} (applyAt f before after p) rest

applyAtT' : βˆ€ f {g} before after {h}
          β†’ g ≣ f
          β†’ before ∘ g ∘ after ≣' h
          β†’ before ∘ f ∘ after ≣' h
applyAtT' f before after p rest = applyAtT f before after (≣-sym p) rest

applyAtTnoB : βˆ€ f {g} after {h}
            β†’ f ≣ g
            β†’ g ∘ after ≣' h
            β†’ f ∘ after ≣' h
applyAtTnoB f after p rest  = applyAtT f e after p rest

applyAtTnoB' : βˆ€ f {g} after {h}
             β†’ g ≣ f
             β†’ g ∘ after ≣' h
             β†’ f ∘ after ≣' h
applyAtTnoB' f after p rest = applyAtT' f e after p rest

applyAtTnoA : βˆ€ f {g} before {h}
            β†’ f ≣ g
            β†’ before ∘ g ≣' h
            β†’ before ∘ f ≣' h
applyAtTnoA f before p rest = applyAtT f before e p rest

applyAtTnoA' : βˆ€ f {g} before {h}
             β†’ g ≣ f
             β†’ before ∘ g ≣' h
             β†’ before ∘ f ≣' h
applyAtTnoA' f before p rest = applyAtT' f before e p rest

applyAtTnoBA : βˆ€ f {g} {h}
             β†’ f ≣ g
             β†’ g ≣' h
             β†’ f ≣' h
applyAtTnoBA f p rest = applyAtT f e e p rest

applyAtTnoBA' : βˆ€ f {g} {h}
              β†’ g ≣ f
              β†’ g ≣' h
              β†’ f ≣' h
applyAtTnoBA' f p rest = applyAtT' f e e p rest

applyAtTM : βˆ€ {g} before after {h}
          β†’ e ≣ g
          β†’ before ∘ g ∘ after ≣' h
          β†’ before ∘ e ∘ after ≣' h
applyAtTM before after p rest = applyAtT e before after p rest

applyAtTM' : βˆ€ {g} before after {h}
          β†’ g ≣ e
          β†’ before ∘ g ∘ after ≣' h
          β†’ before ∘ after ≣' h
applyAtTM' before after p rest = applyAtTM before after (≣-sym p) rest

applyAtTnoBM : βˆ€ {g} after {h}
             β†’ e ≣ g
             β†’ g ∘ after ≣' h
             β†’ after ≣' h
applyAtTnoBM after p rest = applyAtTM e after p rest

applyAtTnoBM' : βˆ€ {g} after {h}
              β†’ g ≣ e
              β†’ g ∘ after ≣' h
              β†’ after ≣' h
applyAtTnoBM' after p rest = applyAtTM' e after p rest

applyAtTnoAM : βˆ€ {g} before {h}
             β†’ e ≣ g
             β†’ before ∘ g ≣' h
             β†’ before ≣' h
applyAtTnoAM before p rest = applyAtTM before e p rest

applyAtTnoAM' : βˆ€ {g} before {h}
              β†’ g ≣ e
              β†’ before ∘ g ≣' h
              β†’ before ≣' h
applyAtTnoAM' before p rest = applyAtTM' before e p rest

applyAtTnoBAM : βˆ€ {g} {h}
              β†’ e ≣ g
              β†’ g ≣' h
              β†’ e ≣' h
applyAtTnoBAM p rest = applyAtTM e e p rest

applyAtTnoBAM' : βˆ€ {g} {h}
               β†’ g ≣ e
               β†’ g ≣' h
               β†’ e ≣' h
applyAtTnoBAM' p rest = applyAtTM' e e p rest

infixr 40 applyAtT
syntax applyAtT f before after p rest = before ∘⟨ f ⟩∘ after β‰£βŸ¨ p ⟩ rest

infixr 40 applyAtT'
syntax applyAtT' f before after p rest = before ∘⟨ f ⟩∘ after β‰£Λ˜βŸ¨ p ⟩ rest

infixr 40 applyAtTnoB
syntax applyAtTnoB f after p rest = ⟨ f ⟩∘ after β‰£βŸ¨ p ⟩ rest

infixr 40 applyAtTnoB'
syntax applyAtTnoB' f after p rest = ⟨ f ⟩∘ after β‰£Λ˜βŸ¨ p ⟩ rest

infixr 40 applyAtTnoA
syntax applyAtTnoA f before p rest = before ∘⟨ f βŸ©β‰£βŸ¨ p ⟩ rest

infixr 40 applyAtTnoA'
syntax applyAtTnoA' f before p rest = before ∘⟨ f βŸ©β‰£Λ˜βŸ¨ p ⟩ rest

infixr 40 applyAtTnoBA
syntax applyAtTnoBA f p rest = ⟨ f βŸ©β‰£βŸ¨ p ⟩ rest

infixr 40 applyAtTnoBA'
syntax applyAtTnoBA' f p rest = ⟨ f βŸ©β‰£Λ˜βŸ¨ p ⟩ rest

infixr 40 applyAtTM
syntax applyAtTM before after p rest = before ∘⟨⟩∘ after β‰£βŸ¨ p ⟩ rest

infixr 40 applyAtTM'
syntax applyAtTM' before after p rest = before ∘⟨⟩∘ after β‰£Λ˜βŸ¨ p ⟩ rest

infixr 40 applyAtTnoBM
syntax applyAtTnoBM after p rest = ⟨⟩∘ after β‰£βŸ¨ p ⟩ rest

infixr 40 applyAtTnoBM'
syntax applyAtTnoBM' after p rest = ⟨⟩∘ after β‰£Λ˜βŸ¨ p ⟩ rest

infixr 40 applyAtTnoAM
syntax applyAtTnoAM before p rest = before βˆ˜βŸ¨βŸ©β‰£βŸ¨ p ⟩ rest

infixr 40 applyAtTnoAM'
syntax applyAtTnoAM' before p rest = before βˆ˜βŸ¨βŸ©β‰£Λ˜βŸ¨ p ⟩ rest

infixr 40 applyAtTnoBAM
syntax applyAtTnoBAM p rest = βŸ¨βŸ©β‰£βŸ¨ p ⟩ rest

infixr 40 applyAtTnoBAM'
syntax applyAtTnoBAM' p rest = βŸ¨βŸ©β‰£Λ˜βŸ¨ p ⟩ rest

end : βˆ€ h β†’ h ≣' h
end h = ≣'-refl {h}

infixr 50 end
syntax end h = h ∎

-- begin_ : βˆ€ {g h} β†’ ⟦ g ⟧ ≣' ⟦ h ⟧ β†’ g β‰ˆ h
-- begin_ {g} {h} p = ⟦⟧-injective p'
--   where
--     p' : ⟦ g ⟧ ≣ ⟦ h ⟧
--     p' .eq = peq p

open import Algebra.Group.Reasoning.Reflection 𝓖 public