{-# OPTIONS --without-K #-}
open import FunUniverse.Core
open import Data.Two
module FunUniverse.Interface.Two
         {t} {T : Set t} (funU : FunUniverse T) where
open FunUniverse funU

record FunTwo : Set t where

  field
    -- already part of a record
    <0₂> <1₁> :  {_𝟙}  _𝟙 `→ `𝟚

    <not> : `𝟚 `→ `𝟚

    const𝟚 :  {_𝟙}  𝟚  _𝟙 `→ `𝟚

    <0,_> :  {A B}  (A `→ B)  A `→ `𝟚  B

    <1,_> :  {A B}  (A `→ B)  A `→ `𝟚  B

    <0,> :  {A}  A `→ `𝟚  A

    <1,> :  {A}  A `→ `𝟚  A

    <0,1> :  {_𝟙}  _𝟙 `→ `𝟚  `𝟚

    <xor> : `𝟚  `𝟚 `→ `𝟚

    <or> : `𝟚  `𝟚 `→ `𝟚

    <and> : `𝟚  `𝟚 `→ `𝟚

    <==ᵇ> : `𝟚  `𝟚 `→ `𝟚

    half-adder : `𝟚  `𝟚 `→ `𝟚  `𝟚

    full-adder : `𝟚  `𝟚  `𝟚 `→ `𝟚  `𝟚