Barras-Coq/000777 000765 000024 00000000000 12404034062 013417 5ustar00nicolastaff000000 000000 Barras-Coq/._.DS_Store000777 000765 000024 00000000170 12357022444 015330 0ustar00nicolastaff000000 000000 Mac OS X  2Fx ATTRxxBarras-Coq/.DS_Store000777 000765 000024 00000014004 12357022444 015114 0ustar00nicolastaff000000 000000 Bud1id_modsetoid_model_v2.vIlocblob  @ @ @ @ EDSDB ` @ @ @Barras-Coq/._setoid_model_v2.v000777 000765 000024 00000000573 12357021066 017120 0ustar00nicolastaff000000 000000 Mac OS X  2I{ATTR{7com.apple.metadata:kMDLabel_pgwv7rgd3bxuc7hm254y2aatsaecom.apple.quarantineWEI# 9:jd38N5ȩCrRV'r#b݅k0ٱzTtXAV,H̐6L<}A./4%KyVuӄ^|%E8ytg>χa q/0002;53bc2237;Mail;Barras-Coq/setoid_model_v2.v000777 000765 000024 00000217557 12357021066 016717 0ustar00nicolastaff000000 000000 (* Use Coq V8.4 or trunk. *) Require Program. Obligation Tactic := idtac. Open Scope type_scope. Reserved Notation "x --> y" (at level 60, y at next level). Reserved Notation "x --> y --> z" (at level 60, y at next level, z at next level). Reserved Notation "x -->[ a ] y" (at level 60, y at next level). Reserved Notation "x ==> y" (at level 60, y at next level). Reserved Notation "f ∘ g" (at level 50, no associativity). Reserved Notation "f ∘∘ g" (at level 50, no associativity). Reserved Notation "x <-> y <-> z" (at level 95, y at next level, z at next level). Reserved Notation "x <-> y <-> z <-> t" (at level 95, y at next level, z at next level, t at next level). (* Inhabitedness: to avoid universe inconsistency in the def of universes... *) Inductive inh (X:Type) : Prop := Inh (x:X). Implicit Arguments Inh [X]. Axiom type_in_type : forall {X}, inh X -> X. Definition inh_map {X Y} (f:X->Y) (x':inh X) : inh Y := match x' with Inh x => Inh (f x) end. Parameter inh_eqn : forall T (x:T), type_in_type (Inh x) = x. (*****************************************************************************************************) (** Lines, Triangles, Tetrahedra *) (** Line completion *) Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }. Infix "<->" := iffT : type_scope. Implicit Arguments mkIff [X Y]. Implicit Arguments iffLR [X Y]. Implicit Arguments iffRL [X Y]. Notation li0 := iffLR (only parsing). Notation li1 := iffRL (only parsing). Definition refl_iffT {X} : iffT X X := mkIff (fun x=>x) (fun x=>x). Definition rel_compose {A B C} (R:A->B->Type) (S:B->C->Type) (a:A) (c:C) : Type := { b:B & R a b * S b c}. (** Line fillers *) Record coh0 {A B} (R:A->B->Type) (i:A<->B) := mkCoh0 { coh00 : forall a, R a (li0 i a); coh01 : forall b, R (li1 i b) b }. Implicit Arguments mkCoh0 [A B R i]. Implicit Arguments coh00 [A B R i]. Implicit Arguments coh01 [A B R i]. Definition triv_coh0 {A B l} : @coh0 A B (fun _ _ => unit) l := mkCoh0 (fun _ => tt) (fun _ => tt). (** Triangle completion *) Record tri {A B C:Type} (R:A->B->Type) (S:A->C->Type) (T:B->C->Type) := mkTri { tri0 : forall a b c, R a b -> S a c -> T b c; tri1 : forall a b c, R a b -> T b c -> S a c; tri2 : forall a b c, S a c -> T b c -> R a b }. Implicit Arguments mkTri [A B C R S T]. Implicit Arguments tri0 [A B C R S T a b c]. Implicit Arguments tri1 [A B C R S T a b c]. Implicit Arguments tri2 [A B C R S T a b c]. Notation "a <-> b <-> c" := (tri a c b). (* /!\ order changed *) Definition triv_tri {A B C} : @tri A B C (fun _ _=>unit) (fun _ _=>unit) (fun _ _=>unit) := mkTri (fun _ _ _ _ _ => tt) (fun _ _ _ _ _ => tt) (fun _ _ _ _ _ => tt). (** (0 1 2) -> (2 0 1) *) Definition tri_rot0 {A B C:Type} {R:A->B->Type} {S:A->C->Type} {T:B->C->Type} (t:R<->T<->S) : (fun c a => S a c)<->R<->(fun c b => T b c) := mkTri(fun _ _ _ w w' => tri2 t w w')(fun _ _ _ w w' => tri0 t w' w)(fun _ _ _ w w' => tri1 t w' w). (** (0 1 2) -> (1 2 0) *) Program Definition tri_rot1 {A B C:Type} {R:A->B->Type} {S:A->C->Type} {T:B->C->Type} (t:R<->T<->S) : T<->(fun c a => S a c)<->(fun b a => R a b) := mkTri(fun _ _ _ w w' => tri1 t w' w)(fun _ _ _ w w' => tri2 t w' w)(fun _ _ _ w w' => tri0 t w w'). (** Stitch two triangles together *) Lemma tri_compose {X0 X1 X2 X3} {R01:X0->X1->Type}{R03:X0->X3->Type}{R12:X1->X2->Type}{R13:X1->X3->Type}{R23:X2->X3->Type} {C13:X1 <-> X3} : coh0 R13 C13 -> (R01 <-> R13 <-> R03) -> (R12 <-> R23 <-> R13) -> (rel_compose R01 R12 <-> R23 <-> R03). intros F13 t013 t123. split; intros x0 x2 x3. intros (x1,(x01,x12)) x03. apply (tri0 t123) with (1:=x12). apply (tri0 t013) with (1:=x01) (2:=x03). intros (x1,(x01,x12)) x23. eapply (tri1 t013) with (1:=x01). eapply (tri1 t123) with (1:=x12) (2:=x23). intros x03 x23. assert (x13:=coh01 F13 x3). exists (li1 C13 x3); split. apply (tri2 t013) with (1:=x03)(2:=x13). apply (tri2 t123) with (1:=x13)(2:=x23). Defined. (** Poor man's univ polymorphism... *) Notation tri_iffT (*: iffT <-> iffT <-> iffT*) := (mkTri (fun X0 X1 X2 E01 E02 => (mkIff(fun x1 => iffLR E02 (iffRL E01 x1))(fun x2 => iffLR E01 (iffRL E02 x2)))) (fun X0 X1 X2 E01 E12 => (mkIff(fun x0 => iffLR E12 (iffLR E01 x0))(fun x2 => iffRL E01 (iffRL E12 x2)))) (fun X0 X1 X2 E02 E12 => (mkIff(fun x0 => iffRL E12 (iffLR E02 x0))(fun x1 => iffRL E02 (iffLR E12 x1))))). (** Triangle filler *) Record coh1 {X0 X1 X2}{R01:X0->X1->Type}{R02:X0->X2->Type}{R12:X1->X2->Type} (T:forall {x0 x1 x2}, R01 x0 x1->R02 x0 x2->R12 x1 x2->Type) (t:R01<->R12<->R02) := mkCoh1 { coh10 : forall {x0 x1 x2} (x01:R01 x0 x1)(x02:R02 x0 x2), T x01 x02 (tri0 t x01 x02); coh11 : forall {x0 x1 x2} (x01:R01 x0 x1)(x12:R12 x1 x2), T x01 (tri1 t x01 x12) x12; coh12 : forall {x0 x1 x2} (x02:R02 x0 x2)(x12:R12 x1 x2), T (tri2 t x02 x12) x02 x12 }. Implicit Arguments mkCoh1 [X0 X1 X2 R01 R02 R12 T t]. Implicit Arguments coh10 [X0 X1 X2 R01 R02 R12 T t x0 x1 x2]. Implicit Arguments coh11 [X0 X1 X2 R01 R02 R12 T t x0 x1 x2]. Implicit Arguments coh12 [X0 X1 X2 R01 R02 R12 T t x0 x1 x2]. Definition triv_coh1 {X0 X1 X2 R01 R02 R12 t} : @coh1 X0 X1 X2 R01 R02 R12 (fun _ _ _ _ _ _ => unit) t := mkCoh1 (fun _ _ _ _ _ => tt) (fun _ _ _ _ _ => tt) (fun _ _ _ _ _ => tt). (** Tetrahedron completion *) Record tetra {A B C D} {Rab:A->B->Type}{Rac:A->C->Type}{Rad:A->D->Type}{Rbc:B->C->Type}{Rbd:B->D->Type}{Rcd:C->D->Type} (Rabc:forall {a b c}, Rab a b -> Rac a c -> Rbc b c -> Type) (Rabd:forall {a b d}, Rab a b -> Rad a d -> Rbd b d -> Type) (Racd:forall {a c d}, Rac a c -> Rad a d -> Rcd c d -> Type) (Rbcd:forall {b c d}, Rbc b c -> Rbd b d -> Rcd c d -> Type) := mkTetra { tet0: forall {a b c d}{ab:Rab a b}{ac:Rac a c}{ad:Rad a d}{bc bd cd}, Rabc ab ac bc -> Rabd ab ad bd -> Racd ac ad cd -> Rbcd bc bd cd; tet1: forall {a b c d}{ab:Rab a b}{ac:Rac a c}{ad:Rad a d}{bc bd cd}, Rabc ab ac bc -> Rabd ab ad bd -> Rbcd bc bd cd -> Racd ac ad cd; tet2: forall {a b c d}{ab:Rab a b}{ac:Rac a c}{ad:Rad a d}{bc bd cd}, Rabc ab ac bc -> Racd ac ad cd -> Rbcd bc bd cd -> Rabd ab ad bd; tet3: forall {a b c d}{ab:Rab a b}{ac:Rac a c}{ad:Rad a d}{bc bd cd}, Rabd ab ad bd -> Racd ac ad cd -> Rbcd bc bd cd -> Rabc ab ac bc }. Implicit Arguments mkTetra [A B C D Rab Rac Rad Rbc Rbd Rcd Rabc Rabd Racd Rbcd]. Implicit Arguments tet0 [A B C D Rab Rac Rad Rbc Rbd Rcd Rabc Rabd Racd Rbcd a b c d ab ac ad bc bd cd]. Implicit Arguments tet1 [A B C D Rab Rac Rad Rbc Rbd Rcd Rabc Rabd Racd Rbcd a b c d ab ac ad bc bd cd]. Implicit Arguments tet2 [A B C D Rab Rac Rad Rbc Rbd Rcd Rabc Rabd Racd Rbcd a b c d ab ac ad bc bd cd]. Implicit Arguments tet3 [A B C D Rab Rac Rad Rbc Rbd Rcd Rabc Rabd Racd Rbcd a b c d ab ac ad bc bd cd]. Notation "abc <-> abd <-> acd <-> bcd" := (tetra abc abd acd bcd). Definition triv_tetra {A B C D Rab Rac Rad Rbc Rbd Rcd} : @tetra A B C D Rab Rac Rad Rbc Rbd Rcd (fun _ _ _ _ _ _=>unit) (fun _ _ _ _ _ _=>unit) (fun _ _ _ _ _ _=>unit) (fun _ _ _ _ _ _=>unit) := mkTetra (fun _ _ _ _ _ _ _ _ _ _ _ _ _ => tt) (fun _ _ _ _ _ _ _ _ _ _ _ _ _ => tt) (fun _ _ _ _ _ _ _ _ _ _ _ _ _ => tt) (fun _ _ _ _ _ _ _ _ _ _ _ _ _ => tt). (*****************************************************************************************************) (** Contexts *) Record context := mkCtx { ctx :> Type; rel : ctx -> ctx -> Type where "x --> y" := (rel x y); ctri : forall {x0 x1 x2}, x0-->x1 -> x0-->x2 -> x1-->x2 -> Type where "x01 --> x12 --> x02" := (ctri x01 x02 x12); (* /!\ order changed *) comp0 : ctx <-> ctx; (* Gives the other handside of a degenerated line *) Comp0 : coh0 rel comp0; (* Fills a degenerated line *) comp1 : rel <-> rel <-> rel; (* Completion of a triangle *) Comp1 : coh1 (@ctri) comp1; (* Fills a triangle *) comp2 : @ctri <-> @ctri <-> @ctri <-> @ctri (* Completion of a tetrahedron *) }. Infix "-->" := (rel _) : ctx_scope. Open Scope ctx_scope. Notation "w1 --> w2 --> w3" := (ctri _ w1 w3 w2). (** Subsitutions = context morphisms *) Record sub (S1 S2:context) := mkSub { sub_f :> S1 -> S2; sub_w : forall {x x':S1}, x --> x' -> sub_f x --> sub_f x'; sub_t : forall {x0 x1 x2} {x01:x0-->x1}{x02:x0-->x2}{x12:x1-->x2}, x01 --> x12 --> x02 -> sub_w x01 --> sub_w x12 --> sub_w x02 }. Implicit Arguments sub_w [S1 S2 x x']. Implicit Arguments sub_t [S1 S2 x0 x1 x2 x01 x02 x12]. Definition etas {S1 S2} (f:sub S1 S2) : sub S1 S2 := mkSub _ _ (fun s => f s) (fun x x' a => sub_w f a) (fun x0 x1 x2 x01 x02 x12 t => sub_t f t). Definition ids {S} : sub S S := mkSub _ _ (fun x => x) (fun x x' a => a) (fun x0 x1 x2 x01 x02 x12 t => t). Definition compS {S1 S2 S3} (f:sub S2 S3) (g:sub S1 S2) : sub S1 S3 := mkSub S1 S3 (fun x => f (g x)) (fun _ _ a => sub_w f (sub_w g a)) (fun _ _ _ _ _ _ t => sub_t f (sub_t g t)). Infix "∘" := compS. Lemma eq_compS_assoc {S1 S2 S3 S4} (f:sub S3 S4) (g:sub S2 S3) (h:sub S1 S2) : (f ∘ g) ∘ h = f ∘ (g ∘ h). reflexivity. Defined. Lemma eq_compS_idl {S1 S2} (f:sub S1 S2) : ids ∘ f = etas f. reflexivity. Defined. Lemma eq_compS_idr {S1 S2} (f:sub S1 S2) : f ∘ ids = etas f. reflexivity. Defined. (** Setoids *) Record setoid := mkSet { car :> Type; srel : car -> car -> Type where "x --> y" := (srel x y) : setoid_scope; scomp0 : car <-> car; sComp0 : coh0 srel scomp0; scomp1 : srel <-> srel <-> srel }. Implicit Arguments srel [s]. Infix "-->" := srel : setoid_scope. Delimit Scope setoid_scope with s. Program Definition mkSetRefl (car:Type) (srel:car->car->Type) (refl:forall x,srel x x) (scomp1:srel<->srel<->srel) := mkSet car srel refl_iffT (mkCoh0 refl refl) scomp1. Program Definition mkSetEq (X:Type) : setoid := mkSetRefl X (fun n m => n=m) (@eq_refl X) _. Next Obligation. split; intros; subst; trivial. Defined. Definition triv (X:Type) : setoid := mkSet X (fun _ _ => unit) refl_iffT triv_coh0 triv_tri. (** setoids are embedded into contexts by equipping them with trivial triangles *) Program Definition setoid2context (A:setoid) : context := mkCtx A (@srel A) (fun _ _ _ _ _ _=>unit) (@scomp0 A) (@sComp0 A) (@scomp1 A) triv_coh1 triv_tetra. (** Final context (nil) *) Program Definition un : context := setoid2context (triv unit). Definition fin {S} : sub S un := mkSub _ un (fun _ => tt) (fun _ _ _ => tt) (fun _ _ _ _ _ _ _ => tt). Lemma eq_compS_fin {S T} (f:sub S T) : fin ∘ f = fin. reflexivity. Defined. (** Setoid morphisms *) Record morphism (S1 S2:setoid) := mkMorph { morph_f :> S1 -> S2; morph_w : forall {x x':S1}, (x --> x')%s -> (morph_f x --> morph_f x')%s }. Implicit Arguments morph_w [S1 S2 x x']. Definition comp_morph {S1 S2 S3} (m1:morphism S2 S3) (m2:morphism S1 S2) : morphism S1 S3 := mkMorph _ _ (fun x => m1 (m2 x)) (fun x x' w => morph_w m1 (morph_w m2 w)). Infix "∘∘" := comp_morph. (** Setoid isomorphisms *) Record iso (A B:setoid) : Type := mkIso { iso_rel :> A -> B -> Type; (** transport forward and backward + coherence *) icomp0 : A <-> B; (* i⁺, i⁻ *) iComp0 : coh0 iso_rel icomp0; (** triangles *) trif : iso_rel <-> @srel B <-> iso_rel; (* η₁ *) trib : @srel A <-> iso_rel <-> iso_rel (* η₀ *) }. Infix "==>" := iso. Implicit Arguments icomp0 [A B]. Implicit Arguments iComp0 [A B]. Implicit Arguments trif [A B]. Implicit Arguments trib [A B]. Definition forw {A B:setoid} (i:A==>B) (a:A) : B := li0 (icomp0 i) a. Definition backw {A B:setoid} (i:A==>B) (b:B) : A := li1 (icomp0 i) b. Definition cohf {A B} (i:A==>B) (a:A) : i a (forw i a) := coh00 (iComp0 i) a. Definition cohb {A B} (i:A==>B) (b:B) : i (backw i b) b := coh01 (iComp0 i) b. (** Weak equivalence turned into iso on associated trivial setoids *) Program Definition triv_iso {X Y} (E:X<->Y) : triv X ==> triv Y := mkIso (triv X) (triv Y) (fun _ _ => unit) E triv_coh0 triv_tri triv_tri. (** Set of squares when we have 4pts in 2 setoids related by an iso *) Lemma transpf_square {A B:setoid}{i:A==>B}{a1 a2:A}{b1 b2:B} : i a1 b1 -> i a2 b2 -> (a1 --> a2)%s -> (b1 --> b2)%s. intros i1 i2 a12. apply (tri0 (trif i)) with (2:=i2). apply (tri0 (trib i)) with (1:=a12) (2:=i1). Defined. Lemma transpb_square {A B:setoid}{i:A==>B}{a1 a2:A}{b1 b2:B} : i a1 b1 -> i a2 b2 -> (b1 --> b2)%s -> (a1 --> a2)%s. intros i1 i2 b12. apply (tri2 (trib i)) with (2:=i2). apply (tri1 (trif i)) with (1:=i1)(2:=b12). Defined. Program Definition mforw {A B} (i:A==>B) : morphism A B := mkMorph _ _ (forw i) (fun x x' w => transpf_square (cohf i x) (cohf i x') w). Program Definition mbackw {A B} (i:A==>B) : morphism B A := mkMorph _ _ (backw i) (fun x x' w => transpb_square (cohb i x) (cohb i x') w). (** Proving that the type of setoids (equipped with iso and iso triangles) form a Kan simplicial set *) Program Definition iso_id {A} : A ==> A := mkIso _ _ (fun a a' => (a-->a')%s) (@scomp0 A) (@sComp0 A) (@scomp1 A) (@scomp1 A). Program Definition iso_sym {A B} (i:A==>B) : B==>A := mkIso _ _ (fun b a => i a b) (mkIff (backw i) (forw i)) (mkCoh0 (cohb i)(cohf i)) (tri_rot0 (trib i)) (tri_rot1 (trif i)). Program Definition iso_comp0 {A B C} (iab:A==>B) (iac:A==>C) : B==>C := mkIso _ _ (fun b c => { a:A & iab a b * iac a c}) (mkIff(fun b => forw iac (backw iab b)) (fun c => forw iab (backw iac c))) (mkCoh0 (fun b => let a := backw iab b in existT _ a (cohb iab b,cohf iac a)) (fun c => let a := backw iac c in existT _ a (cohf iab a,cohb iac c))) _ _. Next Obligation. intros A B C iab iac. split. intros b c c' (a,(xab,xac)) (a',(xa'b,xa'c')). assert (iaa': (a --> a')%s). apply (tri2 (trib iab)) with (1:=xab) (2:=xa'b). apply transpf_square with (1:=xac) (2:=xa'c'); trivial. intros b c c' (a,(xab,xac)) xcc'. exists a; split; trivial. apply (tri1 (trif iac)) with (1:=xac) (2:=xcc'). intros b c c' (a,(xab,xac')) xcc'. exists a; split; trivial. apply (tri2 (trif iac)) with (1:=xac') (2:=xcc'). Defined. Next Obligation. intros A B C iab iac. split. intros b b' c xbb' (a,(xab,xab')). exists a; split; trivial. apply (tri1 (trif iab)) with (1:=xab) (2:=xbb'). intros b b' c xbb' (a,(xab',xac)). exists a; split; trivial. eapply (tri2 (trif iab)) with (1:=xab') (2:=xbb'). intros b b' c (a,(xab,xac)) (a',(xa'b',xa'c)). assert (iaa': (a --> a')%s). apply (tri2 (trib iac)) with (1:=xac) (2:=xa'c). apply transpf_square with (1:=xab) (2:=xa'b'); trivial. Defined. Definition iso_Comp0 {A B C} (iab:A==>B) (iac:A==>C) : iab <-> iso_comp0 iab iac <-> iac. split; simpl. intros a b c xab xac. exists a; split; trivial. intros a b c xab (a',(xa'b,xa'c)). assert ((a-->a')%s). apply (tri2 (trib iab)) with (1:=xab) (2:=xa'b). apply (tri1 (trib iac)) with (2:=xa'c); trivial. intros a b c xac (a',(xa'b,xa'c)). assert ((a-->a')%s). apply (tri2 (trib iac)) with (1:=xac) (2:=xa'c). apply (tri1 (trib iab)) with (2:=xa'b); trivial. Defined. Program Definition iso_comp1 {A B C} (iab:A==>B) (ibc:B==>C) : A==>C := mkIso _ _ (fun a c => { b:B & iab a b * ibc b c}) (mkIff(fun a => forw ibc (forw iab a)) (fun c => backw iab (backw ibc c))) (mkCoh0(fun a => let b := forw iab a in existT _ b (cohf iab a,cohf ibc b)) (fun c => let b := backw ibc c in existT _ b (cohb iab b,cohb ibc c))) _ _. Next Obligation. intros A B C iab ibc. split; intros a c c'. intros (b,(xab,xbc)) (b',(xab',xb'c')). assert (iaa': (b --> b')%s). apply (tri0 (trif iab)) with (1:=xab) (2:=xab'). apply transpf_square with (1:=xbc) (2:=xb'c'); trivial. intros (b,(xab,xbc)) xcc'. exists b; split; trivial. apply (tri1 (trif ibc)) with (1:=xbc) (2:=xcc'). intros (b,(xab,xbc')) xcc'. exists b; split; trivial. apply (tri2 (trif ibc)) with (1:=xbc') (2:=xcc'). Defined. Next Obligation. intros A B C iab ibc. split; intros a a' c. intros xaa' (b,(xab,xbc)). exists b; split; trivial. apply (tri0 (trib iab)) with (1:=xaa') (2:=xab). intros xaa' (b,(xa'b,xbc)). exists b; split; trivial. eapply (tri1 (trib iab)) with (1:=xaa') (2:=xa'b). intros (b,(xab,xbc)) (b',(xa'b',xb'c)). assert (iaa': (b --> b')%s). apply (tri2 (trib ibc)) with (1:=xbc) (2:=xb'c). apply transpb_square with (1:=xab) (2:=xa'b'); trivial. Defined. Definition iso_Comp1 {A B C} (iab:A==>B) (ibc:B==>C) : iab <-> ibc <-> iso_comp1 iab ibc. split; simpl; intros a b c. intros xab (b',(xab',xb'c)). assert ((b-->b')%s). apply (tri0 (trif iab)) with (1:=xab) (2:=xab'). apply (tri1 (trib ibc)) with (2:=xb'c); trivial. intros xab xbc. exists b; split; trivial. intros (b',(xab',xb'c)) xbc. assert ((b-->b')%s). apply (tri2 (trib ibc)) with (1:=xbc) (2:=xb'c). apply (tri2 (trif iab)) with (1:=xab'); trivial. Defined. Program Definition iso_comp2 {A B C} (iac:A==>C) (ibc:B==>C) : A==>B := mkIso _ _ (fun a b => { c:C & ibc b c * iac a c}) (mkIff(fun a => backw ibc (forw iac a)) (fun b => backw iac (forw ibc b))) (mkCoh0(fun a => let c := forw iac a in existT _ c (cohb ibc c,cohf iac a)) (fun b => let c := forw ibc b in existT _ c (cohf ibc b,cohb iac c))) _ _. Next Obligation. intros A B C iac ibc. split; intros a b b'. intros (c,(xbc,xac)) (c',(xb'c',xac')). assert (iaa': (c --> c')%s). apply (tri0 (trif iac)) with (1:=xac) (2:=xac'). apply transpb_square with (1:=xbc) (2:=xb'c'); trivial. intros (c,(xbc,xac)) xbb'. exists c; split; trivial. apply (tri0 (trib ibc)) with (1:=xbb') (2:=xbc). intros (c,(xb'c,xac)) xbb'. exists c; split; trivial. apply (tri1 (trib ibc)) with (1:=xbb') (2:=xb'c). Defined. Next Obligation. intros A B C iac ibc. split; intros a a' b. intros xaa' (c,(xbc,xac)). exists c; split; trivial. apply (tri0 (trib iac)) with (1:=xaa') (2:=xac). intros xaa' (c,(xbc,xa'c)). exists c; split; trivial. eapply (tri1 (trib iac)) with (1:=xaa') (2:=xa'c). intros (c,(xbc,xac)) (c',(xbc',xa'c')). assert (iaa': (c --> c')%s). apply (tri0 (trif ibc)) with (1:=xbc) (2:=xbc'). apply transpb_square with (1:=xac) (2:=xa'c'); trivial. Defined. Definition iso_Comp2 {A B C} (iac:A==>C) (ibc:B==>C) : iso_comp2 iac ibc <-> ibc <-> iac. split; simpl; intros a b c. intros (c',(xbc',xac')) xac. assert ((c-->c')%s). apply (tri0 (trif iac)) with (1:=xac) (2:=xac'). apply (tri2 (trif ibc)) with (1:=xbc'); trivial. intros (c',(xbc',xac')) xbc. assert ((c-->c')%s). apply (tri0 (trif ibc)) with (1:=xbc) (2:=xbc'). apply (tri2 (trif iac)) with (1:=xac'); trivial. intros xac xbc. exists c; split; trivial. Defined. Definition iso_comp_tetra0 {A B C D} (iab:A==>B) (iac:A==>C) (iad:A==>D) (ibc:B==>C) (ibd:B==>D) (icd:C==>D) (tabc:iab<->ibc<->iac) (tabd:iab<->ibd<->iad) (tacd:iac<->icd<->iad) : ibc<->icd<->ibd. split. intros b c d xbc xbd. assert (xab:=cohb iab b). set (a:=backw iab b) in *. assert (xac := tri1 tabc xab xbc). assert (xad := tri1 tabd xab xbd). apply (tri0 tacd xac xad). intros b c d xbc xcd. assert (xab:=cohb iab b). set (a:=backw iab b) in *. assert (xac := tri1 tabc xab xbc). assert (xad := tri1 tacd xac xcd). apply (tri0 tabd xab xad). intros b c d xbd xcd. assert (xab:=cohb iab b). set (a:=backw iab b) in *. assert (xad := tri1 tabd xab xbd). assert (xac := tri2 tacd xad xcd). apply (tri0 tabc xab xac). Defined. Definition iso_comp_tetra1 {A B C D} (iab:A==>B) (iac:A==>C) (iad:A==>D) (ibc:B==>C) (ibd:B==>D) (icd:C==>D) (tabc:iab<->ibc<->iac) (tabd:iab<->ibd<->iad) (tbcd:ibc<->icd<->ibd) : iac<->icd<->iad. split. intros a c d xac xad. assert (xab:=cohf iab a). set (b:=forw iab a) in *. assert (xbc := tri0 tabc xab xac). assert (xbd := tri0 tabd xab xad). apply (tri0 tbcd xbc xbd). intros a c d xac xcd. assert (xab:=cohf iab a). set (b:=forw iab a) in *. assert (xbc := tri0 tabc xab xac). assert (xbd := tri1 tbcd xbc xcd). apply (tri1 tabd xab xbd). intros a c d xad xcd. assert (xab:=cohf iab a). set (b:=forw iab a) in *. assert (xbd := tri0 tabd xab xad). assert (xbc := tri2 tbcd xbd xcd). apply (tri1 tabc xab xbc). Defined. Definition iso_comp_tetra2 {A B C D} (iab:A==>B) (iac:A==>C) (iad:A==>D) (ibc:B==>C) (ibd:B==>D) (icd:C==>D) (tabc:iab<->ibc<->iac) (tacd:iac<->icd<->iad) (tbcd:ibc<->icd<->ibd) : iab<->ibd<->iad. split. intros a b d xab xad. assert (xac:=cohf iac a). set (c:=forw iac a) in *. assert (xcd := tri0 tacd xac xad). assert (xbc := tri0 tabc xab xac). apply (tri1 tbcd xbc xcd). intros a b d xab xbd. assert (xac:=cohf iac a). set (c:=forw iac a) in *. assert (xbc := tri0 tabc xab xac). assert (xcd := tri0 tbcd xbc xbd). apply (tri1 tacd xac xcd). intros a b d xad xbd. assert (xac:=cohf iac a). set (c:=forw iac a) in *. assert (xcd := tri0 tacd xac xad). assert (xbc := tri2 tbcd xbd xcd). apply (tri2 tabc xac xbc). Defined. Program Definition iso_comp_tetra3 {A B C D} (iab:A==>B) (iac:A==>C) (iad:A==>D) (ibc:B==>C) (ibd:B==>D) (icd:C==>D) (tabd:iab<->ibd<->iad) (tacd:iac<->icd<->iad) (tbcd:ibc<->icd<->ibd) : iab<->ibc<->iac. split. intros a b c xab xac. assert (xad:=cohf iad a). set (d:=forw iad a) in *. assert (xbd := tri0 tabd xab xad). assert (xcd := tri0 tacd xac xad). apply (tri2 tbcd xbd xcd). intros a b c xab xbc. assert (xad:=cohf iad a). set (d:=forw iad a) in *. assert (xbd := tri0 tabd xab xad). assert (xcd := tri0 tbcd xbc xbd). apply (tri2 tacd xad xcd). intros a b c xac xbc. assert (xad:=cohf iad a). set (d:=forw iad a) in *. assert (xcd := tri0 tacd xac xad). assert (xbd := tri1 tbcd xbc xcd). apply (tri2 tabd xad xbd). Defined. Program Definition U : context := mkCtx setoid iso (fun X0 X1 X2 X01 X02 X12 => X01 <-> X12 <-> X02) (mkIff(fun A=>A)(fun A=>A)) (mkCoh0 (@iso_id) (@iso_id)) (mkTri (@iso_comp0) (@iso_comp1) (@iso_comp2)) (mkCoh1 (@iso_Comp0) (@iso_Comp1) (@iso_Comp2)) (mkTetra (@iso_comp_tetra0) (@iso_comp_tetra1) (@iso_comp_tetra2) (@iso_comp_tetra3)). Definition ηU (A:U) : A-->A := @iso_id A. Definition η0U {A B:U} (i:A-->B) : ηU A --> i --> i := trib i. Definition η1U {A B:U} (i:A-->B) : i --> ηU B --> i := trif i. Definition η10U (A:U) : ηU A --> ηU A --> ηU A := scomp1 A. (** Type formation judgement (types in a context) *) Definition family (S:context) := sub S U. Notation s2c := setoid2context. Definition sfamily (A:setoid) := family (s2c A). Notation "u -->[ a ] u'" := (sub_w (_:family _) a u u'). Notation "u -->[ a ] u'" := (sub_w (_:sfamily _) a u u') : setoid_scope. Lemma eq_subsT_id S (A:family S) : A ∘ ids = etas A. reflexivity. Defined. Lemma eq_substT_assoc S1 S2 S3 (A:family S3) (g:sub S2 S3) (h:sub S1 S2) : (A ∘ g) ∘ h = A ∘ (g ∘ h). reflexivity. Defined. (** Term judgments *) Record elt (S:context) (A:family S) := mkElt { elt_f :> forall s:S, A s; elt_w : forall {s0 s1} (w:s0-->s1), elt_f s0 -->[w] elt_f s1 }. Implicit Arguments elt_w [S A s0 s1]. Program Definition etae {S} {A:family S} (t:elt S A) : elt S (etas A) := mkElt _ _ (fun s => t s) (fun s0 s1 w => elt_w t w). Definition etae' {S} {A:family S} (t:elt S A) : elt S A := mkElt _ _ (fun s => t s) (fun s0 s1 w => elt_w t w). (** Term level substitution *) Program Definition subst {S T} {A:family T} (t:elt T A) (f:sub S T) : elt S (A ∘ f) := mkElt _ _ (fun s => t (f s)) (fun s0 s1 w => elt_w t (sub_w f w)). Lemma eq_subs_id S (A:family S) (t:elt S A) : subst t ids = etae t. reflexivity. Defined. Lemma eq_subst_assoc S1 S2 S3 (g:sub S2 S3) (h:sub S1 S2)(A:family S3) (t:elt S3 A) : subst (subst t g) h = subst t (g ∘ h). reflexivity. Defined. (** Derived properties of setoids and families: reflexivity, etc. *) Definition ηs {S:setoid} (s:S) : (s-->s)%s := tri2 (scomp1 S) (coh00 (sComp0 S) s) (coh00 (sComp0 S) s). Definition η {S:context} (s:S) : s-->s := tri2 (comp1 S) (coh00 (Comp0 S) s) (coh00 (Comp0 S) s). Lemma η0 {S:context} {s1 s2:S} (s12:s1-->s2) : η s1 --> s12 --> s12. unfold η. set (s11' := coh00 (Comp0 S) s1). assert (s111' := coh12 (Comp1 S) s11' s11'). assert (s11'2 := coh10 (Comp1 S) s11' s12). eapply (tet2 (comp2 S)) with (1:=s111') (2:=s11'2) (3:=s11'2). Defined. Lemma η1 {S:context} {s1 s2:S} (s12:s1-->s2) : s12 --> η s2 --> s12. unfold η. set (s22' := coh00 (Comp0 S) s2). assert (s222' := coh12 (Comp1 S) s22' s22'). assert (s122' := coh11 (Comp1 S) s12 s22'). eapply (tet3 (comp2 S)) with (1:=s122') (2:=s122') (3:=s222'). Defined. Lemma η3 {S:context} (s:S) : η s --> η s --> η s. (* or special case of η0 or η1 *) unfold η at 1. eapply (tet3 (comp2 S)). eapply (coh12 (Comp1 S)). eapply (coh12 (Comp1 S)). eapply (coh12 (Comp1 S)). Defined. Program Definition γs {S:setoid} {A:sfamily S} {s:S} {x0 x1:A s} (x01:(x0-->x1)%s) : (x0 -->[ηs s] x1)%s := let s02 := coh00 (sComp0 S) s in let i := sub_w A s02 in let t := sub_t A tt in tri2 t (cohf i x0) (tri0 (trib i) x01 (cohf i x0)). Program Definition γ {S:context} {A:family S} {s:S} {x0 x1:A s} (x01:(x0-->x1)%s) : x0-->[η s] x1 := let s02 := coh00 (Comp0 S) s in let s012 := coh12 (Comp1 S) s02 s02 in let i := sub_w A s02 in let t := sub_t A s012 in tri2 t (cohf i x0) (tri0 (trib i) x01 (cohf i x0)). (*****************************************************************************************************) (** Lifting setoids as types: constant types, e.g. nat *) Definition cst_type (X:setoid) {S:context} : family S := mkSub S U (fun _ => X) (fun _ _ _ => iso_id) (fun _ _ _ _ _ _ _ => scomp1 X). Lemma eq_cst S T X (f:sub S T) : (cst_type X) ∘ f = cst_type X. reflexivity. Qed. Program Definition cst {X:setoid} (x:X) {S:context} : elt S (cst_type X) := mkElt _ (cst_type X) (fun s => x) (fun _ _ _ => ηs x). Program Definition Nat : setoid := mkSetRefl nat (fun n m => n=m) (@eq_refl nat) _. Next Obligation. split; intros; subst; trivial. Defined. Definition nat2Nat (n:nat) {S} : elt S (cst_type Nat) := cst (X:=Nat) n. (*****************************************************************************************************) (** Extending a context with a type *) Record ext_obj {S} {A:family S} := mkCO_ { pi1 : S ; pi2 : A pi1}. Implicit Arguments ext_obj [ ]. Record ext_rel {S} {A:family S} {sa sa':ext_obj S A} := mkCR_ { pir1 : pi1 sa --> pi1 sa' ; pir2 : pi2 sa -->[pir1] pi2 sa' }. Implicit Arguments ext_rel []. Definition ext_tri {S} {A:family S} {sa1 sa2 sa3} (sa12:ext_rel S A sa1 sa2) (sa13:ext_rel S A sa1 sa3) (sa23:ext_rel S A sa2 sa3) := ctri S (pir1 sa12) (pir1 sa13) (pir1 sa23). (** no triangle for A since A is a setoid *) Program Definition ext (S:context) (A:family S) : context := mkCtx (ext_obj S A) (ext_rel S A) (@ext_tri S A) (mkIff (fun sa => mkCO_ S A (li0 (comp0 S) (pi1 sa)) (forw (sub_w A (coh00 (Comp0 S) (pi1 sa))) (pi2 sa))) (fun sa' => mkCO_ S A (li1 (comp0 S) (pi1 sa')) (backw (sub_w A (coh01 (Comp0 S) (pi1 sa'))) (pi2 sa')))) (mkCoh0(fun sa => mkCR_ S A _ _ (coh00 (Comp0 S) (pi1 sa)) (cohf (sub_w A _) (pi2 sa))) (fun sa' => mkCR_ S A _ _ (coh01 (Comp0 S) (pi1 sa')) (cohb (sub_w A _) (pi2 sa')))) _ _ _. Next Obligation. split; intros. exists (tri0 (comp1 S) (pir1 X) (pir1 X0)). eapply (tri0 (sub_t A (coh10 (Comp1 S) (pir1 X) (pir1 X0))) (pir2 X) (pir2 X0)). exists (tri1 (comp1 S) (pir1 X) (pir1 X0)). eapply (tri1 (sub_t A (coh11 (Comp1 S) (pir1 X) (pir1 X0))) (pir2 X) (pir2 X0)). exists (tri2 (comp1 S) (pir1 X) (pir1 X0)). eapply (tri2 (sub_t A (coh12 (Comp1 S) (pir1 X) (pir1 X0))) (pir2 X) (pir2 X0)). Defined. Next Obligation. split; intros. red; simpl; apply (coh10(Comp1 S)). red; simpl; apply (coh11(Comp1 S)). red; simpl; apply (coh12(Comp1 S)). Defined. Next Obligation. intros S A. split; unfold ext_tri; simpl; intros a b c d ab ac ad bc bd cd t1 t2 t3. apply (tet0 (comp2 S) t1 t2 t3). apply (tet1 (comp2 S) t1 t2 t3). apply (tet2 (comp2 S) t1 t2 t3). apply (tet3 (comp2 S) t1 t2 t3). Defined. Infix "+" := ext : type_scope. Definition mkCO {S:context} {A:family S} (pi1:S) (pi2:A pi1): S+A := mkCO_ S A pi1 pi2. Infix "+" := mkCO : point_scope. Delimit Scope point_scope with p. Definition mkCR {S} {A:family S} {t0 t1:S} {x0:A t0} {x1:A t1} (a:t0-->t1) (b:x0-->[a] x1) : (t0+x0)%p --> (t1+x1)%p := mkCR_ S A (t0+x0)%p (t1+x1)%p a b. Infix "+" := mkCR : path_scope. Delimit Scope path_scope with w. Definition mkCT {S} {A:family S} {s0 s1 s2:S} {a0:A s0}{a1:A s1}{a2:A s2} {s01 s02 s12} (t:s01 --> s12 --> s02) (a01:a0-->[s01]a1) (a02:a0-->[s02]a2) (a12:a1-->[s12]a2) : (s01+a01)%w --> (s12+a12)%w --> (s02+a02)%w := t. (* Substitution operations and properties *) Definition cons {S T A} (f:sub S T) (t:elt S (A ∘ f)) : sub S (T+A) := mkSub _ _ (fun (x:S) => (f x + t x)%p) (fun x x' w => (sub_w f w + elt_w t w)%w) (fun x0 x1 x2 x01 x02 x12 t => sub_t f t). (** Shift of substitution *) Program Definition proj1 {S:context} {A:family S} : sub (S+A) S := mkSub (S+A) S (@pi1 S A) (@pir1 S A) (fun x0 x1 x2 x01 x02 x12 t => t). Notation "⇑ t" := (t ∘ proj1) (at level 9, t at level 9). Notation "↑ t" := (subst t proj1) (at level 9, t at level 9). (** "de Bruijn index" 0 *) Program Definition proj2 {S:context} {A:family S} : elt (S+A) ⇑A := mkElt _ _ (@pi2 S A) (@pir2 S A). (** Lift of substitution (used when crossing a binder) *) Definition lift {S T} {A:family T} (f:sub S T) : sub (S+(A ∘ f)) (T+A) := cons ⇑f (proj2(A:=A∘f)). Lemma eq_proj1 S T (A:family T) (f:sub S T) (a:elt S (A ∘ f)) : proj1 ∘ (cons f a) = etas f. reflexivity. Defined. Lemma eq_proj2 S T (A:family T) (f:sub S T) (a:elt S (A ∘ f)) : subst proj2 (cons f a) = etae a. reflexivity. Defined. Lemma eq_map_cons {D S T} {f:sub S T} {g:sub D S} {A:family T} {u:elt S (A ∘ f)} : cons f u ∘ g = cons (f ∘ g) (subst u g). reflexivity. Defined. (** Type families *) Record isoFAM {A1 A2} (i12:A1==>A2) (F1:sfamily A1) (F2:sfamily A2) := mkIsoFAM { isoF : forall {a1:A1} {a2:A2} (w:i12 a1 a2), F1 a1 ==> F2 a2; (* Fα *) triF : forall a1 a2 a2' (w12:i12 a1 a2) (w12':i12 a1 a2')(w22':(a2 --> a2')%s), isoF w12 <-> sub_w F2 w22' <-> isoF w12'; (* η₁F *) triB : forall a1 a1' a2 (w11': (a1 --> a1')%s)(w12:i12 a1 a2) (w1'2:i12 a1' a2), sub_w F1 w11' <-> isoF w1'2 <-> isoF w12 (* η₀F *) }. Implicit Arguments mkIsoFAM [A1 A2 i12 F1 F2]. Implicit Arguments isoF [A1 A2 i12 F1 F2 a1 a2]. Implicit Arguments triF [A1 A2 i12 F1 F2 a1 a2 a2']. Implicit Arguments triB [A1 A2 i12 F1 F2 a1 a1' a2]. Definition triFAM {A1 A2 A3}{F1:sfamily A1} {F2:sfamily A2} {F3:sfamily A3} {i12 : A1==>A2} {i13 : A1 ==> A3} {i23 : A2 ==> A3} (j12:isoFAM i12 F1 F2) (j13:isoFAM i13 F1 F3) (j23:isoFAM i23 F2 F3) := forall a1 a2 a3 (a12:i12 a1 a2) (a13:i13 a1 a3) (a23:i23 a2 a3), isoF j12 a12 <-> isoF j23 a23 <-> isoF j13 a13. Record FAM (S:context) (A:family S) := mkFAM { Family :> forall s, sfamily (A s); Fam_w : forall {s1 s2} (s12:s1-->s2), isoFAM (sub_w A s12) (Family s1) (Family s2); Fam_t : forall (s1 s2 s3:S) (s12:s1-->s2) (s13:s1-->s3) (s23:s2-->s3), s12 --> s23 --> s13 -> triFAM (Fam_w s12) (Fam_w s13) (Fam_w s23) }. Implicit Arguments Fam_w [S A s1 s2]. Implicit Arguments Fam_t [S A s1 s2 s3 s12 s23 s13]. Program Definition substF {T S} {A:family S} (F:FAM S A) (f:sub T S) : FAM T (A ∘ f) := mkFAM _ (A ∘ f) (fun s => F (f s)) (fun s1 s2 s12 => Fam_w F (sub_w f s12)) (fun s1 s2 s3 s12 s23 s13 t => Fam_t F (sub_t f t)). Lemma substF_comp {D S T} {g:sub D T} {f:sub T S} {A:family S} (F:FAM S A) : substF (substF F f) g = substF F (f ∘ g). reflexivity. Defined. Program Definition App {S:context} {A:family S} (F:FAM S A) (a:elt S A) : family S := mkSub S U (fun s => F s (a s)) (fun s1 s2 s12 => isoF (Fam_w F s12) (elt_w a s12)) (fun s1 s2 s3 s12 s13 s23 t => Fam_t F t _ _ _ (elt_w a s12) (elt_w a s13) (elt_w a s23)). Program Definition Lam {S:context} {A:family S} (B:family(S+A)) : FAM S A := mkFAM S A (fun s => mkSub (s2c (A s)) U (fun a => B(s+a)%p) (fun a1 a2 a12 => sub_w B (η s + γ a12)%w) (fun a1 a2 a3 a12 a13 a23 a123 => sub_t B (mkCT (η3 s) (γ a12) (γ a13) (γ a23)))) (fun s1 s2 s12 => mkIsoFAM (fun a1 a2 (a12:a1-->[s12]a2) => sub_w B (s12+a12)%w) (fun a1 a2 a2' a12 a12' a22' => sub_t B (mkCT (η1 s12) a12 a12' (γ a22'))) (fun a1 a1' a2 a11' a12 a1'2 => sub_t B (mkCT (η0 s12) (γ a11') a12 a1'2))) (fun s1 s2 s3 s12 s13 s23 s123 a1 a2 a3 a12 a13 a23 => sub_t B (mkCT s123 a12 a13 a23)). (** Alternative definition for Lam. This one is closer to the term-level lambda (def lambda below). Thus it's a step towards the generalization to arbitrary dimensions. *) Program Definition Lam' {S:context} {A:family S} (B:family(S+A)) : FAM S A := mkFAM S A (fun s => mkSub (s2c (A s)) U (fun a => B(s+a)%p) (fun a1 a2 a12 => _) (* η(Lam' B)ρ *) (fun a1 a2 a3 a12 a13 a23 a123 => _)) (* η₁η(Lam' B)ρ *) (fun s1 s2 s12 => mkIsoFAM (fun a1 a2 (a12:a1-->[s12]a2) => sub_w B (s12+a12)%w) (fun a1 a2 a2' a12 a12' a22' => _) (* η₁(Lam' B)α *) (fun a1 a2 a2' a12 a1'2 a11' => _)) (* η₀(Lam' B)α *) (fun s1 s2 s3 s12 s13 s23 s123 a1 a2 a3 a12 a13 a23 => sub_t B (mkCT s123 a12 a13 a23)). Next Obligation. intros S A B s a1 a2 a12. pose (s':=li0(comp0 S) s). assert (ss' := coh00(Comp0 S) s). fold s' in ss'. pose (a2' := forw (sub_w A ss') a2). assert (a22' := cohf (sub_w A ss') a2). fold a2' in a22'. assert (a12' := tri1(trib(sub_w A ss')) a12 a22'). eapply (tri2(comp1 U)) with (B(s'+a2')%p). apply (sub_w B (ss'+a12')%w). apply (sub_w B (ss'+a22')%w). Defined. Next Obligation. intros S A B s a1 a2 a3 a12 a13 a23 _. simpl in *|-. unfold Lam'_obligation_1. pose (s':=li0(comp0 S) s). set (ss' := coh00(Comp0 S) s). fold s' in ss'. pose (s's' := tri0 (comp1 S) ss' ss'). pose (a2' := forw (sub_w A ss') a2). pose (a22' := cohf (sub_w A ss') a2). fold a2' in a22'. pose (a12' := tri1(trib(sub_w A ss')) a12 a22'). pose (a3' := forw (sub_w A ss') a3). pose (a33' := cohf (sub_w A ss') a3). fold a3' in a33'. pose (a13' := tri1(trib(sub_w A ss')) a13 a33'). pose (a23' := tri1 (trib (sub_w A ss')) a23 a33'). pose (t1 := η0U(sub_w A ss')). pose (t0 := η10U (A s)). pose (t2 := tet2 (comp2 U) t0 t1 t1). pose (t3 := sub_t A (coh10 (Comp1 S) ss' ss')). pose (a2'3' := tri0 t3 a22' a23'). assert (u0 := coh12 (Comp1 U) (sub_w B (ss'+a12')%w) (sub_w B (ss'+a22')%w)). assert (u1 := sub_t B (mkCT (coh10 (Comp1 S) ss' ss') a22' a23' a2'3')). assert (u2 := sub_t B (mkCT (coh10 (Comp1 S) ss' ss') a12' a13' a2'3')). assert (u3 := tet2 (comp2 U) u0 u2 u1). assert (u4 := coh12 (Comp1 U) (sub_w B (ss'+a23')%w) (sub_w B (ss'+a33')%w)). assert (u5 := coh12 (Comp1 U) (sub_w B (ss'+a13')%w) (sub_w B (ss'+a33')%w)). assert (u6 := tet3 (comp2 U) u3 u5 u4). exact u6. Defined. Next Obligation. intros S A B s1 s2 s12 a1 a2 u2 a12 a1u2 a2u2. simpl sub_w. unfold Lam'_obligation_1. pose (s2' := li0 (comp0 S) s2). pose (s22' := coh00 (Comp0 S) s2). pose (s12' := tri1 (comp1 S) s12 s22'). fold s2' in s22', s12'. assert (s122' := coh11 (Comp1 S) s12 s22'). fold s12' in s122'. pose (u2' := forw (sub_w A s22') u2). pose (u22' := cohf (sub_w A s22') u2). fold u2' in u22'. pose (a2u2' := tri1 (trib (sub_w A s22')) a2u2 u22'). pose (a1u2' := tri1 (sub_t A s122') a12 a2u2'). assert (t0 := sub_t B (mkCT s122' a1u2 a1u2' u22')). assert (t1 := sub_t B (mkCT s122' a12 a1u2' a2u2')). assert (t2 := coh12 (Comp1 U) (sub_w B (s22'+a2u2')%w) (sub_w B (s22'+u22')%w)). assert (t3 := tet3 (comp2 U) t1 t0 t2). exact t3. Defined. Next Obligation. intros S A B s1 s2 s12 a1 u1 a2 a1u1 a12 u1a2. simpl sub_w. unfold Lam'_obligation_1. pose (s1' := li0 (comp0 S) s1). set (s11' := coh00 (Comp0 S) s1). pose (s1'2 := tri0 (comp1 S) s11' s12). fold s1' in s11', s1'2. assert (s11'2 := coh10 (Comp1 S) s11' s12). fold s1'2 in s11'2. pose (u1' := forw (sub_w A s11') u1). pose (u11' := cohf (sub_w A s11') u1). fold u1' in u11'. pose (a1u1' := tri1 (trib (sub_w A s11')) a1u1 u11'). pose (u1'a2 := tri0 (sub_t A s11'2) u11' u1a2). assert (t0 := sub_t B (mkCT s11'2 u11' u1a2 u1'a2)). assert (t1 := sub_t B (mkCT s11'2 a1u1' a12 u1'a2)). assert (t2 := coh12 (Comp1 U) (sub_w B (s11'+a1u1')%w) (sub_w B (s11'+u11')%w)). assert (t3 := tet2 (comp2 U) t2 t1 t0). exact t3. Qed. Lemma eq_betaF {T S:context} {A:family S} (B:family(S+A)) (f:sub T S) (a:elt T (A∘f)) : App (substF(Lam B)f) a = B∘(cons f a). reflexivity. Defined. (** Another set of squares (top square of a cube) *) Lemma isoFAM_cubef {A1 A2} {a12:A1==>A2} {F1:sfamily A1} {F2:sfamily A2} (M:isoFAM a12 F1 F2) {a1 a1' a2 a2' x1 x1' x2 x2'} (w12:a12 a1 a2) (w1'2':a12 a1' a2') (w11':(a1-->a1')%s) (w22':(a2 --> a2')%s) : isoF M w12 x1 x2 -> isoF M w1'2' x1' x2' -> (x1 -->[w11'] x1')%s -> (x2 -->[w22'] x2')%s. intros j12 j1'2' j11'. assert (w12' := tri1 (trif a12) w12 w22'). assert (j12' : isoF M w12' x1 x2'). apply (tri1 (triB M w11' w12' w1'2') j11' j1'2'). apply (tri0 (triF M w12 w12' w22') j12 j12'). Defined. Lemma isoFAM_cubeb {A1 A2} {a12:A1==>A2} {F1:sfamily A1} {F2:sfamily A2} (M:isoFAM a12 F1 F2) {a1 a1' a2 a2' x1 x1' x2 x2'} (w12:a12 a1 a2) (w1'2':a12 a1' a2') (w11':(a1-->a1')%s) (w22':(a2 --> a2')%s) : isoF M w12 x1 x2 -> isoF M w1'2' x1' x2' -> (x2 -->[w22'] x2')%s -> (x1 -->[w11'] x1')%s. intros j12 j1'2' j22'. assert (w1'2 := tri0 (trib a12) w11' w12). assert (j1'2 : isoF M w1'2 x1' x2). apply (tri2 (triF M w1'2 w1'2' w22') j1'2' j22'). apply (tri2 (triB M w11' w12 w1'2) j12 j1'2). Defined. (*****************************************************************************************************) (** Propositions *) (** The setoid of propsitions *) Definition Ω : setoid := mkSetRefl Type (fun X Y => X<->Y) (fun _ => refl_iffT) tri_iffT. Definition prop {S:context} : family S := cst_type Ω. (** Propositions as types with trivial equality *) Program Definition Tprop {S:context} (p:elt S prop) : family S := mkSub S U (fun s => triv (p s)) (fun s0 s1 w => triv_iso (elt_w p w)) (fun _ _ _ _ _ _ _ => triv_tri). Definition Tprop_elt {S} {A:elt S prop} (x:forall s, A s) : elt S (Tprop A) := mkElt _ (Tprop A) x (fun _ _ _ => tt). Lemma eq_ctxt_Tprop S T (P:elt S prop) (f:sub T S) : (Tprop P) ∘ f = Tprop (subst P f). reflexivity. Defined. (** Impredicative product *) Program Definition Forall {S} A (B:elt (S+A) prop) : elt S prop := mkElt _ prop (fun s => inh (forall x:A s, B (s+x)%p)) _. Next Obligation. intros. split; apply inh_map; intros f x. apply (iffLR (elt_w B (w + cohb _ x)%w) (f (backw _ x))). apply (iffRL (elt_w B (w + cohf _ x)%w) (f (forw _ x))). Defined. (*****************************************************************************************************) (** Identity types *) Program Definition eq {S:context} (A:family S) (x y:elt S A) : elt S prop := mkElt _ prop (fun s:S => inh (x s --> y s)%s) _. Next Obligation. simpl; intros. assert (xm := elt_w x w). assert (ym := elt_w y w). split; apply inh_map; intros X. apply transpf_square with (1:=xm) (2:=ym) (3:=X). apply transpb_square with (1:=xm) (2:=ym) (3:=X). Defined. Lemma eq_ctxt_eq S T (A:family S) x y (f:sub T S) : subst (eq A x y) f = eq (A ∘ f) (subst x f) (subst y f). reflexivity. Defined. Definition Id {S:context} (A:family S) (x y:elt S A) := Tprop(eq A x y). Program Definition Refl {S:context} {A:family S} (x:elt S A) : elt S (Id A x x) := Tprop_elt (fun s => Inh (ηs (x s))). Lemma eq_ctxt_Refl {S T} (f:sub T S) {A} (x:elt S A) : subst (Refl x) f = Refl (subst x f). reflexivity. Defined. Program Definition proof_irrelevance {S:context} (P:elt S prop) (x y:elt S (Tprop P)) : elt S (Id (Tprop P) x y) := Tprop_elt (fun _ => Inh tt). Program Definition leibniz {S:context} {A:family S} {x y:elt S A} {P:FAM S A} (e:elt S (Id A x y)) (h:elt S (App P x)) : elt S (App P y) := mkElt _ (App P y) (fun s => forw (sub_w (P s) (type_in_type (e s))) (h s)) _. Next Obligation. intros S A x y P e h s1 s2 s12. simpl. pose (rmk := type_in_type (e s1)). assert (rmk2 : x s1 -->[ s12] y s2). eapply (tri1 (trib (sub_w A s12))) with (1:=rmk) (2:=elt_w y s12). eapply (tri0 (triB (Fam_w P s12) rmk rmk2 (elt_w y s12))). eapply cohf. eapply (tri1 (triF (Fam_w P s12) (elt_w x s12) rmk2 (type_in_type(e s2)))). 2:eapply cohf. apply (elt_w h). Defined. (*****************************************************************************************************) (** Squash *) Program Definition Squash {S} (A:family S) : elt S prop := mkElt _ prop (fun s => inh (A s)) (fun s1 s2 s12 => mkIff(inh_map (forw (sub_w A s12))) (inh_map (backw (sub_w A s12)))). Definition squash {S} {A:family S} (x:elt S A) : elt S (Tprop(Squash A)) := Tprop_elt (A:=Squash A) (fun s => Inh (x s)). (** def: A is a proof-irrelevant family *) Definition ishProp {S} (A:family S) := forall s0 s1 (a:s0-->s1) (u0:A s0) (u1:A s1), u0 -->[a] u1. Program Definition uch {S} (A:family S) (h:ishProp A) (e:elt S (Tprop(Squash A))) : elt S A := mkElt _ A (fun s => type_in_type (e s)) (fun s1 s2 w => h _ _ _ _ _). (*****************************************************************************************************) (** Products *) (** Sections: just like elt, but domain is a setoid, which is in a lower universe than contexts *) Record sect_type (S:setoid) (A:sfamily S) := mkSect { sect :> forall s:S, A s; sect_w : forall {s0 s1} (w:(s0-->s1)%s), (sect s0 -->[w] sect s1)%s }. Implicit Arguments sect_w [S A s0 s1]. Definition sec_rel {S A} (x1 x2 : sect_type S A) : Type := forall s1 s2 (w:(s1-->s2)%s), (x1 s1 -->[w] x2 s2)%s. Lemma sec_tri {S A} : (sec_rel(A:=A)(S:=S)) <-> sec_rel <-> sec_rel. split; intros x0 x1 x2; unfold sec_rel. intros x01 x02 u1 u2 u12. assert (u01 := coh01 (sComp0 S) u1). pose (u02 := tri1 (scomp1 S) u01 u12). set (u0 := iffRL (scomp0 S) u1) in u01, u02. eapply (tri0 (sub_t A tt)) with (a:=x0 u0). eapply x01 with (w:=u01). eapply x02 with (w:=u02). intros x01 x12 u0 u2 u02. assert (u01 := coh00 (sComp0 S) u0). pose (u12 := tri0 (scomp1 S) u01 u02). set (u1 := iffLR (scomp0 S) u0) in u01, u12. eapply (tri1 (sub_t A tt)) with (b:=x1 u1). eapply x01 with (w:=u01). eapply x12 with (w:=u12). intros x02 x12 u0 u1 u01. assert (u02 := coh00 (sComp0 S) u0). pose (u12 := tri0 (scomp1 S) u01 u02). set (u2 := iffLR (scomp0 S) u0) in u02, u12. eapply (tri2 (sub_t A tt)) with (c:=x2 u2). eapply x02 with (w:=u02). eapply x12 with (w:=u12). Defined. Program Definition section (S:setoid) (A:sfamily S) : setoid := mkSetRefl (sect_type S A) (@sec_rel S A) (@sect_w S A) (@sec_tri S A). Program Definition section_iso {A1 A2} (a12:A1==>A2) {F1 F2} (M:isoFAM a12 F1 F2) : section A1 F1 ==> section A2 F2 := mkIso (section _ F1) (section _ F2) (fun f1 f2 => forall (a1:A1) a2 (w:a12 a1 a2), isoF M w (f1 a1) (f2 a2)) (mkIff(fun f => mkSect _ _ (fun a2 => forw (isoF M (cohb a12 a2)) (f (backw a12 a2))) _) (fun f => mkSect _ _ (fun a1 => backw (isoF M (cohf a12 a1)) (f (forw a12 a1))) _)) _ _ _. Next Obligation. simpl; intros A1 A2 a12 F1 F2 M f a2 a2' b. assert (rmk : (backw a12 a2 --> backw a12 a2')%s). apply transpb_square with (1:=cohb a12 a2) (2:=cohb a12 a2') (3:=b). eapply (isoFAM_cubef M) with (w12:=cohb a12 a2) (w1'2':=cohb a12 a2') (w11':=rmk). eapply cohf. eapply cohf. apply (sect_w f). Defined. Next Obligation. simpl; intros A1 A2 a12 F1 F2 M f a1 a1' b. assert (rmk : (forw a12 a1 --> forw a12 a1')%s). apply transpf_square with (1:=cohf a12 a1) (2:=cohf a12 a1') (3:=b). eapply (isoFAM_cubeb M) with (w12:=cohf a12 a1) (w1'2':=cohf a12 a1') (w22':=rmk). eapply cohb. eapply cohb. apply (sect_w f). Defined. Next Obligation. intros A1 A2 i12 F1 F2 M. split; simpl. intros f a1 a2 w. assert (rmk : i12 (backw i12 a2) a2). eapply cohb. assert (rmk2 : (a1 --> backw i12 a2)%s). eapply (tri2 (trib i12)) with (1:=w) (2:=rmk). eapply (tri1 (triB M _ _ _));[|eapply cohf]. eapply (sect_w f) with (w:=rmk2). intros f a1 a2 w. assert (rmk : i12 a1 (forw i12 a1)). eapply cohf. assert (rmk2 : (forw i12 a1 --> a2)%s). eapply (tri0 (trif i12)) with (1:=rmk) (2:=w). eapply (tri1 (triF M _ _ _));[eapply cohb|]. eapply (sect_w f) with (w:=rmk2). Defined. Next Obligation. simpl. intros A1 A2 i12 F1 F2 M. split; simpl. intros f1 f2 f2' if1f2 if1f2' a2 a2' w. (* prism *) pose (a1 := backw i12 a2). assert (rmk : i12 a1 a2). eapply cohb. assert (rmk2 : i12 a1 a2'). eapply (tri1 (trif i12)) with (1:=rmk) (2:=w). eapply (tri0 (triF M _ _ _)). eapply if1f2 with (w:=rmk). eapply if1f2' with (w:=rmk2). intros f1 f2 f2' if1f2 if2f2' a1 a2' w. pose (a2 := forw i12 a1). assert (a12 : i12 a1 a2). apply cohf. assert (a22' : (a2-->a2')%s). apply (tri0 (trif i12) a12 w). eapply (tri1 (triF M a12 w a22')) with (f2 a2). eapply if1f2 with (w:=a12). eapply if2f2' with (w:=a22'). intros f1 f2 f2' if1f2' if2f2' a1 a2 a12. pose (a2' := forw i12 a1). assert (a12' : i12 a1 a2'). apply cohf. assert (a22' : (a2-->a2')%s). apply (tri0 (trif i12) a12 a12'). eapply (tri2 (triF M a12 a12' a22')) with (f2' a2'). eapply if1f2' with (w:=a12'). eapply if2f2' with (w:=a22'). Defined. Next Obligation. simpl. intros A1 A2 i12 F1 F2 M. split; simpl. intros f1 f1' f2 if1f1' if1f2 a1' a2 a1'2. pose (a1 := backw i12 a2). assert (a12 : i12 a1 a2). apply cohb. assert (a11' : (a1-->a1')%s). apply (tri2 (trib i12) a12 a1'2). eapply (tri0 (triB M a11' a12 a1'2)) with (f1 a1). eapply if1f1' with (w:=a11'). eapply if1f2 with (w:=a12). intros f1 f1' f2 if1f1' if1'f2 a1 a2 a12. pose (a1' := backw i12 a2). assert (a1'2 : i12 a1' a2). apply cohb. assert (a11' : (a1-->a1')%s). apply (tri2 (trib i12) a12 a1'2). eapply (tri1 (triB M a11' a12 a1'2)). eapply if1f1' with (w:=a11'). eapply if1'f2 with (w:=a1'2). intros f1 f1' f2 if1f2 if1'f2 a1 a1' a11'. pose (a2 := forw i12 a1). assert (rmk : i12 a1 a2). eapply cohf. assert (rmk2 : i12 a1' a2). eapply (tri0 (trib i12)) with (1:=a11') (2:=rmk). eapply (tri2 (triB M a11' rmk rmk2)) with (f2 a2). eapply if1f2 with (w:=rmk). eapply if1'f2 with (w:=rmk2). Defined. Definition section_tri {A1 A2 A3} {i12:A1==>A2} {i13:A1==>A3} {i23:A2==>A3} {F1 F2 F3} {j12:isoFAM i12 F1 F2} {j13:isoFAM i13 F1 F3} {j23:isoFAM i23 F2 F3} : (i12 <-> i23 <-> i13) -> triFAM j12 j13 j23 -> (section_iso i12 j12 <-> section_iso i23 j23 <-> section_iso i13 j13). Print Grammar constr. intros i123 j123. split. simpl; intros f1 f2 f3 f12 f13 a2 a3 a23. pose (a1 := backw i12 a2). assert (rmk : i12 a1 a2). eapply cohb. assert (rmk2 : i13 a1 a3). eapply (tri1 i123) with (1:=rmk) (2:=a23). eapply (tri0 (j123 _ _ _ rmk rmk2 a23)). eapply f12. eapply f13. simpl; intros f1 f2 f3 f12 f23 a1 a3 a13. pose (a2 := forw i12 a1). assert (a12 : i12 a1 a2). eapply cohf. assert (a23 : i23 a2 a3). eapply (tri0 i123) with (1:=a12) (2:=a13). eapply (tri1 (j123 _ _ _ a12 a13 a23)). eapply f12. eapply f23. simpl; intros f1 f2 f3 f13 f23 a1 a2 a12. pose (a3 := forw i23 a2). assert (a23 : i23 a2 a3). eapply cohf. assert (a13 : i13 a1 a3). eapply (tri1 i123) with (1:=a12) (2:=a23). eapply (tri2 (j123 _ _ _ a12 a13 a23)). eapply f13. eapply f23. Defined. Program Definition Fun {S} (A:family S) (F:FAM S A) : family S := mkSub S U (fun s => section (A s) (F s)) (fun s1 s2 s12 => section_iso (sub_w A s12) (Fam_w F s12)) (fun s1 s2 s3 s12 s23 s13 t => section_tri (sub_t A t) (Fam_t F t)). Lemma eq_Fun_ctxt {T S} (A:family S) (F:FAM S A) (f:sub T S) : Fun A F ∘ f = Fun (A ∘ f) (substF F f). reflexivity. Defined. Program Definition app {S} {A:family S} {F:FAM S A} (c:elt S (Fun A F)) (a:elt S A) : elt S (App F a) := mkElt _ (App F a) (fun s => c s (a s)) (fun s1 s2 s12 => elt_w c _ _ _ (elt_w a s12)). Lemma eq_app_ctxt {T S} {A:family S} {F:FAM S A} (c:elt S (Fun A F)) (a:elt S A) (f:sub T S) : subst (app c a) f = app (A:=A ∘ f)(F:=substF F f) (subst c f) (subst a f). reflexivity. Defined. Program Definition lambda {S} {A:family S} {F:FAM S A} (b:elt (S+A) (App(substF F proj1) proj2)) : elt S (Fun A F) := mkElt _ (Fun A F) (fun s => mkSect (A s) (F s) (fun a=>b (s+a)%p) _) _. Next Obligation. intros S A F b s a1 a2 a12. pose (s' := iffLR(comp0 S) s). pose (w := coh00(Comp0 S) s). fold s' in w. pose (a2' := forw (sub_w A w) a2). assert (a22' := cohf (sub_w A w) a2). fold a2' in a22'. assert (a12' := tri1 (trib (sub_w A w)) a12 a22'). assert (Ft := triB (Fam_w F w) a12 a12' a22'). eapply (tri2 Ft) with (c:=b (s'+a2')%p). exact (elt_w b (w+a12')%w). exact (elt_w b (w+a22')%w). Defined. Next Obligation. simpl; intros. apply (elt_w b (w+w0)%w). Defined. Lemma eq_beta {T S} {A:family S} {F:FAM S A} (b:elt(S+A) (App(substF F proj1) proj2)) (f:sub T S) (a:elt T (A ∘ f)) : app (A:=A∘f) (F:=substF F f) (subst(lambda b) f) a = subst b (cons f a). reflexivity. Defined. Definition Pi {S} A (B:family(S+A)) : family S := Fun A (Lam B). (** Functional extentionality holds *) Program Definition extensionality {S} (A:family S) (B:FAM S A) (t u:elt S (Fun A B)) (e:elt (S+A) (Id (App (substF B proj1) proj2) (app ↑t proj2) (app ↑u proj2))) : elt S (Id (Fun A B) t u) := Tprop_elt _. Next Obligation. reflexivity. Defined. Next Obligation. reflexivity. Defined. Next Obligation. intros; simpl in e. apply Inh; simpl. intros a1 a2 a12. assert (rmk : (t s a1 -->[ηs a1] u s a1)%s). apply γs. exact (type_in_type (e (s+a1)%p)). assert (rmk2:= sect_w (u s) a12). eapply (tri1 (sub_t (B s) tt)) with (1:=rmk) (2:=rmk2). Defined. (** hProp revisited *) Definition hProp {S} (A:family S) : family S := Pi A (Pi ⇑A (Id ⇑⇑A ↑proj2 (proj2(A:=⇑A)))). Lemma hProp_ishProp {S} (A:family S) (e: elt S (hProp A)) : ishProp A. red; intros s1 s2 s12 a1 a2. eapply (tri1 (trif (sub_w A s12))). eapply cohf. exact (type_in_type (e s2 (forw (sub_w A s12) a1) a2)). Defined. Lemma univ_squash {S} (A:family S) (e:elt S (Tprop(Squash A))) (h:elt S (hProp A)) : elt S A. Proof uch A (hProp_ishProp A h) e. Program Definition arrow (A B:setoid) : setoid := mkSetRefl (morphism A B) (fun f1 f2 => forall a1 a2 (a12:(a1-->a2)%s), (f1 a1 --> f2 a2)%s) (fun f a1 a2 a12 => morph_w f a12) _. Next Obligation. intros A B. split; intros f1 f2 f3. intros xf1f2 xf1f3 a2 a3 a23. apply (tri0 (scomp1 B)) with (f1 a2); auto. apply xf1f2. apply ηs. intros xf1f2 xf2f3 a1 a3 a13. apply (tri1 (scomp1 B)) with (f2 a3); auto. apply xf2f3. apply ηs. intros xf1f3 xf2f3 a1 a2 a12. apply (tri2 (scomp1 B)) with (f3 a2); auto. apply xf2f3. apply ηs. Defined. Program Definition arrow_iso {A1 A2 B1 B2} (i:A1==>A2) (j:B1==>B2) : arrow A1 B1 ==> arrow A2 B2 := mkIso _ _ (fun f1 f2 => forall a1 a2 (a12:i a1 a2), j (f1 a1) (f2 a2)) (mkIff(fun f1 => mforw j ∘∘ f1 ∘∘ mbackw i)(fun f2 => mbackw j ∘∘ f2 ∘∘ mforw i)) _ _ _. Next Obligation. split; simpl. intros. apply (tri0 (trib j)) with (a (backw i a2)). apply morph_w. apply (tri2 (trib i)) with a2; trivial. apply cohb. apply cohf. intros. apply (tri1 (trif j)) with (b (forw i a1)). apply cohb. apply morph_w. apply (tri0 (trif i)) with a1; trivial. apply cohf. Defined. Next Obligation. intros A1 A2 B1 B2 i j. split; simpl; intros f1 f2 f2'. intros m12 m12' a2 a2' a22'. apply (tri0 (trif j)) with (f1 (backw i a2)). apply m12; apply cohb. apply m12'. apply (tri1 (trif i)) with a2; trivial. apply cohb. intros m12 m22' a1 a2' a12'. apply (tri1 (trif j)) with (f2 (forw i a1)). apply m12; apply cohf. apply m22'. apply (tri0 (trif i)) with a1; trivial. apply cohf. intros m12' m22' a1 a2 a12. apply (tri2 (trif j)) with (f2' (forw i a1)). apply m12'; apply cohf. apply m22'. apply (tri0 (trif i)) with a1; trivial. apply cohf. Defined. Next Obligation. intros A1 A2 B1 B2 i j. split; simpl; intros f1 f1' f2. intros m11' m12 a1' a2 a1'2. apply (tri0 (trib j)) with (f1 (backw i a2)). apply m11'. apply (tri2 (trib i)) with a2; trivial. apply cohb. apply m12; apply cohb. intros m11' m1'2 a1 a2 a12. apply (tri1 (trib j)) with (f1' (backw i a2)). apply m11'. apply (tri2 (trib i)) with a2; trivial. apply cohb. apply m1'2; apply cohb. intros m12 m1'2 a1 a1' a11'. apply (tri2 (trib j)) with (f2 (forw i a1)). apply m12; apply cohf. apply m1'2. apply (tri0 (trib i)) with a1; trivial. apply cohf. Defined. Program Definition Arrow {S:context} (A B:family S) : family S := mkSub S U (fun s => arrow (A s) (B s)) (fun s1 s2 s12 => arrow_iso (sub_w A s12) (sub_w B s12)) _. Next Obligation. intros S A B s0 s1 s2 s01 s02 s12 s012. split; simpl. intros m0 m1 m2 m01 m02 a1 a2 a12. apply (tri0 (sub_t B s012)) with (m0 (backw (sub_w A s01) a1)). apply m01. apply cohb. apply m02. apply (tri1 (sub_t A s012)) with a1; trivial. apply cohb. intros m0 m1 m2 m01 m12 a0 a2 a02. apply (tri1 (sub_t B s012)) with (m1 (forw (sub_w A s01) a0)). apply m01. apply cohf. apply m12. apply (tri0 (sub_t A s012)) with a0; trivial. apply cohf. intros m0 m1 m2 m02 m12 a0 a1 a01. apply (tri2 (sub_t B s012)) with (m2 (forw (sub_w A s02) a0)). apply m02. apply cohf. apply m12. apply (tri0 (sub_t A s012)) with a0; trivial. apply cohf. Defined. Infix "→" := Arrow (at level 60, right associativity). Infix "→" := arrow : setoid_scope. Program Definition lambda' {S:context}{A B} (b:elt (S+A) ⇑B) : elt S (A→B) := mkElt _ _ (fun s => mkMorph _ _ (fun x => b(s+x)%p) _) _. Next Obligation. intros S A B b s x x' w. pose (s' := iffLR(comp0 S) s). pose (w' := coh00(Comp0 S) s). fold s' in w'. pose (x'' := forw (sub_w A w') x'). assert (a22' := cohf (sub_w A w') x'). fold x'' in a22'. assert (a12' := tri1 (trib (sub_w A w')) w a22'). eapply (tri2 (trib (sub_w B w'))) with (c:=b (s'+x'')%p). exact (elt_w b (w'+a12')%w). exact (elt_w b (w'+a22')%w). Defined. Next Obligation. simpl; intros S A B b s0 s1 s01 a0 a1 a01. apply (elt_w b (s01+a01)%w). Defined. Program Definition app' {S:context}{A B} (u:elt S (A→B)) (v:elt S A) : elt S B := mkElt _ _ (fun s => u s (v s)) (fun s1 s2 s12 => _). Next Obligation. simpl; intros S A B u v s0 s1 s01. assert (rmk: v s0 -->[s01] v s1). apply (elt_w v). apply (elt_w u s01 _ _ rmk). Defined. (** app' expressed when type do not mention the last 1 or 2 variables of the context. Makes type-checking much faster. *) Definition app'1 {S A' A B} (u:elt (S+A') ⇑(A→B)) (a:elt (S+A') ⇑A) : elt (S+A') ⇑B := @app' (S+A') ⇑A ⇑B u a. Definition app'2 {S A' B' A B} (u:elt (S+A'+B') ⇑⇑(A→B)) (a:elt (S+A'+B') ⇑⇑A) : elt (S+A'+B') ⇑⇑B := @app' (S+A'+B') ⇑⇑A ⇑⇑B u a. (*****************************************************************************************************) (** Sigma-types *) Record sig_obj {S} {A:sfamily S} := mkSO { pis1 : S ; pis2 : A pis1}. Implicit Arguments sig_obj [ ]. Implicit Arguments mkSO [S A]. Record sig_rel {S} {A:sfamily S} {sa sa':sig_obj S A} := mkSR { pisr1 : (pis1 sa --> pis1 sa')%s ; pisr2 : (pis2 sa -->[pisr1] pis2 sa')%s }. Implicit Arguments sig_rel []. Program Definition sig_set (S:setoid) (A:sfamily S) : setoid := mkSet (sig_obj S A) (sig_rel S A) (mkIff(fun sa => mkSO(li0(scomp0 S)(pis1 sa))(forw(sub_w A (coh00(sComp0 S)(pis1 sa))) (pis2 sa))) (fun sa => mkSO(li1(scomp0 S)(pis1 sa))(backw(sub_w A (coh01(sComp0 S)(pis1 sa)))(pis2 sa)))) _ _. Next Obligation. intros S A. split; intros sa; simpl. exists (coh00(sComp0 S)(pis1 sa)); simpl. apply cohf. exists (coh01(sComp0 S)(pis1 sa)); simpl. apply cohb. Defined. Next Obligation. split. intros a0 a1 a2 a01 a02. exists (tri0 (scomp1 S) (pisr1 a01) (pisr1 a02)). apply (tri0 (sub_t A tt) (pisr2 a01) (pisr2 a02)). intros a0 a1 a2 a01 a12. exists (tri1 (scomp1 S) (pisr1 a01) (pisr1 a12)). apply (tri1 (sub_t A tt) (pisr2 a01) (pisr2 a12)). intros a0 a1 a2 a02 a12. exists (tri2 (scomp1 S) (pisr1 a02) (pisr1 a12)). apply (tri2 (sub_t A tt) (pisr2 a02) (pisr2 a12)). Defined. Program Definition sig_iso {A1 A2} (i12:A1==>A2) {F1 F2} (M:isoFAM i12 F1 F2) : sig_set A1 F1 ==> sig_set A2 F2 := mkIso (sig_set A1 F1) (sig_set A2 F2) (fun af1 af2 => { a12 : i12 (pis1 af1) (pis1 af2) & isoF M a12 (pis2 af1) (pis2 af2)}) (mkIff(fun af => mkSO (forw i12 (pis1 af)) (forw (isoF M (cohf i12 (pis1 af))) (pis2 af))) (fun af => mkSO (backw i12 (pis1 af)) (backw (isoF M (cohb i12 (pis1 af))) (pis2 af)))) _ _ _. Next Obligation. intros A1 A2 i12 F1 F2 M. split. intros af1; simpl. exists (cohf i12 (pis1 af1)); simpl. eapply cohf. intros af2. exists (cohb i12 (pis1 af2)); simpl. eapply cohb. Defined. Next Obligation. intros A1 A2 i12 F1 F2 M. split; intros af1 af2 af2'. intros if12 if12'. pose (rmk := tri0 (trif i12) (projT1 if12) (projT1 if12') : (pis1 af2 --> pis1 af2')%s). exists rmk. eapply (tri0 (triF M (projT1 if12) (projT1 if12') rmk)). eapply (projT2 if12). eapply (projT2 if12'). intros if12 if22'. pose (rmk := tri1 (trif i12) (projT1 if12) (pisr1 if22')). exists rmk. eapply (tri1 (triF M (projT1 if12) rmk (pisr1 if22'))). eapply (projT2 if12). eapply (pisr2 if22'). intros if12' if22'. pose (rmk := tri2 (trif i12) (projT1 if12') (pisr1 if22')). exists rmk. eapply (tri2 (triF M rmk (projT1 if12') (pisr1 if22'))). eapply (projT2 if12'). eapply (pisr2 if22'). Defined. Next Obligation. intros A1 A2 i12 F1 F2 M. split; intros af1 af1' af2. intros if11' if1'2. pose (rmk := tri0 (trib i12) (pisr1 if11') (projT1 if1'2)). exists rmk. eapply (tri0 (triB M (pisr1 if11') (projT1 if1'2) rmk)). eapply (pisr2 if11'). eapply (projT2 if1'2). intros if11' if1'2. pose (rmk := tri1 (trib i12) (pisr1 if11') (projT1 if1'2)). exists rmk. eapply (tri1 (triB M (pisr1 if11') rmk (projT1 if1'2))). eapply (pisr2 if11'). eapply (projT2 if1'2). intros if12 if1'2. pose (rmk := tri2 (trib i12) (projT1 if12) (projT1 if1'2)). exists rmk. eapply (tri2 (triB M rmk (projT1 if12) (projT1 if1'2))). eapply (projT2 if12). eapply (projT2 if1'2). Defined. Definition sig_tri {A1 A2 A3} {i12:A1==>A2} {i13:A1==>A3} {i23:A2==>A3} {F1 F2 F3} {j12:isoFAM i12 F1 F2} {j13:isoFAM i13 F1 F3} {j23:isoFAM i23 F2 F3} : (i12 <-> i23 <-> i13) -> triFAM j12 j13 j23 -> (sig_iso i12 j12 <-> sig_iso i23 j23 <-> sig_iso i13 j13). intros i123 j123. split. simpl; intros af1 af2 af3 af12 af13. assert (rmk := tri0 i123 (projT1 af12) (projT1 af13)). exists rmk. eapply (tri0 (j123 _ _ _ (projT1 af12) (projT1 af13) rmk)). eapply (projT2 af12). eapply (projT2 af13). simpl; intros af1 af2 af3 af12 af23. assert (rmk := tri1 i123 (projT1 af12) (projT1 af23)). exists rmk. eapply (tri1 (j123 _ _ _ (projT1 af12) rmk (projT1 af23))). eapply (projT2 af12). eapply (projT2 af23). simpl; intros af1 af2 af3 af13 af23. assert (rmk := tri2 i123 (projT1 af13) (projT1 af23)). exists rmk. eapply (tri2 (j123 _ _ _ rmk (projT1 af13) (projT1 af23))). eapply (projT2 af13). eapply (projT2 af23). Defined. Definition Sum {S} (A:family S) (F:FAM S A) : family S := mkSub S U (fun s => sig_set (A s) (F s)) (fun s1 s2 s12 => sig_iso (sub_w A s12) (Fam_w F s12)) (fun s1 s2 s3 s12 s23 s13 s123 => sig_tri (sub_t A s123) (Fam_t F s123)). Lemma eq_Sum_ctxt {T S} (A:family S) (F:FAM S A) (f:sub T S) : Sum A F ∘ f = Sum (A ∘ f) (substF F f). reflexivity. Defined. Program Definition couple {S} {A:family S} {F:FAM S A} (u:elt S A) (v:elt S (App F u)) : elt S (Sum A F) := mkElt _ (Sum A F) (fun s => mkSO (u s) (v s)) (fun s1 s2 s12 => existT _ (elt_w u s12) (elt_w v s12)). Program Definition sig_p1 {S} {A:family S} {F:FAM S A} (c:elt S (Sum A F)) : elt S A := mkElt _ _ (fun s => pis1 (c s)) (fun s1 s2 s12 => projT1 (elt_w c s12)). Program Definition sig_p2 {S} {A:family S} {F:FAM S A} (c:elt S (Sum A F)) : elt S (App F (sig_p1 c)) := mkElt _ _ (fun s => pis2 (c s)) (fun s1 s2 s12 => projT2 (elt_w c s12)). Lemma eq_sig1 {S} {A:family S} {F:FAM S A} (u:elt S A) (v:elt S (App F u)) : sig_p1 (couple u v) = etae' u. reflexivity. Qed. Lemma eq_sig2 {S} {A:family S} {F:FAM S A} (u:elt S A) (v:elt S (App F u)) : sig_p2 (couple u v) = etae' v. reflexivity. Qed. Lemma eq_ctxt_couple {S T:context} {A:family S} {F:FAM S A} {f:sub T S} (u:elt S A) (v:elt S (App F u)) : subst (couple u v) f = couple (F:=substF F f) (subst u f) (subst v f). reflexivity. Qed. Definition Sigma {S} (A:family S) (B:family(S+A)) : family S := Sum A (Lam B). Program Definition prodcart (A B:setoid) : setoid := mkSet (A*B) (fun p1 p2 => (fst p1 --> fst p2)%s*(snd p1 --> snd p2)%s) (mkIff(fun p1 => (li0 (scomp0 A) (fst p1), li0 (scomp0 B) (snd p1))) (fun p2 => (li1 (scomp0 A) (fst p2), li1 (scomp0 B) (snd p2)))) (mkCoh0(fun p1 => (coh00 (sComp0 A) (fst p1), coh00 (sComp0 B) (snd p1))) (fun p2 => (coh01 (sComp0 A) (fst p2), coh01 (sComp0 B) (snd p2)))) (mkTri(fun _ _ _ p12 p13 => (tri0 (scomp1 A) (fst p12) (fst p13),tri0(scomp1 B)(snd p12)(snd p13))) (fun _ _ _ p12 p23 => (tri1 (scomp1 A) (fst p12) (fst p23),tri1(scomp1 B)(snd p12)(snd p23))) (fun _ _ _ p13 p23 => (tri2 (scomp1 A) (fst p13) (fst p23),tri2(scomp1 B)(snd p13)(snd p23))) ). Program Definition prodcart_iso {A1 A2 B1 B2} (i:A1==>A2) (j:B1==>B2) : prodcart A1 B1 ==> prodcart A2 B2 := mkIso _ _ (fun p1 p2 => i (fst p1) (fst p2) * j (snd p1) (snd p2)) (mkIff(fun p1 => (forw i (fst p1), forw j (snd p1))) (fun p2 => (backw i (fst p2), backw j (snd p2)))) _ _ _. Next Obligation. split; simpl. split; apply cohf. split; apply cohb. Defined. Next Obligation. intros A1 A2 B1 B2 i j. split; simpl; intros p1 p2 p2'. intros m12 m12'. split. apply (tri0 (trif i)) with (1:=fst m12) (2:=fst m12'). apply (tri0 (trif j)) with (1:=snd m12) (2:=snd m12'). intros m12 m22'. split. apply (tri1 (trif i)) with (1:=fst m12) (2:=fst m22'). apply (tri1 (trif j)) with (1:=snd m12) (2:=snd m22'). intros m12' m22'. split. apply (tri2 (trif i)) with (1:=fst m12') (2:=fst m22'). apply (tri2 (trif j)) with (1:=snd m12') (2:=snd m22'). Defined. Next Obligation. intros A1 A2 B1 B2 i j. split; simpl; intros p1 p1' p2. intros m11' m12. split. apply (tri0 (trib i)) with (1:=fst m11') (2:=fst m12). apply (tri0 (trib j)) with (1:=snd m11') (2:=snd m12). intros m11' m1'2. split. apply (tri1 (trib i)) with (1:=fst m11') (2:=fst m1'2). apply (tri1 (trib j)) with (1:=snd m11') (2:=snd m1'2). intros m12 m1'2. split. apply (tri2 (trib i)) with (1:=fst m12) (2:=fst m1'2). apply (tri2 (trib j)) with (1:=snd m12) (2:=snd m1'2). Defined. Program Definition Prodcart {S:context} (A B:family S) : family S := mkSub S U (fun s => prodcart (A s) (B s)) (fun s1 s2 s12 => prodcart_iso (sub_w A s12) (sub_w B s12)) _. Next Obligation. intros S A B s0 s1 s2 s01 s02 s12 s012. split; simpl; intros m0 m1 m2 ma mb; split. apply (tri0 (sub_t A s012)) with (1:=fst ma)(2:=fst mb). apply (tri0 (sub_t B s012)) with (1:=snd ma)(2:=snd mb). apply (tri1 (sub_t A s012)) with (1:=fst ma)(2:=fst mb). apply (tri1 (sub_t B s012)) with (1:=snd ma)(2:=snd mb). apply (tri2 (sub_t A s012)) with (1:=fst ma)(2:=fst mb). apply (tri2 (sub_t B s012)) with (1:=snd ma)(2:=snd mb). Defined. Infix "×" := Prodcart (at level 50). Infix "×" := prodcart : setoid_scope. Program Definition fst' {S}{A B:family S}(p:elt S (A×B)) : elt S A := mkElt _ _ (fun s => fst (p s)) (fun s0 s1 s01 => fst (elt_w p s01)). Program Definition snd' {S}{A B:family S}(p:elt S (A×B)) : elt S B := mkElt _ _ (fun s => snd (p s)) (fun s0 s1 s01 => snd (elt_w p s01)). Program Definition fst'1 {S}{A' A B:family S}(p:elt (S+A') (⇑A×⇑B)) : elt (S+A') ⇑A := @fst' (S+A') ⇑A ⇑B p. Program Definition snd'1 {S}{A' A B:family S}(p:elt (S+A') (⇑A×⇑B)) : elt (S+A') ⇑B := @snd' (S+A') ⇑A ⇑B p. Program Definition fst'2 {S A' B'}{A B:family S}(p:elt (S+A'+B') (⇑⇑A×⇑⇑B)) : elt (S+A'+B') ⇑⇑A := @fst' (S+A'+B') ⇑⇑A ⇑⇑B p. Program Definition snd'2 {S A' B'}{A B:family S}(p:elt (S+A'+B') (⇑⇑A×⇑⇑B)) : elt (S+A'+B') ⇑⇑B := @snd' (S+A'+B') ⇑⇑A ⇑⇑B p. (*****************************************************************************************************) (** Example: univalence *) Section Univalence. (* Definition WEQ {S} (A B:family S) : family S := Sigma ((A → B)×(B → A)) (let f := fst'(A:=⇑A→⇑B)(B:=⇑B→⇑A)(proj2(A:=(A→B)×(B→A))) in let g := snd'(A:=⇑A→⇑B)(B:=⇑B→⇑A)(proj2(A:=(A→B)×(B→A))) in Pi ⇑A (Id ⇑⇑A (app'1 ↑g (app'1 ↑f proj2)) proj2) × Pi ⇑B (Id ⇑⇑B (app'1 ↑f (app'1 ↑g proj2)) proj2) ). *) (** Weak equivalences between types *) Record Iso (A B:U) := mkISO { Iso_f : morphism A B; Iso_g : morphism B A; Iso_id1 : forall x:A, (Iso_g (Iso_f x) --> x)%s; Iso_id2 : forall y:B, (Iso_f (Iso_g y) --> y)%s }. Implicit Arguments Iso_f [A B]. Implicit Arguments Iso_g [A B]. Implicit Arguments Iso_id1 [A B]. Implicit Arguments Iso_id2 [A B]. Program Definition Univalence {A B:U} (I:Iso A B) : A-->B := mkIso A B (fun a b => (Iso_f I a --> b)%s) (mkIff (Iso_f I) (Iso_g I)) _ _ _. Next Obligation. intros A B I. split. intros a. simpl. apply ηs. intros b. simpl. apply (Iso_id2 I). Defined. Next Obligation. intros A B I. split. intros a b b' xab xab'. apply (tri0 (scomp1 B)) with (1:=xab) (2:=xab'). intros a b b' xab xbb'. apply (tri1 (scomp1 B)) with (1:=xab) (2:=xbb'). intros a b b' xab' xbb'. apply (tri2 (scomp1 B)) with (1:=xab') (2:=xbb'). Defined. Next Obligation. intros A B I. split. intros a a' b xaa' xab. apply (tri0 (scomp1 B)) with (Iso_f I a); trivial. apply (morph_w (Iso_f I)); trivial. intros a a' b xaa' xa'b. apply (tri1 (scomp1 B)) with (Iso_f I a'); trivial. apply (morph_w (Iso_f I)); trivial. intros a a' b xab xa'b. assert (gfa : (Iso_g I (Iso_f I a) --> a)%s). apply (Iso_id1 I). assert (gfa' : (Iso_g I (Iso_f I a') --> a')%s). apply (Iso_id1 I). apply (tri0 (scomp1 A)) with (1:=gfa). apply (tri1 (scomp1 A)) with (2:=gfa'). apply (morph_w (Iso_g I)). apply (tri2 (scomp1 B)) with (1:=xab) (2:=xa'b). Defined. End Univalence. Implicit Arguments Iso_f [A B]. Implicit Arguments Iso_g [A B]. (** Another example: N1=N1->N1 *) Definition N1 : U := triv unit. Program Definition Iso_N1_N1toN1 : Iso N1 (N1→N1)%s := mkISO _ _ (mkMorph _ _ (fun n1 => mkMorph _ _ (fun n1' => n1') _) _) (mkMorph _ _ (fun f1 => tt) _) _ _. Next Obligation. simpl. trivial. Defined. Next Obligation. simpl. trivial. Defined. Next Obligation. simpl; intros. exact tt. Defined. Next Obligation. simpl; intros. trivial. Defined. Next Obligation. simpl; intros. trivial. Defined. (** Example 3: *) Definition generic_family : family U := mkSub _ _ (fun X => X) (fun _ _ w => w) (fun _ _ _ _ _ _ t => t). Definition CtxPair := U + generic_family + ⇑generic_family. Definition EqFam : family CtxPair := Id ⇑⇑generic_family ↑proj2 proj2. (** same as hProp but on context U *) Definition HProp : family U := Pi generic_family (Pi ⇑generic_family EqFam). Program Definition hProp_N1 : HProp N1 : Type := (* :Type -> bug in Program ? *) mkSect _ _ (fun n1 => mkSect _ _ (fun n2 => Inh tt) _) _. Next Obligation. simpl; trivial. Defined. Next Obligation. simpl; trivial. Defined. Lemma eqN1_N1toN1 : N1 --> arrow N1 N1. apply Univalence. exact Iso_N1_N1toN1. Defined. Lemma hProp_N1toN1 : HProp (arrow N1 N1). assert (rmk: HProp N1 --> HProp(arrow N1 N1)). apply (sub_w HProp). exact eqN1_N1toN1. apply (forw rmk). exact hProp_N1. Defined. Section Test. Variable f0 f1:arrow N1 N1. Eval compute in hProp_N1toN1 f0 f1. End Test. (** Generic transport of structure *) Section GenericTransport. Variable A B: U. Variable Struct : family U. Variable instance : Struct A. Hypothesis i : Iso A B. Definition transport_structure : Struct B := forw (sub_w Struct (Univalence i)) instance. End GenericTransport. (** Monoids *) Section Monoid. Let X : family U := generic_family. Let ctx := U + ((X→X→X)×X) + ⇑X. Let p : elt ctx (⇑⇑(X→X→X)×⇑⇑X) := ↑proj2. Let op : elt ctx ⇑⇑(X→X→X) := fst' p. Let unit : elt ctx ⇑⇑X := snd' p. Let x : elt ctx ⇑⇑X := proj2. Definition Monoid : family U := Sigma ((X→X→X)×X) (Pi ⇑X (Id ⇑⇑X (app'2 (app'2 op x) unit) x)). Variable A B:U. Hypothesis Aop : (A→A→A)%s. Hypothesis Aunit : A. Hypothesis Aunitl : forall x:A, (Aop x Aunit --> x)%s. Definition Amon : Monoid A. exists (Aop,Aunit). exists (fun x => Inh (Aunitl x)). simpl; intros; exact tt. Defined. Hypothesis i : Iso A B. Let Bmon := transport_structure _ _ _ Amon i. Let Bop : (B→B→B)%s := fst (pis1 Bmon). Let Bunit : B := snd (pis1 Bmon). Lemma Bop_def b1 b2 : Bop b1 b2 = Iso_f i (Aop (Iso_g i b1) (Iso_g i b2)). reflexivity. Qed. Lemma Bunit_def : Bunit = Iso_f i Aunit. reflexivity. Qed. Lemma Bunitl : forall x:B, (Bop x Bunit --> x)%s. exact (fun x => type_in_type (pis2 Bmon x)). Defined. Let j (y:B) : inh (Aop (backw _ y) Aunit --> backw _ y)%s <-> inh (Bop y Bunit --> y)%s := let w : Univalence i (Aop (backw _ y) Aunit) (Bop y Bunit) := (cohf (arrow_iso _ (arrow_iso _ _)) Aop _ _ (cohb _ y) _ _ (cohf _ Aunit)) in let w' : Univalence i (backw _ y) y := cohb _ y in (mkIff (inh_map (transpf_square w w')) (inh_map (transpb_square w w'))). Lemma Bunitl_def (y:B) : Bunitl y = type_in_type (forw (triv_iso (j y)) (Inh (Aunitl (backw (Univalence i) y)))). unfold Bunitl. simpl. reflexivity. Qed. End Monoid. (** Application: transport boolean op by the negation iso yields boolean or *) (** We use a functional encoding of booleans *) Definition Bcmp (b1 b2:forall X:Type,X->X->X) : Prop := forall X (R:X->X->Prop) t t' f f', R t t' -> R f f' -> R (b1 _ t f) (b2 _ t' f'). Lemma Bcmp_sym {b1 b2} : Bcmp b1 b2 -> Bcmp b2 b1. unfold Bcmp; intros e Y R t t' f f' Rt Rf. apply e with (R:=fun x y => R y x); trivial. Defined. Lemma Bcmp_trans {b1 b2 b3} : Bcmp b1 b2 -> Bcmp b2 b3 -> Bcmp b1 b3. unfold Bcmp; intros. assert (h:=H0 _ (fun x2 x3 => forall x1, R x1 x2 -> R x1 x3)); simpl in h. eapply h. 3:eapply H. 3:eexact H1. 3:eexact H2. auto. auto. Defined. Program Let B : setoid := mkSetRefl{b:forall Y:Type,Y->Y->Y|Bcmp b b} (fun b1 b2 => Bcmp (proj1_sig b1) (proj1_sig b2)) _ _. Next Obligation. intros b; apply (proj2_sig b). Defined. Next Obligation. split; intros. apply @Bcmp_trans with (proj1_sig a); auto using Bcmp_sym. apply @Bcmp_trans with (proj1_sig b); auto using Bcmp_sym. apply @Bcmp_trans with (proj1_sig c); auto using Bcmp_sym. Defined. Definition Beq := @srel B. Program Let TRUE : B:Type := exist _ (fun Y t f => t) (fun _ _ _ _ _ _ e1 e2=>e1). Program Let FALSE : B:Type := exist _ (fun Y t f => f) (fun _ _ _ _ _ _ e1 e2=>e2). Program Let IFB (b t e:B) : B := exist _ (fun Y y y' => b Y (t Y y y') (e Y y y')) _. Next Obligation. red; simpl; intros. apply (proj2_sig b). apply (proj2_sig t); trivial. apply (proj2_sig e); trivial. Defined. Definition AND b1 b2 := IFB b1 b2 FALSE. Definition OR b1 b2 := IFB b1 TRUE b2. Definition NOT b := IFB b FALSE TRUE. Program Definition ANDm : (B→B→B)%s : Type := mkMorph _ _ (fun b1 => mkMorph _ _ (fun b2 => AND b1 b2) _) _. Next Obligation. simpl; intros. red; simpl; intros. apply (proj2_sig b1); trivial. apply H; trivial. Defined. Next Obligation. simpl; intros. red; simpl; intros. apply H; trivial. apply a12; trivial. Defined. Program Definition NOTm : (B→B)%s : Type := mkMorph _ _ NOT _. Next Obligation. simpl; intros. red; simpl; intros. apply H; trivial. Defined. Lemma NOT_invol b : (NOT (NOT b) --> b)%s. simpl. apply (proj2_sig b). Qed. Definition negb_iso : Iso B B := mkISO _ _ NOTm NOTm NOT_invol NOT_invol. Lemma true_unitl_and : forall b:B, Beq (AND b TRUE) b. Proof. red; simpl; red; simpl; intros. apply (proj2_sig b); trivial. Qed. Lemma false_unitl_or : forall b:B, Beq (OR b FALSE) b. exact (Bunitl _ _ ANDm TRUE true_unitl_and negb_iso). Qed. (** Choice does not hold in the model *) Section NoChoice. Definition N0 := cst_type (S:=U) (triv False). Hypothesis CHholds : elt U (((generic_family→N0)→N0)→generic_family). (** A theorem "for free": negation has no fixpoint *) Definition discr b (abs:Beq (NOT b) b) : False := abs Prop (fun X Y => (X->Y)->(Y->X)->False) True False False True (fun h1 h2 => h1 I) (fun h1 h2 => h2 I) (fun x => x) (fun x => x). (** The double negation of bool is inhabited *) Let m : ((B→triv False)→triv False)%s. simpl. exists (fun f:(B→triv False)%s => f TRUE). intros; exact tt. Qed. Lemma choice_does_not_hold : False. (** The image of m by CHholds is related by any iso from B to B, let us take negation *) assert (h := elt_w CHholds (Univalence negb_iso) m m (fun _ _ _ => tt)). simpl in h. exact (discr _ h). Qed. End NoChoice.