Library UniMath.CategoryTheory.SimplicialSets
Homotopy theory of simplicial sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Export UniMath.Combinatorics.FiniteSets.
Require Export UniMath.CategoryTheory.Core.Categories.
Require Export UniMath.CategoryTheory.Core.Functors.
Require Export UniMath.CategoryTheory.FunctorCategory.
Require Export UniMath.CategoryTheory.categories.HSET.Core.
Require Export UniMath.CategoryTheory.categories.HSET.Univalence.
Require Export UniMath.CategoryTheory.opp_precat.
Local Open Scope stn.
Definition monfunstn ( n m : nat ) : UU := ∑ f : ⟦ n ⟧ -> ⟦ m ⟧, ∏ (x y: ⟦n⟧), x ≤ y -> f x ≤ f y.
Definition make_monfunstn { m n : nat } f is := (f,,is) : monfunstn m n.
Definition monfunstnpr1 {n m : nat} : monfunstn n m -> ⟦ n ⟧ -> ⟦ m ⟧ := pr1.
Lemma monfunstnpr1_isInjective {m n} (f g : monfunstn m n) : monfunstnpr1 f = monfunstnpr1 g -> f = g.
Show proof.
intros e.
apply subtypePath.
{ intros h. apply impred; intro i. apply impred; intro j. apply impred; intro l.
apply propproperty. }
exact e.
apply subtypePath.
{ intros h. apply impred; intro i. apply impred; intro j. apply impred; intro l.
apply propproperty. }
exact e.
Coercion monfunstnpr1 : monfunstn >-> Funclass .
Lemma isasetmonfunstn n m : isaset ( monfunstn n m ) .
Show proof.
intros . apply ( isofhleveltotal2 2 ) .
{ apply impred. intro t. apply isasetstn. }
intro f. apply impred; intro i. apply impred; intro j. apply impred; intro l.
apply isasetaprop, propproperty.
{ apply impred. intro t. apply isasetstn. }
intro f. apply impred; intro i. apply impred; intro j. apply impred; intro l.
apply isasetaprop, propproperty.
Definition monfunstnid n : monfunstn n n := make_monfunstn (idfun _) (λ x y is, is).
Definition monfunstncomp { n m k : nat } ( f : monfunstn n m ) ( g : monfunstn m k ) :
monfunstn n k .
Show proof.
intros . exists ( g ∘ f ) . intros i j l. unfold funcomp.
apply ( pr2 g ). apply ( pr2 f ) . assumption.
apply ( pr2 g ). apply ( pr2 f ) . assumption.
Definition precatDelta : precategory .
Show proof.
use tpair.
{ use tpair.
{ exists nat. intros m n. exact (monfunstn (S m) (S n)). }
{ split.
{ intros m. apply monfunstnid. }
{ intros l m n f g. exact (monfunstncomp f g). } } }
apply is_precategory_one_assoc_to_two.
simpl. split.
{ simpl. split.
{ intros m n f. now apply monfunstnpr1_isInjective. }
{ intros m n f. now apply monfunstnpr1_isInjective. } }
{ simpl. intros m n o p f g h. now apply monfunstnpr1_isInjective. }
{ use tpair.
{ exists nat. intros m n. exact (monfunstn (S m) (S n)). }
{ split.
{ intros m. apply monfunstnid. }
{ intros l m n f g. exact (monfunstncomp f g). } } }
apply is_precategory_one_assoc_to_two.
simpl. split.
{ simpl. split.
{ intros m n f. now apply monfunstnpr1_isInjective. }
{ intros m n f. now apply monfunstnpr1_isInjective. } }
{ simpl. intros m n o p f g h. now apply monfunstnpr1_isInjective. }
Local Open Scope cat.
Definition has_homsets_precatDelta : has_homsets precatDelta.
Show proof.
Definition catDelta : category := make_category precatDelta has_homsets_precatDelta.
Definition sSet := functor_category catDelta^op category_HSET.