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 monfunstnpair { 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 subtypeEquality.
{ intros h. apply impred; intro i. apply impred; intro j. apply impred; intro l.
apply propproperty. }
exact e.
apply subtypeEquality.
{ 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 := monfunstnpair (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 sSet := [ precatDelta^op , HSET, pr2 is_univalent_HSET ] .