open import 1Lab.Reflection.Subst
open import 1Lab.Reflection

open import Cat.Instances.Shape.Terminal
open import Cat.Functor.Naturality
open import Cat.Reasoning
open import Cat.Prelude

module Cat.Functor.Naturality.Reflection where

module _ {o  o' ℓ'} {C : Precategory o } {D : Precategory o' ℓ'} where

  -- Tactic worker for filling in trivial natural isomorphisms F ≅ⁿ G.
  --
  -- The assumptions are:
  -- 1. ∀ x, F .F₀ x is definitionally equal to G .F₀ x
  -- 2. ∀ f, F .F₁ f is extensionally equal (by `trivial!`) to G .F₁ f
  --    OR C = ⊤Cat
  --
  -- The functor arguments are only used for type inference.
  trivial-isoⁿ : (F G : Functor C D)  Term  TC 
  trivial-isoⁿ _ _ hole = do
    `C  quoteTC C
    `D  quoteTC D
    wait-just-a-bit `C >>= unify hole  λ where
      (def₀ (quote ⊤Cat))  def₀ (quote !const-isoⁿ)
        ##ₙ (def₀ (quote id-iso) ##ₙ `D)
      _  def₀ (quote iso→isoⁿ)
        ##ₙ vlam "" (def₀ (quote id-iso) ##ₙ raise 1 `D)
        ##ₙ vlam ""
          (def₀ (quote _··_··_)
            ##ₙ (def₀ (quote idr) ##ₙ raise 1 `D ##ₙ unknown)
            ##ₙ def₀ (quote trivial!)
            ##ₙ (def₀ (quote sym)
              ##ₙ (def₀ (quote idl) ##ₙ raise 1 `D ##ₙ unknown)))

  trivial-isoⁿ!
    :  {F G : Functor C D}
     {@(tactic trivial-isoⁿ F G) is : F ≅ⁿ G}
     F ≅ⁿ G
  trivial-isoⁿ! {is = is} = is

-- Tests

module _ {o } {C : Precategory o } where

  _ :  {F : Functor C C}  F ≅ⁿ F
  _ = trivial-isoⁿ!

  _ :  {K : Functor ⊤Cat C}  !Const (K .Functor.F₀ _) ≅ⁿ K
  _ = trivial-isoⁿ!