Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Category.Fin

Documentation

data Nat Source #

Constructors

Z
S Nat

data Fin n where Source #

Constructors

FZ :: Fin ('S n)
FS :: Fin n -> Fin ('S n)

Instances

Instances details

Category (LTE n :: Fin n -> Fin n -> Type) Source #
Instance details Defined in Data.Category.Fin Methods src :: forall (a :: k) (b :: k). LTE n a b -> Obj (LTE n) a Source # tgt :: forall (a :: k) (b :: k). LTE n a b -> Obj (LTE n) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). LTE n b c -> LTE n a b -> LTE n a c Source #
CartesianClosed (LTE ('S n)) => CartesianClosed (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) Source #
Instance details Defined in Data.Category.Fin Associated Types type Exponential (LTE ('S ('S n))) y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj (LTE ('S ('S n))) y -> Obj (LTE ('S ('S n))) z -> LTE ('S ('S n)) (BinaryProduct (LTE ('S ('S n))) (Exponential (LTE ('S ('S n))) y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj (LTE ('S ('S n))) y -> Obj (LTE ('S ('S n))) z -> LTE ('S ('S n)) z (Exponential (LTE ('S ('S n))) y (BinaryProduct (LTE ('S ('S n))) z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). LTE ('S ('S n)) z1 z2 -> LTE ('S ('S n)) y2 y1 -> LTE ('S ('S n)) (Exponential (LTE ('S ('S n))) y1 z1) (Exponential (LTE ('S ('S n))) y2 z2) Source #
CartesianClosed (LTE ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin Associated Types type Exponential (LTE ('S 'Z)) y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj (LTE ('S 'Z)) y -> Obj (LTE ('S 'Z)) z -> LTE ('S 'Z) (BinaryProduct (LTE ('S 'Z)) (Exponential (LTE ('S 'Z)) y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj (LTE ('S 'Z)) y -> Obj (LTE ('S 'Z)) z -> LTE ('S 'Z) z (Exponential (LTE ('S 'Z)) y (BinaryProduct (LTE ('S 'Z)) z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). LTE ('S 'Z) z1 z2 -> LTE ('S 'Z) y2 y1 -> LTE ('S 'Z) (Exponential (LTE ('S 'Z)) y1 z1) (Exponential (LTE ('S 'Z)) y2 z2) Source #
HasBinaryCoproducts (LTE ('S n)) => HasBinaryCoproducts (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) Source #
Instance details Defined in Data.Category.Fin Associated Types type BinaryCoproduct (LTE ('S ('S n))) x y :: Kind k Source # Methods inj1 :: forall (x :: k) (y :: k). Obj (LTE ('S ('S n))) x -> Obj (LTE ('S ('S n))) y -> LTE ('S ('S n)) x (BinaryCoproduct (LTE ('S ('S n))) x y) Source # inj2 :: forall (x :: k) (y :: k). Obj (LTE ('S ('S n))) x -> Obj (LTE ('S ('S n))) y -> LTE ('S ('S n)) y (BinaryCoproduct (LTE ('S ('S n))) x y) Source # (\|\|\|) :: forall (x :: k) (a :: k) (y :: k). LTE ('S ('S n)) x a -> LTE ('S ('S n)) y a -> LTE ('S ('S n)) (BinaryCoproduct (LTE ('S ('S n))) x y) a Source # (+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). LTE ('S ('S n)) a1 b1 -> LTE ('S ('S n)) a2 b2 -> LTE ('S ('S n)) (BinaryCoproduct (LTE ('S ('S n))) a1 a2) (BinaryCoproduct (LTE ('S ('S n))) b1 b2) Source #
HasBinaryCoproducts (LTE ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin Associated Types type BinaryCoproduct (LTE ('S 'Z)) x y :: Kind k Source # Methods inj1 :: forall (x :: k) (y :: k). Obj (LTE ('S 'Z)) x -> Obj (LTE ('S 'Z)) y -> LTE ('S 'Z) x (BinaryCoproduct (LTE ('S 'Z)) x y) Source # inj2 :: forall (x :: k) (y :: k). Obj (LTE ('S 'Z)) x -> Obj (LTE ('S 'Z)) y -> LTE ('S 'Z) y (BinaryCoproduct (LTE ('S 'Z)) x y) Source # (\|\|\|) :: forall (x :: k) (a :: k) (y :: k). LTE ('S 'Z) x a -> LTE ('S 'Z) y a -> LTE ('S 'Z) (BinaryCoproduct (LTE ('S 'Z)) x y) a Source # (+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). LTE ('S 'Z) a1 b1 -> LTE ('S 'Z) a2 b2 -> LTE ('S 'Z) (BinaryCoproduct (LTE ('S 'Z)) a1 a2) (BinaryCoproduct (LTE ('S 'Z)) b1 b2) Source #
HasBinaryProducts (LTE ('S n)) => HasBinaryProducts (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) Source #
Instance details Defined in Data.Category.Fin Associated Types type BinaryProduct (LTE ('S ('S n))) x y :: Kind k Source # Methods proj1 :: forall (x :: k) (y :: k). Obj (LTE ('S ('S n))) x -> Obj (LTE ('S ('S n))) y -> LTE ('S ('S n)) (BinaryProduct (LTE ('S ('S n))) x y) x Source # proj2 :: forall (x :: k) (y :: k). Obj (LTE ('S ('S n))) x -> Obj (LTE ('S ('S n))) y -> LTE ('S ('S n)) (BinaryProduct (LTE ('S ('S n))) x y) y Source # (&&&) :: forall (a :: k) (x :: k) (y :: k). LTE ('S ('S n)) a x -> LTE ('S ('S n)) a y -> LTE ('S ('S n)) a (BinaryProduct (LTE ('S ('S n))) x y) Source # (***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). LTE ('S ('S n)) a1 b1 -> LTE ('S ('S n)) a2 b2 -> LTE ('S ('S n)) (BinaryProduct (LTE ('S ('S n))) a1 a2) (BinaryProduct (LTE ('S ('S n))) b1 b2) Source #
HasBinaryProducts (LTE ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin Associated Types type BinaryProduct (LTE ('S 'Z)) x y :: Kind k Source # Methods proj1 :: forall (x :: k) (y :: k). Obj (LTE ('S 'Z)) x -> Obj (LTE ('S 'Z)) y -> LTE ('S 'Z) (BinaryProduct (LTE ('S 'Z)) x y) x Source # proj2 :: forall (x :: k) (y :: k). Obj (LTE ('S 'Z)) x -> Obj (LTE ('S 'Z)) y -> LTE ('S 'Z) (BinaryProduct (LTE ('S 'Z)) x y) y Source # (&&&) :: forall (a :: k) (x :: k) (y :: k). LTE ('S 'Z) a x -> LTE ('S 'Z) a y -> LTE ('S 'Z) a (BinaryProduct (LTE ('S 'Z)) x y) Source # (***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). LTE ('S 'Z) a1 b1 -> LTE ('S 'Z) a2 b2 -> LTE ('S 'Z) (BinaryProduct (LTE ('S 'Z)) a1 a2) (BinaryProduct (LTE ('S 'Z)) b1 b2) Source #
HasInitialObject (LTE ('S n) :: Fin ('S n) -> Fin ('S n) -> Type) Source #
Instance details Defined in Data.Category.Fin Associated Types type InitialObject (LTE ('S n)) :: Kind k Source # Methods initialObject :: Obj (LTE ('S n)) (InitialObject (LTE ('S n))) Source # initialize :: forall (a :: k). Obj (LTE ('S n)) a -> LTE ('S n) (InitialObject (LTE ('S n))) a Source #
HasTerminalObject (LTE ('S n)) => HasTerminalObject (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) Source #
Instance details Defined in Data.Category.Fin Associated Types type TerminalObject (LTE ('S ('S n))) :: Kind k Source # Methods terminalObject :: Obj (LTE ('S ('S n))) (TerminalObject (LTE ('S ('S n)))) Source # terminate :: forall (a :: k). Obj (LTE ('S ('S n))) a -> LTE ('S ('S n)) a (TerminalObject (LTE ('S ('S n)))) Source #
HasTerminalObject (LTE ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin Associated Types type TerminalObject (LTE ('S 'Z)) :: Kind k Source # Methods terminalObject :: Obj (LTE ('S 'Z)) (TerminalObject (LTE ('S 'Z))) Source # terminate :: forall (a :: k). Obj (LTE ('S 'Z)) a -> LTE ('S 'Z) a (TerminalObject (LTE ('S 'Z))) Source #
type InitialObject (LTE ('S n) :: Fin ('S n) -> Fin ('S n) -> Type) Source #
Instance details Defined in Data.Category.Fin type InitialObject (LTE ('S n) :: Fin ('S n) -> Fin ('S n) -> Type) = 'FZ :: Fin ('S n)
type TerminalObject (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) Source #
Instance details Defined in Data.Category.Fin type TerminalObject (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) = 'FS (TerminalObject (LTE ('S n)))
type TerminalObject (LTE ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin type TerminalObject (LTE ('S 'Z)) = 'FZ :: Fin ('S 'Z)
type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) = 'FS (Exponential (LTE ('S n)) ('FZ :: Fin ('S n)) ('FZ :: Fin ('S n)))
type Exponential (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin type Exponential (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) = 'FZ :: Fin ('S 'Z)
type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) = 'FZ :: Fin ('S ('S n))
type BinaryCoproduct (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin type BinaryCoproduct (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) = 'FZ :: Fin ('S 'Z)
type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) = 'FZ :: Fin ('S ('S n))
type BinaryProduct (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin type BinaryProduct (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) = 'FZ :: Fin ('S 'Z)
type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FS (Exponential (LTE ('S n)) ('FZ :: Fin ('S n)) b)
type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FS (BinaryCoproduct (LTE ('S n)) ('FZ :: Fin ('S n)) b)
type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FZ :: Fin ('S ('S n))
type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) = 'FZ :: Fin ('S ('S n))
type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) = 'FS (BinaryCoproduct (LTE ('S n)) a ('FZ :: Fin ('S n)))
type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) = 'FZ :: Fin ('S ('S n))
type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FS (Exponential (LTE ('S n)) a b)
type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FS (BinaryCoproduct (LTE ('S n)) a b)
type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FS (BinaryProduct (LTE ('S n)) a b)

data LTE (n :: Nat) (a :: Fin n) (b :: Fin n) where Source #

Constructors

ZEQ :: LTE ('S m) 'FZ 'FZ
ZLT :: LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
SLT :: LTE ('S m) a b -> LTE ('S ('S m)) ('FS a) ('FS b)

Instances

Instances details

Category (LTE n :: Fin n -> Fin n -> Type) Source #
Instance details Defined in Data.Category.Fin Methods src :: forall (a :: k) (b :: k). LTE n a b -> Obj (LTE n) a Source # tgt :: forall (a :: k) (b :: k). LTE n a b -> Obj (LTE n) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). LTE n b c -> LTE n a b -> LTE n a c Source #
CartesianClosed (LTE ('S n)) => CartesianClosed (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) Source #
Instance details Defined in Data.Category.Fin Associated Types type Exponential (LTE ('S ('S n))) y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj (LTE ('S ('S n))) y -> Obj (LTE ('S ('S n))) z -> LTE ('S ('S n)) (BinaryProduct (LTE ('S ('S n))) (Exponential (LTE ('S ('S n))) y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj (LTE ('S ('S n))) y -> Obj (LTE ('S ('S n))) z -> LTE ('S ('S n)) z (Exponential (LTE ('S ('S n))) y (BinaryProduct (LTE ('S ('S n))) z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). LTE ('S ('S n)) z1 z2 -> LTE ('S ('S n)) y2 y1 -> LTE ('S ('S n)) (Exponential (LTE ('S ('S n))) y1 z1) (Exponential (LTE ('S ('S n))) y2 z2) Source #
CartesianClosed (LTE ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin Associated Types type Exponential (LTE ('S 'Z)) y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj (LTE ('S 'Z)) y -> Obj (LTE ('S 'Z)) z -> LTE ('S 'Z) (BinaryProduct (LTE ('S 'Z)) (Exponential (LTE ('S 'Z)) y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj (LTE ('S 'Z)) y -> Obj (LTE ('S 'Z)) z -> LTE ('S 'Z) z (Exponential (LTE ('S 'Z)) y (BinaryProduct (LTE ('S 'Z)) z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). LTE ('S 'Z) z1 z2 -> LTE ('S 'Z) y2 y1 -> LTE ('S 'Z) (Exponential (LTE ('S 'Z)) y1 z1) (Exponential (LTE ('S 'Z)) y2 z2) Source #
HasBinaryCoproducts (LTE ('S n)) => HasBinaryCoproducts (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) Source #
Instance details Defined in Data.Category.Fin Associated Types type BinaryCoproduct (LTE ('S ('S n))) x y :: Kind k Source # Methods inj1 :: forall (x :: k) (y :: k). Obj (LTE ('S ('S n))) x -> Obj (LTE ('S ('S n))) y -> LTE ('S ('S n)) x (BinaryCoproduct (LTE ('S ('S n))) x y) Source # inj2 :: forall (x :: k) (y :: k). Obj (LTE ('S ('S n))) x -> Obj (LTE ('S ('S n))) y -> LTE ('S ('S n)) y (BinaryCoproduct (LTE ('S ('S n))) x y) Source # (\|\|\|) :: forall (x :: k) (a :: k) (y :: k). LTE ('S ('S n)) x a -> LTE ('S ('S n)) y a -> LTE ('S ('S n)) (BinaryCoproduct (LTE ('S ('S n))) x y) a Source # (+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). LTE ('S ('S n)) a1 b1 -> LTE ('S ('S n)) a2 b2 -> LTE ('S ('S n)) (BinaryCoproduct (LTE ('S ('S n))) a1 a2) (BinaryCoproduct (LTE ('S ('S n))) b1 b2) Source #
HasBinaryCoproducts (LTE ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin Associated Types type BinaryCoproduct (LTE ('S 'Z)) x y :: Kind k Source # Methods inj1 :: forall (x :: k) (y :: k). Obj (LTE ('S 'Z)) x -> Obj (LTE ('S 'Z)) y -> LTE ('S 'Z) x (BinaryCoproduct (LTE ('S 'Z)) x y) Source # inj2 :: forall (x :: k) (y :: k). Obj (LTE ('S 'Z)) x -> Obj (LTE ('S 'Z)) y -> LTE ('S 'Z) y (BinaryCoproduct (LTE ('S 'Z)) x y) Source # (\|\|\|) :: forall (x :: k) (a :: k) (y :: k). LTE ('S 'Z) x a -> LTE ('S 'Z) y a -> LTE ('S 'Z) (BinaryCoproduct (LTE ('S 'Z)) x y) a Source # (+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). LTE ('S 'Z) a1 b1 -> LTE ('S 'Z) a2 b2 -> LTE ('S 'Z) (BinaryCoproduct (LTE ('S 'Z)) a1 a2) (BinaryCoproduct (LTE ('S 'Z)) b1 b2) Source #
HasBinaryProducts (LTE ('S n)) => HasBinaryProducts (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) Source #
Instance details Defined in Data.Category.Fin Associated Types type BinaryProduct (LTE ('S ('S n))) x y :: Kind k Source # Methods proj1 :: forall (x :: k) (y :: k). Obj (LTE ('S ('S n))) x -> Obj (LTE ('S ('S n))) y -> LTE ('S ('S n)) (BinaryProduct (LTE ('S ('S n))) x y) x Source # proj2 :: forall (x :: k) (y :: k). Obj (LTE ('S ('S n))) x -> Obj (LTE ('S ('S n))) y -> LTE ('S ('S n)) (BinaryProduct (LTE ('S ('S n))) x y) y Source # (&&&) :: forall (a :: k) (x :: k) (y :: k). LTE ('S ('S n)) a x -> LTE ('S ('S n)) a y -> LTE ('S ('S n)) a (BinaryProduct (LTE ('S ('S n))) x y) Source # (***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). LTE ('S ('S n)) a1 b1 -> LTE ('S ('S n)) a2 b2 -> LTE ('S ('S n)) (BinaryProduct (LTE ('S ('S n))) a1 a2) (BinaryProduct (LTE ('S ('S n))) b1 b2) Source #
HasBinaryProducts (LTE ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin Associated Types type BinaryProduct (LTE ('S 'Z)) x y :: Kind k Source # Methods proj1 :: forall (x :: k) (y :: k). Obj (LTE ('S 'Z)) x -> Obj (LTE ('S 'Z)) y -> LTE ('S 'Z) (BinaryProduct (LTE ('S 'Z)) x y) x Source # proj2 :: forall (x :: k) (y :: k). Obj (LTE ('S 'Z)) x -> Obj (LTE ('S 'Z)) y -> LTE ('S 'Z) (BinaryProduct (LTE ('S 'Z)) x y) y Source # (&&&) :: forall (a :: k) (x :: k) (y :: k). LTE ('S 'Z) a x -> LTE ('S 'Z) a y -> LTE ('S 'Z) a (BinaryProduct (LTE ('S 'Z)) x y) Source # (***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). LTE ('S 'Z) a1 b1 -> LTE ('S 'Z) a2 b2 -> LTE ('S 'Z) (BinaryProduct (LTE ('S 'Z)) a1 a2) (BinaryProduct (LTE ('S 'Z)) b1 b2) Source #
HasInitialObject (LTE ('S n) :: Fin ('S n) -> Fin ('S n) -> Type) Source #
Instance details Defined in Data.Category.Fin Associated Types type InitialObject (LTE ('S n)) :: Kind k Source # Methods initialObject :: Obj (LTE ('S n)) (InitialObject (LTE ('S n))) Source # initialize :: forall (a :: k). Obj (LTE ('S n)) a -> LTE ('S n) (InitialObject (LTE ('S n))) a Source #
HasTerminalObject (LTE ('S n)) => HasTerminalObject (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) Source #
Instance details Defined in Data.Category.Fin Associated Types type TerminalObject (LTE ('S ('S n))) :: Kind k Source # Methods terminalObject :: Obj (LTE ('S ('S n))) (TerminalObject (LTE ('S ('S n)))) Source # terminate :: forall (a :: k). Obj (LTE ('S ('S n))) a -> LTE ('S ('S n)) a (TerminalObject (LTE ('S ('S n)))) Source #
HasTerminalObject (LTE ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin Associated Types type TerminalObject (LTE ('S 'Z)) :: Kind k Source # Methods terminalObject :: Obj (LTE ('S 'Z)) (TerminalObject (LTE ('S 'Z))) Source # terminate :: forall (a :: k). Obj (LTE ('S 'Z)) a -> LTE ('S 'Z) a (TerminalObject (LTE ('S 'Z))) Source #
type InitialObject (LTE ('S n) :: Fin ('S n) -> Fin ('S n) -> Type) Source #
Instance details Defined in Data.Category.Fin type InitialObject (LTE ('S n) :: Fin ('S n) -> Fin ('S n) -> Type) = 'FZ :: Fin ('S n)
type TerminalObject (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) Source #
Instance details Defined in Data.Category.Fin type TerminalObject (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) = 'FS (TerminalObject (LTE ('S n)))
type TerminalObject (LTE ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin type TerminalObject (LTE ('S 'Z)) = 'FZ :: Fin ('S 'Z)
type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) = 'FS (Exponential (LTE ('S n)) ('FZ :: Fin ('S n)) ('FZ :: Fin ('S n)))
type Exponential (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin type Exponential (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) = 'FZ :: Fin ('S 'Z)
type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) = 'FZ :: Fin ('S ('S n))
type BinaryCoproduct (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin type BinaryCoproduct (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) = 'FZ :: Fin ('S 'Z)
type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FZ :: Fin ('S ('S n))) = 'FZ :: Fin ('S ('S n))
type BinaryProduct (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin type BinaryProduct (LTE ('S 'Z)) ('FZ :: Fin ('S 'Z)) ('FZ :: Fin ('S 'Z)) = 'FZ :: Fin ('S 'Z)
type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FS (Exponential (LTE ('S n)) ('FZ :: Fin ('S n)) b)
type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FS (BinaryCoproduct (LTE ('S n)) ('FZ :: Fin ('S n)) b)
type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FZ :: Fin ('S ('S n))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FZ :: Fin ('S ('S n))
type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) = 'FZ :: Fin ('S ('S n))
type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) = 'FS (BinaryCoproduct (LTE ('S n)) a ('FZ :: Fin ('S n)))
type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) Source #
Instance details Defined in Data.Category.Fin type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FZ :: Fin ('S ('S n))) = 'FZ :: Fin ('S ('S n))
type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type Exponential (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FS (Exponential (LTE ('S n)) a b)
type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type BinaryCoproduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FS (BinaryCoproduct (LTE ('S n)) a b)
type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) Source #
Instance details Defined in Data.Category.Fin type BinaryProduct (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) ('FS a :: Kind (LTE ('S ('S n)))) ('FS b :: Kind (LTE ('S ('S n)))) = 'FS (BinaryProduct (LTE ('S n)) a b)

data Proof a n where Source #

Constructors

Proof :: (BinaryProduct (LTE ('S n)) 'FZ a ~ 'FZ, BinaryProduct (LTE ('S n)) a 'FZ ~ 'FZ) => Proof a n

proof :: Obj (LTE ('S n)) a -> Proof a n Source #