Skip to content

Instantly share code, notes, and snippets.

@5HT

5HT/gist:4116423b484af3602188

Created February 14, 2016 09:23
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save 5HT/4116423b484af3602188 to your computer and use it in GitHub Desktop.
Save 5HT/4116423b484af3602188 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
$ linja
[1/6] "/usr/local/Cellar/lean/0.2.0.20151115213912.gitdb59c6829c9f56c....clean" -i "/Users/5HT/depot/groupoid/exe/prelude/lean/Setoid.ilean"
structure SetoidType : Type.{l_1+1}
fields:
SetoidType.El : SetoidType.{l_1} → Type.{l_1}
SetoidType.Equ : Π (c : SetoidType.{l_1}), EquType.{l_1} (SetoidType.El.{l_1} c)
SetoidType.Refl : ∀ (c : SetoidType.{l_1}), Equ.ReflProp.{l_1} (SetoidType.Equ.{l_1} c)
SetoidType.Trans : ∀ (c : SetoidType.{l_1}), Equ.TransProp.{l_1} (SetoidType.Equ.{l_1} c)
SetoidType.Sym : ∀ (c : SetoidType.{l_1}), Equ.SymProp.{l_1} (SetoidType.Equ.{l_1} c)
[2/6] "/usr/local/Cellar/lean/0.2.0.20151115213912.gitdb59c6829c9f56c...Cat.clean" -i "/Users/5HT/depot/groupoid/exe/prelude/lean/Cat.ilean"
definition Cat.HomType [reducible] : Type.{l_1} → Type.{max l_1 (l_2+1)} :=
HomType.{??l.1 ??l.2}
structure CatType : Type.{max (imax l_1 l_2) (l_1+1) (l_2+1)}
fields:
CatType.Ob : CatType.{l_1 l_2} → Type.{l_1}
CatType.Hom : Π (c : CatType.{l_1 l_2}), Cat.HomType.{l_1 l_2} (CatType.Ob.{l_1 l_2} c)
CatType.Id : Π (c : CatType.{l_1 l_2}), Cat.IdType.{l_1 l_2} (CatType.Hom.{l_1 l_2} c)
CatType.Mul : Π (c : CatType.{l_1 l_2}), Cat.MulType.{l_1 l_2} (CatType.Hom.{l_1 l_2} c)
CatType.UnitL : ∀ (c : CatType.{l_1 l_2}), Cat.UnitLProp.{l_1 l_2} (CatType.Id.{l_1 l_2} c) (CatType.Mul.{l_1 l_2} c)
CatType.UnitR : ∀ (c : CatType.{l_1 l_2}), Cat.UnitRProp.{l_1 l_2} (CatType.Id.{l_1 l_2} c) (CatType.Mul.{l_1 l_2} c)
CatType.Assoc : ∀ (c : CatType.{l_1 l_2}), Cat.AssocProp.{l_1 l_2} (CatType.Mul.{l_1 l_2} c)
[4/6] "/usr/local/Cellar/lean/0.2.0.20151115213912.gitdb59c6829c9f56c...clean" -i "/Users/5HT/depot/groupoid/exe/prelude/lean/Functor.ilean"
structure FunctorType : CatType.{l_1 l_2} → CatType.{l_3 l_4} → Type.{max 1 (imax l_1 l_3) (imax l_2 l_4) l_1}
fields:
FunctorType.onOb : Π {C : CatType.{l_1 l_2}} {D : CatType.{l_3 l_4}}, FunctorType.{l_1 l_2 l_3 l_4} C D → C → D
FunctorType.onHom : Π {C : CatType.{l_1 l_2}} {D : CatType.{l_3 l_4}} (c : FunctorType.{l_1 l_2 l_3 l_4} C D) {X Y : C},
(X⇒C⇒Y)⥤(FunctorType.onOb.{l_1 l_2 l_3 l_4} c X⇒D⇒FunctorType.onOb.{l_1 l_2 l_3 l_4} c Y)
FunctorType.onId : ∀ {C : CatType.{l_1 l_2}} {D : CatType.{l_3 l_4}} (c : FunctorType.{l_1 l_2 l_3 l_4} C D),
Functor.OnIdProp.{l_1 l_2 l_3 l_4} C D (FunctorType.onOb.{l_1 l_2 l_3 l_4} c) (FunctorType.onHom.{l_1 l_2 l_3 l_4} c)
FunctorType.onMul : ∀ {C : CatType.{l_1 l_2}} {D : CatType.{l_3 l_4}} (c : FunctorType.{l_1 l_2 l_3 l_4} C D),
Functor.OnMulProp.{l_1 l_2 l_3 l_4} C D (FunctorType.onOb.{l_1 l_2 l_3 l_4} c) (FunctorType.onHom.{l_1 l_2 l_3 l_4} c)
definition Functor.HomSet : Π {C : CatType.{l_1 l_2}} {D : CatType.{l_3 l_4}},
Cat.HomType.{(max 1 (imax l_1 l_3) (imax l_2 l_4) l_1) (max 1 (imax l_1 l_4))} (FunctorType.{l_1 l_2 l_3 l_4} C D) :=
λ (C : CatType.{l_1 l_2}) (D : CatType.{l_3 l_4}) (F G : FunctorType.{l_1 l_2 l_3 l_4} C D),
Setoid.MkOb.{??l.1} (HomType.{l_1 l_2 l_3 l_4} F G)
(λ (f g : HomType.{l_1 l_2 l_3 l_4} F G), ∀ (X : C), f/$$X ≡ (F$$X⇒D⇒G$$X)≡g/$$X)
(λ (f : HomType.{l_1 l_2 l_3 l_4} F G) (X : C), ⊜)
(λ (f g h : HomType.{l_1 l_2 l_3 l_4} F G)
(fg : (λ (f g : HomType.{l_1 l_2 l_3 l_4} F G), ∀ (X : C), f/$$X ≡ (F$$X⇒D⇒G$$X)≡g/$$X) f g)
(gh : (λ (f g : HomType.{l_1 l_2 l_3 l_4} F G), ∀ (X : C), f/$$X ≡ (F$$X⇒D⇒G$$X)≡g/$$X) g h) (X : C),
fg X⊡(F$$X⇒D⇒G$$X)⊡gh X)
(λ (f g : HomType.{l_1 l_2 l_3 l_4} F G)
(fg : (λ (f g : HomType.{l_1 l_2 l_3 l_4} F G), ∀ (X : C), f/$$X ≡ (F$$X⇒D⇒G$$X)≡g/$$X) f g) (X : C),
SetoidType.Sym.{l_4} (F$$X⇒D⇒G$$X) (fg X))
definition FunctorCat : CatType.{l_1 l_2} → CatType.{l_3 l_4} → CatType.{(max 1 (imax l_1 l_3) (imax l_2 l_4) l_1) (max 1 (imax l_1 l_4))} :=
λ (C : CatType.{l_1 l_2}) (D : CatType.{l_3 l_4}),
Cat.MkOb.{??l.1 ??l.2} (FunctorType.{l_1 l_2 l_3 l_4} C D) Functor.HomSet.{l_1 l_2 l_3 l_4}
Functor.Id.{l_1 l_2 l_3 l_4}
Functor.Mul.{l_1 l_2 l_3 l_4}
Functor.UnitL.{l_1 l_2 l_3 l_4}
Functor.UnitR.{l_1 l_2 l_3 l_4}
Functor.Assoc.{l_1 l_2 l_3 l_4}
definition Cat.MulFF : Π {C : CatType.{o1 h1}} {D : CatType.{o2 h2}} {E : CatType.{o3 h3}}, D⟶E → C⟶D → C⟶E :=
λ (C : CatType.{o1 h1}) (D : CatType.{o2 h2}) (E : CatType.{o3 h3}) (F : D⟶E) (G : C⟶D),
Functor.MkOb.{??l.1 ??l.2 ??l.3 ??l.4} (λ (X : C), F$$(G$$X))
(λ (X Y : C), FunctorType.onHom.{o2 h2 o3 h3} F∙FunctorType.onHom.{o1 h1 o2 h2} G)
(λ (X : C), F$$//FunctorType.onId.{o1 h1 o2 h2} G⊡(F$$(G$$X)⇒E⇒F$$(G$$X))⊡FunctorType.onId.{o2 h2 o3 h3} F)
(λ (X Y Z : C) (g : Y⇒C⇒Z) (f : X⇒C⇒Y),
F$$//FunctorType.onMul.{o1 h1 o2 h2} G g f⊡(F$$(G$$X)⇒E⇒F$$(G$$Z))⊡FunctorType.onMul.{o2 h2 o3 h3} F
(G$$/g)
(G$$/f))
[5/6] "/usr/local/Cellar/lean/0.2.0.20151115213912.gitdb59c6829c9f56c...an" -i "/Users/5HT/depot/groupoid/exe/prelude/lean/Adjunction.ilean"
structure AdjType : Π {C : CatType.{o1 h1}} {D : CatType.{o2 h2}}, D⟶C → C⟶D → Type.{max 1 (imax o1 h1) (imax o2 h2)}
fields:
AdjType.unit : Π {C : CatType.{o1 h1}} {D : CatType.{o2 h2}} {L : D⟶C} {R : C⟶D}, (L⊣R) → (𝟙⟹(R⊗L))
AdjType.counit : Π {C : CatType.{o1 h1}} {D : CatType.{o2 h2}} {L : D⟶C} {R : C⟶D}, (L⊣R) → (L⊗R⟹𝟙)
AdjType.triangleL : ∀ {C : CatType.{o1 h1}} {D : CatType.{o2 h2}} {L : D⟶C} {R : C⟶D} (c : L⊣R),
bash-3.2$
Adj.TriangleLProp.{o1 h1 o2 h2} L R (AdjType.unit.{o1 h1 o2 h2} c) (AdjType.counit.{o1 h1 o2 h2} c)
AdjType.triangleR : ∀ {C : CatType.{o1 h1}} {D : CatType.{o2 h2}} {L : D⟶C} {R : C⟶D} (c : L⊣R),
Adj.TriangleRProp.{o1 h1 o2 h2} L R (AdjType.unit.{o1 h1 o2 h2} c) (AdjType.counit.{o1 h1 o2 h2} c)
structure RightAdj : Π {C : CatType.{l_1 l_2}} {D : CatType.{l_3 l_4}},
D⟶C → Type.{max 1 (imax l_1 l_2) (imax l_1 l_3) (imax l_2 l_4) (imax l_3 l_4) l_1}
fields:
RightAdj.Right : Π {C : CatType.{l_1 l_2}} {D : CatType.{l_3 l_4}} {Left : D⟶C}, RightAdj.{l_1 l_2 l_3 l_4} Left → C⟶D
RightAdj.adj : Π {C : CatType.{l_1 l_2}} {D : CatType.{l_3 l_4}} {Left : D⟶C} (c : RightAdj.{l_1 l_2 l_3 l_4} Left),
Left⊣RightAdj.Right.{l_1 l_2 l_3 l_4} c
definition HaveAllLim : CatType.{l_1 l_2} →
Type.{max
(imax (max 1 (imax l_3 l_1) (imax l_4 l_2) l_3) l_1)
(imax (max 1 (imax l_3 l_2)) l_2)
(imax l_3 l_4)
(imax l_3 l_1)
(imax l_3 l_2)
(imax l_4 l_2)
(imax l_1 l_2)
(l_3+1)
(l_4+1)
l_3} :=
λ (D : CatType.{l_1 l_2}), Π (C : CatType.{l_3 l_4}), Lim.{l_3 l_4 l_1 l_2} C D
[6/6] "/usr/local/Cellar/lean/0.2.0.20151115213912.gitdb59c6829c9f56c...clean" -i "/Users/5HT/depot/groupoid/exe/prelude/lean/Initial.ilean"
structure InitialType : Π (C : CatType.{l_1 l_2}), C → Type.{max 1 (imax l_1 l_2)}
fields:
InitialType.Cone : Π {C : CatType.{l_1 l_2}} {Obj : C}, InitialType.{l_1 l_2} C Obj → Functor.ConeType.{l_1 l_2 l_1 l_2} Obj 𝟙
InitialType.IsCone : ∀ {C : CatType.{l_1 l_2}} {Obj : C} (c : InitialType.{l_1 l_2} C Obj),
Functor.IsConeProp.{l_1 l_2 l_1 l_2} Obj 𝟙 (InitialType.Cone.{l_1 l_2} c)
InitialType.Ok : ∀ {C : CatType.{l_1 l_2}} {Obj : C} (c : InitialType.{l_1 l_2} C Obj),
InitialType.Cone.{l_1 l_2} c Obj ≡ (Obj⇒C⇒Obj)≡①
definition Initial.FromLim : Π {C : CatType.{o1 h1}}, HaveAllLim.{o1 h1 o1 h1} C → C :=
λ (C : CatType.{o1 h1}) (lim : HaveAllLim.{o1 h1 o1 h1} C), Lim.Apply.{o1 h1 o1 h1} lim 𝟙
/Users/5HT/depot/groupoid/exe/prelude/lean/Initial.lean:60:18: warning: using 'sorry'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment