-- This file:
--   http://angg.twu.net/AGDA/2022HuC3.agda.html
--   http://angg.twu.net/AGDA/2022HuC3.agda
--           (find-angg "AGDA/2022HuC3.agda")
-- file:///home/edrx/TH/L/AGDA/2022HuC3.agda.html
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
-- Version: 20220207
-- Public domain.
--
-- (find-angg "AGDA/find-agdatype.el")
--
-- (defun a2 () (interactive) (find-angg "AGDA/2022HuC2.agda"))
-- (defun a3 () (interactive) (find-angg "AGDA/2022HuC3.agda"))
-- (defun a  () (interactive) (find-angg "AGDA/2022HuC3.agda"))

module 2022HuC3 where

open import Level
open import Function.Base using (flip)
open import Relation.Binary using (Rel; IsEquivalence)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
open import Categories.Category.Core
open import Categories.Functor.Core

postulate catA : Category zero zero zero
postulate catB : Category zero zero zero
postulate R    : Functor catB catA

module A = Category catA
module B = Category catB
module R = Functor R

postulate A : A.Obj
postulate C : B.Obj
postulate η : A A.⇒ (R.₀ C)

-- (find-agdatype "R.₀ C")
-- (find-agdatype "A A.⇒ (R.₀ C)")



-- Local Variables:
-- coding:  utf-8-unix
-- End: