agda-gset/Category/G-Sets/Properties/A4.agda

{-# OPTIONS --irrelevant-projections #-}
open import Algebra.G-Set
open import Algebra.Group
open import Category.G-Sets
open import Categories.Category.Instance.Sets
open import Categories.Functor.Core
open import Categories.Category.Core
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
open import Relation.Binary.PropositionalEquality.Properties
open import Relation.Binary.PropositionalEquality.WithK
open import Axiom.UniquenessOfIdentityProofs.WithK
open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.Dependent.WithK
open import Data.Product.Relation.Binary.Pointwise.Dependent
open import Data.Product.Properties renaming (Σ-≡,≡→≡ to peq)
open import Level


module Category.G-Sets.Properties.A4 {ℓ} (G : Group ℓ) where

  open Functor
  open G-Set-Morphism using () renaming (u to <_>)
  D : Functor (Sets ℓ) (G-Sets G)
  D .F₀ S = record
    { X = S
    ; _⊳_ = λ _ s → s
    ; ε⊳ = ≡.refl
    ; ∘⊳ = ≡.refl
    }
  D .F₁ {A} {B} f = record
    { u = f
    ; equivariance = ≡.refl
    }
  D .identity = ≡.refl
  D .homomorphism = ≡.refl
  D .F-resp-≈ f≡g = f≡g

  V : Functor (G-Sets G) (Sets ℓ)
  V .F₀ GS = Orb
    where
      open G-Set GS
  V .F₁ {A} {B} f O = Orb[ < f > O.x , G-Set.orb[ (< f > o.y) , o.g , (≡.trans (≡.sym f.equivariance) (≡.cong < f > o.eq)) ] ]
  -- V .F₁ {A} {B} f (x , (y , (g , eq))) = (< f > x , (< f > y , (g , ≡.trans (≡.sym f.equivariance) (≡.cong < f > eq))))
    where
      open G-Set A using () renaming (Orb to OrbA; orb to orbA; Orb[_,_] to OrbA[_,_])
      open G-Set B using (Orb[_,_]; orb[_,_,_]) renaming (Orb to OrbB; orb to orbB)
      module f = G-Set-Morphism f
      module O = OrbA O
      module o = orbA O.o
  V .identity {GS} {O} = Orb-intro ≡.refl ≡.refl
    where
    open G-Set GS

  -- V .identity {GS} {(x , (y , (g , ≡.refl)))} = ≡.refl
  V .homomorphism {X} {Y} {Z} {f} {g} {O} = Orb-intro ≡.refl ≡.refl
    where
    open G-Set Z
  -- TODO needs something like subst-application, but for orb...
  V .F-resp-≈ {A} {B} {f} {g} eq {O} = {!!}
  -- V .F-resp-≈ {A} {B} {f} {g} eq {(x , (y , (h , ≡.refl)))} = peq ((eq {x}) , {!!})
    where
      module f = G-Set-Morphism f hiding (u)
      module g = G-Set-Morphism g hiding (u)
      module A = G-Set A
      open G-Set A using () renaming (Orb to OrbA; orb to orbA)
      open G-Set B using () renaming (Orb[_,_] to OrbB[_,_]; orb[_,_,_] to orbB[_,_,_]; Orb-intro to Orb-introB; orb-intro to orb-introB)
      module O = OrbA O
      module o = orbA O.o
      helper : (e : < f > O.x ≡ < g > O.x) → (≡.subst (G-Set.orb B) (eq {O.x}) orbB[ < f > o.y , o.g , _ ]) ≡ orbB[ < f > o.y , o.g , _ ]
      helper e = {!!}