Skip to content

Instantly share code, notes, and snippets.

View zraffer's full-sized avatar
πŸš€
let it be

Bay Raktar zraffer

πŸš€
let it be
16 followers · 18 following
  • Ukraine
View GitHub Profile
@zraffer
zraffer / MySum.idr
Created September 28, 2014 10:01
module MySum
record ADepType : Type where
MkADepType :
(dtBase : Type) ->
(dtFiber : dtBase -> Type) ->
ADepType
record ADepSum : ADepType -> Type where
MkADepSum :
@zraffer
zraffer / idris-error-1.idr
Created October 7, 2014 18:03
Monoid_Unit : Type -> Type
Monoid_Unit carrier = carrier
data TypeUnit : (Monoid_Unit Type) where
MkTypeUnit : TypeUnit
@zraffer
zraffer / idris-error-3.idr
Last active August 29, 2015 14:07
infixr 1 ~>
Relation_Arrow : Type -> Type
Relation_Arrow ob = (source, target: ob) -> Type
class RelationClass (ob: Type) where
(~>) : Relation_Arrow ob
record RelationRecord : Type where
MkRelation : (recOb: Type) -> (recInst: RelationClass recOb) -> RelationRecord
@zraffer
zraffer / idris-error-inductive.idr
Created November 30, 2014 19:46
mutual
data T1 : Type where
Mk1 : T1
Mk2 : T2 Mk1 -> T1
data T2 : T1 -> Type where
Mk0 : T2 Mk1
@zraffer
zraffer / Auto.agda
Created November 30, 2014 19:47
module Auto where
mutual
data T1 : Set where
Mk1 : T1
Mk2 : T2 Mk1 -> T1
data T2 : T1 -> Set where
Mk0 : T2 Mk1
@zraffer
zraffer / package.scala
Last active April 26, 2017 11:17
a few operations with functors
package object types {
import scala.language.reflectiveCalls
import scala.language.higherKinds
// quantifiers aka (co)ends
type Forall[+F[_]] = { def apply[X]: F[X] }
type Exists[+F[_]] = F[_]
// basic categorical notions
@zraffer
zraffer / iterY.idr
Created August 18, 2015 12:33
get Y-combinator from infinite number
module iterY
total
iter : Nat->(x->x)->(x->x)
iter Z f = id
iter (S n) f = f . (iter n f)
partial
inf : Nat
inf = S inf
@zraffer
zraffer / noInfinity.idr
Last active August 29, 2015 14:27
proof of absence of infinity
module noInfinity
%default total
data T2 = Mk1 | Mk2
Mk1neqMk2 : Not (Mk1 = Mk2)
Mk1neqMk2 Refl impossible
Mk2neqMk1 : Not (Mk2 = Mk1)
@zraffer
zraffer / gist:732c689d6ca7a43f75e6
Created February 20, 2016 13:34
fast term
Ξ»(sh : βˆ€(Shadow : *) β†’ βˆ€(ShadowOk : Shadow β†’ *) β†’ βˆ€(ShadowEqu : Shadow β†’ Shadow β†’ *) β†’ βˆ€(ShadowRefl : βˆ€(s : Shadow) β†’ ShadowEqu s s) β†’ βˆ€(ShadowTrans : βˆ€(s1 : Shadow) β†’ βˆ€(s2 : Shadow) β†’ βˆ€(s3 : Shadow) β†’ ShadowEqu s1 s2 β†’ ShadowEqu s2 s3 β†’ ShadowEqu s1 s3) β†’ βˆ€(ShadowSym : βˆ€(s1 : Shadow) β†’ βˆ€(s2 : Shadow) β†’ ShadowEqu s1 s2 β†’ ShadowEqu s2 s1) β†’ βˆ€(Mk : βˆ€(A : *) β†’ βˆ€(AOk : A β†’ *) β†’ βˆ€(AEqu : A β†’ A β†’ *) β†’ βˆ€(ARefl : βˆ€(a : A) β†’ AEqu a a) β†’ βˆ€(ATrans : βˆ€(a1 : A) β†’ βˆ€(a2 : A) β†’ βˆ€(a3 : A) β†’ AEqu a1 a2 β†’ AEqu a2 a3 β†’ AEqu a1 a3) β†’ βˆ€(ASym : βˆ€(a1 : A) β†’ βˆ€(a2 : A) β†’ AEqu a1 a2 β†’ AEqu a2 a1) β†’ Shadow) β†’ βˆ€(MkOk : βˆ€(A : *) β†’ βˆ€(AOk : A β†’ *) β†’ βˆ€(AEqu : A β†’ A β†’ *) β†’ βˆ€(ARefl : βˆ€(a : A) β†’ AEqu a a) β†’ βˆ€(ATrans : βˆ€(a1 : A) β†’ βˆ€(a2 : A) β†’ βˆ€(a3 : A) β†’ AEqu a1 a2 β†’ AEqu a2 a3 β†’ AEqu a1 a3) β†’ βˆ€(ASym : βˆ€(a1 : A) β†’ βˆ€(a2 : A) β†’ AEqu a1 a2 β†’ AEqu a2 a1) β†’ ShadowOk (Mk A AOk AEqu ARefl ATrans ASym)) β†’ βˆ€(MkIsoEqu : βˆ€(A : *) β†’ βˆ€(AOk : A β†’ *) β†’ βˆ€(AEqu : A β†’ A β†’ *) β†’ βˆ€(ARefl : βˆ€(a : A) β†’ AEqu a a) β†’ βˆ€(ATrans : βˆ€(a1 : A) β†’ βˆ€(a2 : A) β†’ βˆ€(a3 : A) β†’ AEqu a1
@zraffer
zraffer / AND
Created February 23, 2016 17:36
slowness issue for https://github.com/Gabriel439/Haskell-Morte-Library
-- #AND: #Prop -> #Prop -> #Prop
\(A: #Prop )-> \(B: #Prop )->
\/(AND: #Prop )->
\/(Intro: A -> B -> AND)->
AND