Skip to content
Snippets Groups Projects
Commit 81b93e98 authored by Håkon Gylterud's avatar Håkon Gylterud
Browse files

Add a straight forward definition of (homotopic) M-types.

parent 7a6bdc42
No related branches found
No related tags found
No related merge requests found
module Type.M where
open import lib.Base
open import lib.NType
open import Notation
module _ {i j} (S : Type i) (P : S → Type j) where
module _ (M : Type (lmax i j))
(desup : M → Σ S (λ s → P s → M)) where
Final : ∀ k → Type (lmax (lsucc k) (lmax i j))
Final k = ∀ (X : Type k) (f : X → Σ S (λ s → P s → X))
→ is-contr (Σ (X → M)
(λ r → ∀ x → desup (r x) == (fst (f x) , λ p → r (snd (f x) p))))
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment