{- Use with Andrea Vezzosi's agda-flat -}
{-# OPTIONS --no-pattern-matching --rewriting #-}

-- Some standard Agda definitions
open import agda.prelude
-- Some standard Agda-flat definitions
open import agda-flat.prelude
-- Definition 2.2
open import agda.fibration


module agda-flat.tiny
  -- the path functor is a parameter
  ( :{}
    {l : Level}
    (Γ : Set l)
     ---------
    Set l)
  (℘` :{}
    {l m : Level}
    {Γ : Set l}
    {Δ : Set m}
    (γ : Δ  Γ)
     -----------
     Δ   Γ)
  (℘`comp :{}
    {l m n : Level}
    {Γ : Set l}
    {Δ : Set m}
    {Θ : Set n}
    (γ : Δ  Γ)
    (σ : Θ  Δ)
    (p :  Θ)
     -----------
    ℘` γ (℘` σ p)  ℘` (γ  σ) p)
  where

----------------------------------------------------------------------
-- Instantiating this module with a path object functor, ℘, asserts
-- that ℘ has a right adjoint, √. For ℘ = 𝕀 → (_) this follows from
-- the fact that the interval is tiny.
----------------------------------------------------------------------
postulate
  -- the value of the right adjoint on objects
    :
    {l :{} Level}
    (A :{} Set l)
     ------------
    Set l
  -- right transposition across the adjunction 
  R  :
    {l l' :{} Level}
    {A :{} Set l}
    {B :{} Set l'}
    (f :{}  A  B)
     ---------------
    A   B
  -- left transposition across the adjunction
  L  :
    {l l' :{} Level}
    {A :{} Set l}
    {B :{} Set l'}
    (g :{} A   B)
     --------------
     A  B
  -- right and left transposition are mutually inverse
  LR :
    {l l' :{} Level}
    {A :{} Set l}
    {B :{} Set l'}
    {f :{}  A  B}
     ---------------
    L (R f)  f
  RL :
    {l l' :{} Level}
    {A :{} Set l}
    {B :{} Set l'}
    {g :{} A   B}
     ---------------
    R (L g)  g
  -- one-sided naturality of right transposition
  R℘ :
    {l l' l'' :{} Level}
    {A :{} Set l}
    {B :{} Set l'}
    {C :{} Set l''}
    (g :{} A  B)
    (f :{}  B  C)
     --------------------
    R (f  ℘` g)  R f  g

{-# REWRITE LR RL #-}
{- 
The use of these REWRITES is not necessary, but it does simplify
proofs of equality in the paper by making some of the steps
computational. The proof of L℘ below is an example.
-}

-- One-sided naturality of left transposition is derivable
L℘ :
  {l l' l'' :{} Level}
  {A :{} Set l}
  {B :{} Set l'}
  {C :{} Set l''}
  (f :{} B   C)
  (g :{} A  B)
   --------------------
  L f  ℘` g  L (f  g)
L℘ f g = cong♭ L (R℘ g (L f))
{- 
Here is the proof without declaring LR and RL to be REWRITES:
     proof
       (L f ∘ ℘` g)
     ≡[ symm LR  ]
       L (R (L f ∘ ℘` g))
     ≡[ cong♭ L (R℘ g (L f)) ]
       L (R (L f) ∘ g)
     ≡[ cong♭ (λ h → L (h ∘ g)) RL ]
       L (f ∘ g)
     qed
-}
  
-- Functoriality of √
√` :
  {l l' :{} Level}
  {A :{} Set l}
  {B :{} Set l'}
  (f :{} A  B)
   ---------------
   A   B
√` f = R (f  L id)

-- The other naturality property of right transposition
√R :
  {l l' l'' :{} Level}
  {A :{} Set l}
  {B :{} Set l'}
  {C :{} Set l''}
  (g :{} B  C)
  (f :{}  A  B)
   --------------------
  √` g  R f  R (g  f)
√R g f =
  proof
    R (g  L id)  R f
  ≡[ symm (R℘ (R f) (g  L id)) ]
    R (g  L id  ℘`(R f))
  ≡[ cong♭  h  R (g  h)) (L℘ id (R f)) ]
    R (g  f)
  qed

-- The other naturality property of left transposition
L√ :
  {l l' l'' :{} Level}
  {A :{} Set l}
  {B :{} Set l'}
  {C :{} Set l''}
  (g :{} B  C)
  (f :{} A   B)
   ---------------------
  g  L f   L (√` g  f)
L√ g f = cong♭ L (symm (√R g (L f)))