在Coq中有（ - >）的顯式類型構造函數嗎？

Question

我想定義一個提供身份和組成的類。除了其他有用的實例（List with nil and concatenation;與關係，好，身份和組合;-)），我想有一個函數實例。

鑑於

Class Cat (C0 : Type) (C1 : C0 -> C0 -> Type) := 
    { identity : forall a, C1 a a 
    ; compose : forall {a b c : C0}, C1 b c -> C1 a b -> C1 a c 
    (* snip: some laws *) 
    }. 

我希望能夠定義像

Instance Cat (->) := { ... }. 

但在勒柯克運營商不一樣，一起想。首先我假設->是一個符號，但Locate "_ -> _".聲稱這是一個Unknown notation。使用fun a b => a -> b有點作品，但類型看起來很有趣。

> Check (identity nat). 
identity nat 
    : (fun a b : Type => a -> b) nat nat 

（同去的Eval compute in，看來它並沒有簡化的類型。）我寧願更具可讀性identity nat : nat -> nat。 （目前，這些類型對於我正在做的事情來說變得不可讀）

有沒有辦法讓'原始'->或至少說服Coq給我更好的類型？

---

附註：我建立了很多代表評價語義Inductive，那是我的目標是「正常」的編程語言的子集映射到勒柯克和背部，傳輸安全約束和做魔術。我不得不一遍又一遍地用不同的構造函數來證明相同的東西，並希望這能讓我證明一次又一次的東西。我認爲類別是抽象的正確方法。我在這裏包括這個筆記，以防萬一我錯了，也許有更好的方法來避免整個->問題。

Answer 1

我只能回答部分問題。 ->不是像+和exists和{ ... | ... }這樣的標記，它是內置在解析器中的，如forall。語法a -> b相當於forall x:a, b當x不b（我不知道，如果它在任何情況下都等同，可能會有用途，其中x不能b發生，你必須使用->）免費。

原因是函數抽象和應用，並執行它們的類型，是Coq的基礎，它們不是從更原始的概念派生的。您不能直接使用fun，應用程序->或forall，因爲它們不是一流的對象。

這就是說，類型類是一種專門用於應用程序的方法。我不熟悉他們，所以我不知道是否有辦法做你想做的事情。