module Chapter2.Equality where

open import Data.Product hiding (map)

open import Relation.Binary.PropositionalEquality hiding (subst₂)



subst₂ : ∀{A : Set} {B : A → Set} (P : (a : A) → B a → Set)
          {x₁ x₂ y₁} → (q : x₁ ≡ x₂) → P x₁ y₁ → P x₂ (subst B q y₁)
subst₂ P refl p = p

cong₃ : ∀{A : Set}{B : A → Set}{C : (a : A) → B a → Set}{D : Set}
        (f : (a : A)(b : B a) → C a b → D ) 
        {x y : A}{u : B x}{s : C x u} → 
        (qa : x ≡ y) → f x u s ≡ f y (subst B qa u) (subst₂ C qa s)
cong₃ f refl = refl

{-

module Groupoid {A : Set} where
  infix 10 _∘_

  id : {a : A} → a ≡ a
  id = refl 

  _⁻¹ : {a b : A} → a ≡ b → b ≡ a
  q ⁻¹ = sym q

  _∘_ : {a b c : A} → b ≡ c → a ≡ b → a ≡ c
  q₁ ∘ q₂ = trans q₂ q₁

open Groupoid public

module Functor {A B : Set}{f : A → B} where

  map : ∀{x y} → x ≡ y → f x ≡ f y
  map = cong f

open Functor public

module Product {A : Set}{B : A → Set} where

  _,≡_ : ∀{a c : A}{b d : B a} → 
      (q : a ≡ c) → b ≡ d → (a , b) ≡ (c , subst B q d)
  refl ,≡ refl = refl

open Product public

{-
module Weak2-1Category {A : Set} where
  
  open Groupoid {A}

  infix 4 _≡₂_

  _≡₂_ : {a b : A} → (q₁ q₂ : a ≡ b) → Set
  q₁ ≡₂ q₂ = q₁ ≡ q₂

  idR : ∀{a b} → (q : a ≡ b) → q ∘ id ≡₂ q
  idR q = refl

  idL : ∀{a b} → (q : a ≡ b) → id ∘ q ≡ q
  idL refl = refl

  assoc : ∀{x y z w} → (q₁ : x ≡ y)(q₂ : y ≡ z)(q₃ : z ≡ w) →
          q₃ ∘ (q₂ ∘ q₁) ≡₂ (q₃ ∘ q₂) ∘ q₁
  assoc refl refl refl = refl

  comp : ∀{x y z}{q q' : x ≡ y}{p p' : y ≡ z} →
         q ≡₂ q' → p ≡₂ p' → p ∘ q ≡₂ p' ∘ q'
  comp refl refl = refl

module Weak2Groupoid {A : Set} where
  
  open Groupoid {A}
  open Weak2-1Category {A}

  invR : ∀{x y} → (q : x ≡ y) → q ∘ (q ⁻¹) ≡₂ id 
  invR refl = refl

  invL : ∀{x y} → (q : x ≡ y) → (q ⁻¹) ∘ q ≡₂ id
  invL refl = refl

  inv : ∀{x y}{q q' : x ≡ y} → q ≡₂ q' → q ⁻¹ ≡₂ q' ⁻¹
  inv refl = refl


module Functor {A B : Set}{f : A → B} where

  open Groupoid
  open Weak2-1Category
  open Weak2Groupoid 

  map : ∀{x y} → x ≡ y → f x ≡ f y
  map = cong f

  map2 : ∀{x y} {q q' : x ≡ y} → q ≡₂ q' → map q ≡₂ map q'
  map2 refl = refl

  map∘ : ∀{x y z} (q : x ≡ y)(q' : y ≡ z) →
         map (q' ∘ q) ≡₂ map q' ∘ map q
  map∘ refl refl = refl

  -- Derivable:

  mapId : ∀{x} → map {x} id ≡₂ id
  mapId = refl

  mapInv : ∀{x y} (q : x ≡ y) → map (q ⁻¹) ≡₂ (map q) ⁻¹
  mapInv refl = refl

module Naturality 
    {A B : Set}{f g : A → B}
    (α : (a : A) → f a ≡ g a) where

  open Groupoid
  open Weak2-1Category
  open Weak2Groupoid 
  open Functor
  
  nat : ∀{a b} → (q : a ≡ b) → 
        α b ∘ map q ≡₂ map q ∘ α a
  nat {a} refl rewrite α a = refl

--  nat2 : ∀{a} (β : (a : A) → f a ≡ g a) → 
--         α a ≡₂ β a
--  nat2 {a} β = {!!}
-}
-}