# Finiteness

```
{-# OPTIONS --allow-unsolved-metas --without-K #-}

open import Level using (Level; Lift)
import Level as L
open import Data.Nat
open import Data.Bool
open import Data.Unit
open import Data.List as List
open import Data.List.Properties as List
open import Data.List.Membership.Propositional
import Data.List.Membership.Propositional.Properties as List
open import Data.List.Relation.Unary.Any
open import Data.Empty
open import Data.Product as Σ
open import Data.Sum as ⊎
open import Function.Base using (_∘_; flip; case_of_)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary using (_⊆_)
open import Function.Definitions using (Injective; Surjective)

module Finite where

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Set ℓ
    B : Set ℓ'
    C : Set ℓ''
```

## Finite sets with a fixed number of elements
```
module Fin-Redef where
  data Fin : ℕ → Set where
    zero : ∀ {k : ℕ} → Fin (suc k)
    suc : ∀ {k : ℕ} → (i : Fin k) → Fin (suc k)

  List' : Set → Set
  List' X = Σ[ n ∈ ℕ ] (Fin n) → X

```
## Vector
```
module Vec-Redef where
  data Vec (X : Set) : ℕ → Set where
    [] : Vec X 0
    _∷_ : ∀ {n : ℕ} → (x : X) → (tl : Vec X n) → Vec X (suc n)

  -- Blatt 04:
  -- Vec X n ≡ Fin n → X
```

## Definitions of Finiteness
```
open import Data.Fin hiding (_+_)

record Finite (X : Set ℓ) : Set ℓ where
  field
    k : ℕ
    f : Fin k → X
    f-surj : ∀ x → ∃[ i ] f i ≡ x

record FiniteL (X : Set ℓ) : Set ℓ where
  field
    elems : List X
    all-contained : ∀ (x : X) → x ∈ elems

```
[Ende der Vorlesung am 11.05.2026]

## Decidability

## Quantifiers

## Alternative (and more) complicated solutions
Idea: strengthen the induction hypothesis by generalizing from "all elements of A"
to "all elements satisfying a predicate P ⊆ A".
```

```

## Stdlib

```
import Data.Fin using (Fin)
import Data.Vec using (Vec)
```