# Steiner systems

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-07-15.

module univalent-combinatorics.steiner-systems where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.contractible-types
open import foundation.decidable-subtypes
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import univalent-combinatorics.finite-types


## Idea

A Steiner system of type (t,k,n) : ℕ³ consists of an n-element type X equipped with a (decidable) set P of k-element subtypes of X such that each t-element subtype of X is contained in exactly one k-element subtype in P. A basic example is the Fano plane, which is a Steiner system of type (2,3,7).

## Definition

### Steiner systems

Steiner-System : ℕ → ℕ → ℕ → UU (lsuc lzero)
Steiner-System t k n =
Σ ( UU-Fin lzero n)
( λ X →
Σ ( decidable-subtype lzero
( Σ ( decidable-subtype lzero (type-UU-Fin n X))
( λ P → has-cardinality k (type-decidable-subtype P))))
( λ P →
( Q : decidable-subtype lzero (type-UU-Fin n X)) →
has-cardinality t (type-decidable-subtype Q) →
is-contr
( Σ ( type-decidable-subtype P)
( λ U →
(x : type-UU-Fin n X) →
is-in-decidable-subtype Q x →
is-in-decidable-subtype (pr1 (pr1 U)) x))))