-- This file:
--   http://angg.twu.net/AGDA/Cats1.agda.html
--   http://angg.twu.net/AGDA/Cats1.agda
--           (find-angg "AGDA/Cats1.agda")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "AGDA/Cats1.agda"))
-- (find-es "agda" "selinger-records")
-- (find-es "agda" "isinverse")
-- (find-es "agda" "variable")

-- {-# BUILTIN NATURAL name #-}

open import Level
open import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning

module Cats1 where

variable ℓ₀ ℓ₁ ℓ₂ ℓ₃ : Level

-- record Cat oℓ mℓ eℓ : Set (suc (oℓ ⊔ mℓ ⊔ eℓ)) where

record Cat : Set1 where
  field
    Objs  : Set
    Hom   : Objs → Objs → Set
    id    : (A : Objs) -> (Hom A A)
    _◦_   : {A B C : Objs} -> (g : Hom B C) -> (f : Hom A B) -> (Hom A C)
    idL   : (A B : Objs) -> (f : Hom A B) -> (f ≡ f ◦ id A)
    idR   : (A B : Objs) -> (f : Hom A B) -> (id B ◦ f ≡ f)
    assoc : {A B C D : Objs}
            -> (f : Hom A B)
            -> (g : Hom B C)
            -> (h : Hom C D)
            -> (((h ◦ g) ◦ f) ≡ (h ◦ (g ◦ f)))

record Functor (A B : Cat) : Set3 where
  open Cat
  field
    -- A B      : Cat
    ac₀      : (Objs A) -> (Objs B)
    ac₁      : {C D : Objs A} -> (Hom A C D) -> (Hom B (ac₀ C) (ac₀ D))
    respid   : (C : Objs A) -> (id B (ac₀ C) ≡ ac₁ (id A C))
    respcomp : (C D E : Objs A) -> (f : Hom A C D) -> (g : Hom A D E)
               -> (ac₁ ((_◦_) A g f) ≡ (_◦_) B (ac₁ g) (ac₁ f))



record ProtoCat : Set1 where
  field
    Objs  : Set
    Hom   : Objs → Objs → Set
    id    : (A : Objs) → (Hom A A)
    _◦_   : {A B C : Objs} → (g : Hom B C) → (f : Hom A B) → (Hom A C)

record CatNess (catA : ProtoCat) : Set2 where
  field
    x : Set
    
    -- idL : (A B : ProtoCat.Objs catA) -> Set
    -- idL   : (A B : Objs) -> (f : Hom A B) -> (f ≡ f ◦ id A)
    -- idR   : (A B : Objs) -> (f : Hom A B) -> (id B ◦ f ≡ f)
    -- assoc : {A B C D : Objs}
    --         -> (f : Hom A B)
    --         -> (g : Hom B C)
    --         -> (h : Hom C D)
    --         -> (((h ◦ g) ◦ f) ≡ (h ◦ (g ◦ f)))




--   oℓ mℓ eℓ : Level
-- (find-agdastdlibsrcfile "Function/Bundles.agda" "isInverse : IsInverse f f⁻¹")
-- open import Function.Structures

-- (favp 16 "freyd-with-functors")
-- (fava    "freyd-with-functors")
--
--           A
--           |    |
--           | η  |
--           v    |
--    B |-> RB    | g
--    |      |    |
--  f | |->  | Rf |
--    v      v    v
--    C |-> RC
--
--       R
--  catB -> catA
--
record Universalness
    (catA catB : Cat)
    (R   : Functor catB catA)
    (A   : Cat.Objs catA)
    (B   : Cat.Objs catB)
    (η   : Cat.Hom catA A (Functor.ac₀ R B))
      : Set (suc (suc (suc zero))) where
  field
    inv :
      (C : Cat.Objs catB) ->
      (g : Cat.Hom catA A (Functor.ac₀ R C)) ->
        (Cat.Hom catB B C)
    [B,C]-round-trip :
      ∀ (C : Cat.Objs catB) →
      ∀ (f : Cat.Hom catB B C) →
        (inv C (Cat._◦_ catA (Functor.ac₁ R f) η) ≡ f)
    [A,RC]-round-trip :
      ∀ (C : Cat.Objs catB) →
      ∀ (g : Cat.Hom catA A (Functor.ac₀ R C)) →
        (Cat._◦_ catA (Functor.ac₁ R (inv C g)) η ≡ g)

-- (favp 29 "basic-example-as-skel")
-- (fava    "basic-example-as-skel")

--
--            A
--            |    |
--            | η  |
--            v    |
--     C |-> RC    | h
--     |      |    |
--   f | |->  | Rf |
--     v      v    v
--     D |-> RD
--     |      |
--   g | |->  | Rg
--     v      v
--     E |-> RD
--
--        R
--  catB --> catA
--
--  catB[C,-]₀ = λ D    : catB . R₀ D
--  catB[C,-]₁ = λ D, E : catB .
--               λ g    : Hom_catB(D,E) .
--               λ h    :                
-- 
--               








-- (find-es "agda" "syntax")





-- variable A B : Set
-- variable f : A -> B
-- variable g : B -> A
-- variable ii : IsInverse.inverse f g



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